
diff -r dd8eebae11ec -r 123401a5c8e9 CookBook/Parsing.thy
--- a/CookBook/Parsing.thy	Thu Feb 05 22:44:11 2009 +0000
+++ b/CookBook/Parsing.thy	Fri Feb 06 06:19:52 2009 +0000
@@ -515,38 +515,104 @@
 
 *}
 
-ML{*
-  OuterParse.position
-*}
-
-
 section {* Parsing Inner Syntax *}
 
-ML{*
-let 
+ML{*let 
   val input = OuterSyntax.scan Position.none "0"
 in 
   OuterParse.prop input
-end 
+end*}
+
+text {* (FIXME funny output for a proposition) *}
+
+section {* Parsing Specifications *}
+
+text {*
+  There are a number of special purpose parsers that help for parsing specifications.
+  For example the function @{ML OuterParse.target} reads a target in order to indicate
+  a locale.
+
+@{ML_response [display,gray]
+"let 
+  val input = filtered_input \"(in test)\"
+in 
+  parse OuterParse.target input 
+end" "(\"test\",[])"}
+  
+  The function @{ML OuterParse.opt_target} makes this parser ``optional''.
+
+  The function @{ML OuterParse.fixes} reads a list of constants
+  which can include a type annotation and a syntax translation.
+  The list needs to be separated by \isacommand{and}.
 
 *}
 
-ML{*
-  OuterParse.opt_target
+text {*
+
+@{ML_response [display,gray]
+"let
+  val input = filtered_input 
+        \"foo::\\\"int \<Rightarrow> bool\\\" (\\\"FOO\\\" [100] 100) and bar::nat and blonk\"
+in
+   parse OuterParse.fixes input
+end"
+"([(foo, SOME \<dots>, Mixfix (\"FOO\",[100],100)), 
+  (bar, SOME \<dots>, NoSyn), 
+  (blonk, NONE, NoSyn)],[])"}  
+
+  The types of the constants is stored in the @{ML SOME}s. 
+  We need to write @{text "\\\"int \<Rightarrow> bool\\\""} to properly
+  escape the type.
+
+  @{ML OuterParse.for_fixes} is an ``optional'' that prefixes 
+  @{ML OuterParse.fixes} with the comman \isacommand{for}.
+*}
+
+ML{*let 
+  val input = filtered_input "test_lemma[intro,foo,elim,dest!,bar]:"
+in 
+  parse (SpecParse.thm_name ":") input 
+     |> fst |> snd |> (Attrib.pretty_attribs @{context}) |> (map Pretty.string_of)
+end*}
+
+text {*
+  (FIXME: why is intro, elim and dest treated differently from bar?) 
 *}
 
-text {* (FIXME funny output for a proposition) *}
+text {*
+@{ML_response [display,gray]
+"let
+  val input = filtered_input
+     (\"even and odd \" ^  
+      \"where \" ^
+      \"  even0[intro]: \\\"even 0\\\" \" ^ 
+      \"| evenS[intro]: \\\"odd n \<Longrightarrow> even (Suc n)\\\" \" ^ 
+      \"| oddS[intro]:  \\\"even n \<Longrightarrow> odd (Suc n)\\\"\")
 
-ML{*
-  OuterParse.opt_target --
-  OuterParse.fixes -- 
-  OuterParse.for_fixes --
-  Scan.optional (OuterParse.$$$ "where" |--
-    OuterParse.!!! (OuterParse.enum1 "|" (SpecParse.opt_thm_name ":" -- OuterParse.prop))) []
-
+  val parser = 
+    OuterParse.opt_target --
+    OuterParse.fixes -- 
+    OuterParse.for_fixes --
+    Scan.optional 
+        (OuterParse.$$$ \"where\" |--
+           OuterParse.!!! 
+             (OuterParse.enum1 \"|\" 
+                (SpecParse.opt_thm_name \":\" -- OuterParse.prop))) []
+in
+  parse parser input
+end"
+"((((NONE, [(even, NONE, NoSyn), (odd, NONE, NoSyn)]), []),
+     [((even0,\<dots>), \"\\^E\\^Ftoken\\^Eeven 0\\^E\\^F\\^E\"),
+      ((evenS,\<dots>), \"\\^E\\^Ftoken\\^Eodd n \<Longrightarrow> even (Suc n)\\^E\\^F\\^E\"),
+      ((oddS,\<dots>), \"\\^E\\^Ftoken\\^Eeven n \<Longrightarrow> odd (Suc n)\\^E\\^F\\^E\")]), [])"}
 *}
 
-ML{* OuterSyntax.command *}
+text {* 
+  The (outer?) parser for the package: returns optionally a locale; 
+  a list of predicate constants with optional type-annotation and 
+  optional syntax-annotation; a list of for-fixes (fixed parameters); 
+  and a list of rules where each rule has optionally a name and an attribute.
+*}
 
 section {* New Commands and Keyword Files *}
 
@@ -575,7 +641,7 @@
   parser producing a top-level transition function (its purpose will also explained
   later). 
 
-  While this is everything we have to do on the ML-level, we need a keyword
+  While this is everything you have to do on the ML-level, you need a keyword
   file that can be loaded by ProofGeneral. This is to enable ProofGeneral to
   recognise \isacommand{foobar} as a command. Such a keyword file can be
   generated with the command-line:
@@ -586,7 +652,7 @@
   will be assigned. In the case above the file will be named @{text
   "isar-keywords-foobar.el"}. This command requires log files to be
   present (in order to extract the keywords from them). To generate these log
-  files, we first package the code above into a separate theory file named
+  files, you first need to package the code above into a separate theory file named
   @{text "Command.thy"}, say---see Figure~\ref{fig:commandtheory} for the
   complete code.
 
@@ -633,7 +699,7 @@
 
   @{text [display] "$ ./build -m \"Pure-ProofGeneral\" \"Pure\""}
 
-  For the theory @{text "Command.thy"}, we first create a ``managed'' subdirectory 
+  For the theory @{text "Command.thy"}, you first need to create a ``managed'' subdirectory 
   with
 
   @{text [display] "$ isabelle mkdir FoobarCommand"}
@@ -647,17 +713,17 @@
 ./FoobarCommand/document/root.tex"}
 
 
-  We need to copy the file @{text "Command.thy"} into the directory @{text "FoobarCommand"}
+  You need to copy the file @{text "Command.thy"} into the directory @{text "FoobarCommand"}
   and add the line 
 
   @{text [display] "use_thy \"Command\";"} 
   
-  to the file @{text "./FoobarCommand/ROOT.ML"}. We can now compile the theory by just typing
+  to the file @{text "./FoobarCommand/ROOT.ML"}. You can now compile the theory by just typing
 
   @{text [display] "$ isabelle make"}
 
-  We created finally all the necessary log files. They are stored 
-  in the directory 
+  If the compilation succeeds, you have finally created all the necessary log files. 
+  They are stored in the directory 
   
   @{text [display]  "~/.isabelle/heaps/Isabelle2008/polyml-5.2.1_x86-linux/log"}
 
@@ -674,7 +740,7 @@
 Pure-ProofGeneral.gz
 HOL-FoobarCommand.gz"} 
 
-  From them we create the keyword files. Assuming the name 
+  From them you can create the keyword files. Assuming the name 
   of the directory is in  @{text "$ISABELLE_LOGS"},
   then the Unix command for creating the keyword file is:
 
@@ -687,14 +753,14 @@
   that @{text "grep foobar"} on this file returns something
   non-empty.}  This keyword file needs to
   be copied into the directory @{text "~/.isabelle/etc"}. To make Isabelle
-  aware of this keyword file, we have to start Isabelle with the option @{text
+  aware of this keyword file, you have to start Isabelle with the option @{text
   "-k foobar"}, i.e.
 
 
   @{text [display] "$ isabelle -k foobar a_theory_file"}
 
-  If we now build a theory on top of @{text "Command.thy"}, 
-  then we can make use of the command \isacommand{foobar}. 
+  If you now build a theory on top of @{text "Command.thy"}, 
+  then the command \isacommand{foobar} can be used. 
   Similarly with any other new command. 
 
 
@@ -710,7 +776,6 @@
   parser @{ML OuterParse.prop}), then prints out the tracing
   information (using a new top-level function @{text trace_top_lvl}) and 
   finally does nothing. For this we can write
-
 *}
 
 ML{*let
@@ -797,7 +862,11 @@
   Similarly for the other function composition combinators.
 
   
-  (FIXME What does @{text "Toplevel.theory"} @{text "Toplevel.print"}?)
+  (FIXME What do @{ML "Toplevel.theory"} 
+  @{ML "Toplevel.print"} 
+  @{ML Toplevel.local_theory}?)
+
+  
 
   (FIXME read a name and show how to store theorems)
 




