This commit was manufactured by cvs2svn to create branch 'init'.

[helm.git] / helm / xmltheory / XmlTheory / README

diff --git a/helm/xmltheory/XmlTheory/README b/helm/xmltheory/XmlTheory/README
deleted file mode 100644 (file)
index ce4c86c..0000000
--- a/helm/xmltheory/XmlTheory/README
+++ /dev/null
@@ -1,78 +0,0 @@
-Here we show the procedure to follow to add the recognition of
-a new syntactical form.
-
-Form to recognize in the model:
-
-Lemma existsDec : (l:(list A)){(list_exists l)}+{~(list_exists l)}.
-
-1. cd V7 ; grep "Lemma" */*.ml4
-   the result should be one or a few files. In this case the
-   only file is parsing/g_vernac.ml4. In the case of many files,
-   only one is the good one.
-2. open the file and search for Lemma:
-   thm_tok:
-    [ [ "Theorem" -> <:ast< "THEOREM" >>
-      | IDENT "Lemma" -> <:ast< "LEMMA" >>
-      | IDENT "Fact" -> <:ast< "FACT" >>
-      | IDENT "Remark" -> <:ast< "REMARK" >>
-      | IDENT "Decl" -> <:ast< "DECL" >> ] ]
-
-   so a Lemma is mapped into an ast of phylum thm_tok.
-   Let's search for thm_tok. Many occurrences are found,
-   but the only one that matches the form to recognize is
-
-  gallina:
-    (* Definition, Goal *)
-    [ [ thm = thm_tok; id = identarg; ":"; c = constrarg ->
-          <:ast< (StartProof $thm $id $c) >>
-
-  So the ast created is tagged StartProof
-3. grep "StartProof" */*.ml   (usually toplevel/...)
-   Open the file and search for StartProof.
-   This is found:
-    let _ =
-  add "StartProof"
-    (function
-       | [VARG_STRING kind;VARG_IDENTIFIER s;VARG_CONSTR com] ->
-           ...
-4. edit xmltheoryentries.ml and copy the entry for another rule,
-   substituting StartProof as the parameter for set_hook and
-   using the above match (with V. added where appropriate) after function:
-
-let module V = Vernacinterp in
- set_hook "StartProof"
-  (function
-      [V.VARG_STRING kind;V.VARG_IDENTIFIER s;V.VARG_CONSTR com] ->
-       ???
-    | _ -> fail ()
-  )
-;;
-
-    Finally, write OCaml code to print to XML the availables interesting
-    infos. In our case the code becomes
-
-let module V = Vernacinterp in
- set_hook "StartProof"
-  (function
-      [V.VARG_STRING kind;V.VARG_IDENTIFIER s;V.VARG_CONSTR com] ->
-       IXml.output
-        (Xml.xml_empty
-          "THEOREM"
-          ["uri", Names.string_of_id s ^ ".con"; "as",kind]
-        )
-    | _ -> fail ()
-  )
-;;
-
-     IXml.output should always be present and the code inside
-     (that is simply XML written in OCaml form) should be changed.
-     The syntax is
-        Xml.xml_empty "name" ["att1","value1" ; ... ; "attn","valuen"]
-     to create an empty element name with attributes att1 ... attn.
-     To create a non-empty element, use
-        Xml.xml_nempty "name" ["att1","value1" ; ... ; "attn","valuen"]
-         stream
-     where stream is an OCaml stream of other XML elements, as:
-       * another Xml.xml_nempty 
-       * an Xml.xml_empty
-       * [< stream1 ; ... ; streamk >]