isabelle-cookbook: comparison ProgTutorial/Parsing.thy

equal deleted inserted replaced

-:f223f8223d4a
+:7e25716c3744
 *}
 ML{*type 'a parser = Token.T list -> 'a * Token.T list*}
 text {*
+{\bf REDO!!}
 The reason for using token parsers is that theory syntax, as well as the
 parsers for the arguments of proof methods, use the type @{ML_type
 Token.T}.
 \begin{readmore}
 produces three tokens where the first and the last are identifiers, since
 @{text [quotes] "hello"} and @{text [quotes] "world"} do not match any
 other syntactic category. The second indicates a space.
 We can easily change what is recognised as a keyword with the function
-@{ML_ind keyword in Keyword}. For example calling it with
+@{ML_ind define in Keyword}. For example calling it with
 *}
-ML{*val _ = Keyword.keyword "hello"*}
+ML{*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\""
 ML{*let
 val do_nothing = Scan.succeed (Local_Theory.background_theory I)
 val kind = Keyword.thy_decl
 in
-Outer_Syntax.local_theory "foobar" "description of foobar" kind do_nothing
+Outer_Syntax.local_theory ("foobar", kind) "description of foobar" do_nothing
 end *}
 text {*
 The crucial function @{ML_ind local_theory in Outer_Syntax} expects a name for the command, a
 short description, a kind indicator (which we will explain later more thoroughly) and a
 @{ML
 "let
 val do_nothing = Scan.succeed (Local_Theory.background_theory I)
 val kind = Keyword.thy_decl
 in
-Outer_Syntax.local_theory \"foobar\" \"description of foobar\" kind do_nothing
+Outer_Syntax.local_theory (\"foobar\", kind) \"description of foobar\" do_nothing
 end"}\\
 @{text "\<verbclose>"}\\
 \isacommand{end}
 \end{graybox}
 \caption{This file can be used to generate a log file. This log file in turn can
 text {*
 but you will not see any action as we chose to implement this command to do
 nothing. The point of this command is only to show the procedure of how
 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 keyword in Keyword}. For example:
+the function @{ML_ind define in Keyword}. For example:
 *}
-ML{*val _ = Keyword.keyword "blink" *}
+ML{*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.
 fun trace_prop str =
 Local_Theory.background_theory (fn ctxt => (tracing str; ctxt))
 val kind = Keyword.thy_decl
 in
-Outer_Syntax.local_theory "foobar_trace" "traces a proposition"
+Outer_Syntax.local_theory ("foobar_trace", kind) "traces a proposition"
-kind (Parse.prop >> trace_prop)
+(Parse.prop >> trace_prop)
 end *}
 text {*
 The command is now \isacommand{foobar\_trace} and can be used to
 see the proposition in the tracing buffer.
 Proof.theorem NONE (K I) [[(prop, [])]] lthy
 end
 val kind = Keyword.thy_goal
 in
-Outer_Syntax.local_theory_to_proof "foobar_goal" "proves a proposition"
+Outer_Syntax.local_theory_to_proof ("foobar_goal", kind) "proves a proposition"
-kind (Parse.prop >> goal_prop)
+(Parse.prop >> goal_prop)
 end *}
 text {*
 The function @{text goal_prop} in Lines 2 to 7 takes a string (the proposition to be
 proved) and a context as argument.  The context is necessary in order to be able to use
 end
 val parser = Parse_Spec.opt_thm_name ":" -- Parse.ML_source
 in
-Outer_Syntax.local_theory_to_proof "foobar_prove" "proving a proposition"
+Outer_Syntax.local_theory_to_proof ("foobar_prove", Keyword.thy_goal)
-Keyword.thy_goal (parser >> setup_proof)
+"proving a proposition"
+(parser >> setup_proof)
 end*}
 (*
 foobar_prove test: {* @{prop "True"} *}
 apply(rule TrueI)

changeset 514	7e25716c3744
parent 473	fea1b7ce5c4a
child 517	d8c376662bb4