Missing file.

diff --git a/.gitignore b/.gitignore
index 5f1da95e158f42cedba27f31a631bd9b5e1d8d14..6e0786af59b7da35aa637731ca5231f40b3c3c3c 100644 (file)
--- a/.gitignore
+++ b/.gitignore
@@ -13,6 +13,7 @@ sync
 doc/manual/html
 doc/manual/pdf
 doc/manual/extensions.ent
+doc/manual/config.xml
 doc/design/*.pdf
 doc/design/*.log
 doc/design/*.aux

diff --git a/doc/manual/config.py b/doc/manual/config.py
new file mode 100644 (file)
index 0000000..673174b
--- /dev/null
+++ b/doc/manual/config.py
@@ -0,0 +1,24 @@
+import sys
+current_tag = None
+current_doc = None
+current_opt = False
+print '<itemizedlist>'
+with open(sys.argv[1]) as f:
+    for line in f:
+        line = line.strip();
+        if line.startswith('/* [XML'):
+            code = line.split()[1]
+            current_tag = line.split()[2]
+            current_opt = code == '[XML:opt]'
+            line = line[5+len(code)+len(current_tag):]
+            current_doc = ''
+        if current_tag is not None:
+            current_doc += line.replace('/* [XML] ', '').replace('*/', '').strip() + ' '
+        if line.find('*/') != -1 and current_tag is not None:
+            if current_opt:
+                optional = ' (optional)'
+            else:
+                optional = ''
+            print '<listitem><code>&lt;%s&gt;</code>%s &#8212; %s</listitem>' % (current_tag, optional, current_doc.strip())
+            current_tag = None
+print '</itemizedlist>'