--- 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)