isabelle-cookbook: comparison ProgTutorial/Parsing.thy

equal deleted inserted replaced

-:fb6c29a90003
+:d8c376662bb4
 theory Parsing
 imports Base "Helper/Command/Command" "Package/Simple_Inductive_Package"
 begin
-(*<*)
-setup {*
-open_file_with_prelude
-"Parsing_Code.thy"
-["theory Parsing",
-"imports Base \"Package/Simple_Inductive_Package\"",
-"begin"]
-*}
-(*>*)
 chapter {* Parsing\label{chp:parsing} *}
 text {*
 \begin{flushright}
 Let us now return to our example of parsing @{ML "(p -- q) || r" for p q
 r}. If you want to generate the correct error message for failure
 of parsing @{text "p"}-followed-by-@{text "q"}, then you have to write:
 *}
-ML{*fun p_followed_by_q p q r =
+ML %grayML{*fun p_followed_by_q p q r =
 let
 val err_msg = fn _ => p ^ " is not followed by " ^ q
 in
 ($$ p -- (!! (fn _ => err_msg) ($$ q))) || ($$ r -- $$ r)
 end *}
 the tree corresponding to the string @{text [quotes] "(A, A), (A, A)"} where
 the @{text "A"}s will be the leaves.  We assume the trees are represented by the
 datatype:
 *}
-ML{*datatype tree =
+ML %grayML{*datatype tree =
 Lf of string
 | Br of tree * tree*}
 text {*
 Since nested parentheses should be treated in a meaningful way---for example
 the string @{text [quotes] "((A))"} should be read into a single
 leaf---you might implement the following parser.
 *}
-ML{*fun parse_basic s =
+ML %grayML{*fun parse_basic s =
 $$ s >> Lf || $$ "(" |-- parse_tree s --| $$ ")"
 and parse_tree s =
 parse_basic s --| $$ "," -- parse_tree s >> Br || parse_basic s*}
 parser until an input is given. This can be done by adding the parsed
 string as an explicit argument. So the parser above should be implemented
 as follows.
 *}
-ML{*fun parse_basic s xs =
+ML %grayML{*fun parse_basic s xs =
 ($$ s >> Lf || $$ "(" |-- parse_tree s --| $$ ")") xs
 and parse_tree s xs =
 (parse_basic s --| $$ "," -- parse_tree s >> Br || parse_basic s) xs*}
 text {*
 Most of the time, however, Isabelle developers have to deal with parsing
 tokens, not strings.  These token parsers have the type:
 *}
-ML{*type 'a parser = Token.T list -> 'a * Token.T list*}
+ML %grayML{*type 'a parser = Token.T list -> 'a * Token.T list*}
 text {*
 {\bf REDO!!}
 We can easily change what is recognised as a keyword with the function
 @{ML_ind define in Keyword}. For example calling it with
 *}
-ML{*val _ = Keyword.define ("hello", NONE) *}
+ML %grayML{*val _ = Keyword.define ("hello", NONE) *}
 text {*
 then lexing @{text [quotes] "hello world"} will produce
 @{ML_response_fake [display,gray] "Outer_Syntax.scan Position.none \"hello world\""
 "[Token (\<dots>,(Ident, \"hello\"), \<dots>), Token (\<dots>,(Ident, \"world\"), \<dots>)]"}
 For convenience we define the function:
 *}
-ML{*fun filtered_input str =
+ML %grayML{*fun filtered_input str =
 filter Token.is_proper (Outer_Syntax.scan Position.none str) *}
 text {*
 If you now parse
 "([\"in\", \"in\", \"in\"], [])"}
 The following function will help to run examples.
 *}
-ML{*fun parse p input = Scan.finite Token.stopper (Scan.error p) input *}
+ML %grayML{*fun parse p input = Scan.finite Token.stopper (Scan.error p) input *}
 text {*
 The function @{ML_ind "!!!" in Parse} can be used to force termination
 of the parser in case of a dead end, just like @{ML "Scan.!!"} (see previous
 section). A difference, however, is that the error message of @{ML
 occurred. For this Isabelle can attach positional information to tokens
 and then thread this information up the ``processing chain''. To see this,
 modify the function @{ML filtered_input}, described earlier, as follows
 *}
-ML{*fun filtered_input' str =
+ML %grayML{*fun filtered_input' str =
 filter Token.is_proper (Outer_Syntax.scan (Position.line 7) str) *}
 text {*
 where we pretend the parsed string starts on line 7. An example is
 To keep things simple, let us start with a ``silly'' command that does nothing
 at all. We shall name this command \isacommand{foobar}. On the ML-level it can be
 defined as:
 *}
-ML{*let
+ML %grayML{*let
 val do_nothing = Scan.succeed (Local_Theory.background_theory I)
 val kind = Keyword.thy_decl
 in
 Outer_Syntax.local_theory ("foobar", kind) "description of foobar" do_nothing
 end *}
 to interact with ProofGeneral. A similar procedure has to be done with any
 other new command, and also any new keyword that is introduced with
 the function @{ML_ind define in Keyword}. For example:
 *}
-ML{*val _ = Keyword.define ("blink", NONE) *}
+ML %grayML{*val _ = Keyword.define ("blink", NONE) *}
 text {*
 At the moment the command \isacommand{foobar} is not very useful. Let us
 refine it a bit next by letting it take a proposition as argument and
 printing this proposition inside the tracing buffer.
 parser @{ML Parse.prop}), then prints out the tracing
 information (using a new function @{text trace_prop}) and
 finally does nothing. For this you can write:
 *}
-ML{*let
+ML %grayML{*let
 fun trace_prop str =
 Local_Theory.background_theory (fn ctxt => (tracing str; ctxt))
 val kind = Keyword.thy_decl
 in
 fun init thy () = error "Result")
 val result_cookie = (Result.get, Result.put, "Result.put")
 *}
-ML{*let
+ML %grayML{*let
 fun after_qed thm_name thms lthy =
 Local_Theory.note (thm_name, (flat thms)) lthy |> snd
 fun setup_proof (thm_name, (txt, pos)) lthy =
 let

changeset 517	d8c376662bb4
parent 514	7e25716c3744
child 519	cf471fa86091