isabelle-cookbook: comparison CookBook/Parsing.thy

equal deleted inserted replaced

-:e7519207c2b7
+:19106a9975c1
 Let us now return to our example of parsing @{ML "(p -- q) || r" for p q r}. If we want
 to generate the correct error message for p-followed-by-q, then
 we have to write:
 *}
-ML {*
+ML{*fun p_followed_by_q p q r =
-fun p_followed_by_q p q r =
 let
 val err_msg = (fn _ => p ^ " is not followed by " ^ q)
 in
 ($$ p -- (!! err_msg ($$ q))) || ($$ r -- $$ r)
-end
+end *}
-*}
 text {*
 Running this parser with the @{text [quotes] "h"} and @{text [quotes] "e"}, and
 the input @{text [quotes] "holle"}
 For convenience we define the function
 *}
-ML {*
+ML{*fun filtered_input str =
-fun filtered_input str =
+filter OuterLex.is_proper (OuterSyntax.scan Position.none str) *}
-filter OuterLex.is_proper (OuterSyntax.scan Position.none str)
-*}
 text {*
 If we parse
 The following function will help us later to run examples
 *}
-ML {*
+ML{*fun parse p input = Scan.finite OuterLex.stopper (Scan.error p) input *}
-fun parse p input = Scan.finite OuterLex.stopper (Scan.error p) input
-*}
 text {*
 The function @{ML "OuterParse.!!!"} can be used to force termination of the
 parser in case of a dead end, just like @{ML "Scan.!!"} (see previous section),
 @{ML OuterParse.position}
 *}
-ML {*
+ML{*
 OuterParse.position
 *}
 section {* Parsing Inner Syntax *}
-ML {*
+ML{*
 let
 val input = OuterSyntax.scan Position.none "0"
 in
 OuterParse.prop input
 end
 *}
-ML {*
+ML{*
 OuterParse.opt_target
 *}
 text {* (FIXME funny output for a proposition) *}
-ML {*
+ML{*
 OuterParse.opt_target --
 OuterParse.fixes --
 OuterParse.for_fixes --
 Scan.optional (OuterParse.$$$ "where" |--
 OuterParse.!!! (OuterParse.enum1 "|" (SpecParse.opt_thm_name ":" -- OuterParse.prop))) []
 *}
-ML {* OuterSyntax.command *}
+ML{* OuterSyntax.command *}
 section {* New Commands and Creating Keyword Files *}
 text {*
 Often new commands, for example for providing new definitional principles,
 Let us start with a ``silly'' command, which we call \isacommand{foobar} in what follows.
 To keep things simple this command does nothing at all. On the ML-level it can be defined as
 *}
-ML {*
+ML{*let
-let
 val do_nothing = Scan.succeed (Toplevel.theory I)
 val kind = OuterKeyword.thy_decl
 in
 OuterSyntax.command "foobar" "description of foobar" kind do_nothing
-end
+end *}
-*}
 text {*
 The function @{ML OuterSyntax.command} expects a name for the command, a
 short description, a kind indicator (which we will explain later on more thoroughly) and a
 parser for a top-level transition function (its purpose will also explained
 complete code.
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \begin{figure}[t]
-\begin{boxedminipage}{\textwidth}\small
+\begin{graybox}\small
 \isacommand{theory}~@{text Command}\\
 \isacommand{imports}~@{text Main}\\
 \isacommand{begin}\\
 \isacommand{ML}~\isa{\isacharverbatimopen}\\
 @{ML
 in
 OuterSyntax.command \"foobar\" \"description of foobar\" kind do_nothing
 end"}\\
 \isa{\isacharverbatimclose}\\
 \isacommand{end}
-\end{boxedminipage}
+\end{graybox}
 \caption{The file @{text "Command.thy"} is necessary for generating a log
 file. This log file enables Isabelle to generate a keyword file containing
 the command \isacommand{foobar}.\label{fig:commandtheory}}
 \end{figure}
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 @{text [display] "$ isabelle -k foobar a-theory-file"}
 If we now run the original code
 *}
-ML {*
+ML{*let
-let
 val do_nothing = Scan.succeed (Toplevel.theory I)
 val kind = OuterKeyword.thy_decl
 in
 OuterSyntax.command "foobar" "description of foobar" kind do_nothing
-end
+end *}
-*}
 text {*
 then we can make use of \isacommand{foobar}! Similarly with any other new command.
 In the example above, we built the theories on top of the HOL-logic. If you
 @{ML "Toplevel.theory I"}. We can replace this code by a function that first
 parses a proposition (using the parser @{ML OuterParse.prop}), then prints out
 the tracing information and finally does nothing. For this we can write
 *}
-ML {*
+ML{*let
-let
 val trace_prop =
 OuterParse.prop >> (fn str => (tracing str; (Toplevel.theory I)))
 val kind = OuterKeyword.thy_decl
 in
 OuterSyntax.command "foobar" "traces a proposition" kind trace_prop
-end
+end *}
-*}
 text {*
 Now we can type for example
 @{ML_response_fake_both [display] "foobar \"True \<and> False\"" "True \<and> False"}
 Below we change \isacommand{foobar} is such a way that an proposition as
 argument and then start a proof in order to prove it. Therefore in Line 13
 below, we set the kind indicator to @{ML thy_goal in OuterKeyword}.
 *}
-ML %linenumbers {*let
+ML%linenumbers{*let
 fun set_up_thm str ctxt =
 let
 val prop = Syntax.read_prop ctxt str
 in
 Proof.theorem_i NONE (K I) [[(Syntax.read_prop ctxt str,[])]] ctxt
 Toplevel.local_theory_to_proof NONE (set_up_thm str))
 val kind = OuterKeyword.thy_goal
 in
 OuterSyntax.command "foobar" "proving a proposition" kind prove_prop
-end
+end *}
-*}
 text {*
 The function @{text set_up_thm} takes a string (the proposition) and a context.
 The context is necessary in order to convert the string into a proper proposition
 using the function @{ML Syntax.read_prop}. In Line 6 we use the function
 *}
-ML {*
+ML{*
 val toks = OuterSyntax.scan Position.none
 "theory,imports;begin x.y.z apply ?v1 ?'a 'a -- || 44 simp (* xx *) { * fff * }" ;
 *}
-ML {*
+ML{*
 print_depth 20 ;
 *}
-ML {*
+ML{*
 map OuterLex.text_of toks ;
 *}
-ML {*
+ML{*
 val proper_toks = filter OuterLex.is_proper toks ;
 *}
-ML {*
+ML{*
 map OuterLex.kind_of proper_toks
 *}
-ML {*
+ML{*
 map OuterLex.unparse proper_toks ;
 *}
-ML {*
+ML{*
 OuterLex.stopper
 *}
 text {*

changeset 69	19106a9975c1
parent 68	e7519207c2b7
child 72	7b8c4fe235aa