# HG changeset patch # User Christian Urban # Date 1332236384 0 # Node ID 7e25716c374493e02e3d8b9a839bef4efc217fdf # Parent f223f8223d4a5a15280a16e3c194ef4ec3c5b90e updated to outer syntax / parser changes diff -r f223f8223d4a -r 7e25716c3744 ProgTutorial/Advanced.thy --- a/ProgTutorial/Advanced.thy Sun Feb 19 01:33:47 2012 +0000 +++ b/ProgTutorial/Advanced.thy Tue Mar 20 09:39:44 2012 +0000 @@ -657,7 +657,7 @@ local_setup %gray {* Local_Theory.define ((@{binding "TrueConj"}, NoSyn), - (Attrib.empty_binding, @{term "True \ True"})) #> snd *} + ((@{binding "TrueConj_def"}, []), @{term "True \ True"})) #> snd *} text {* Now querying the definition you obtain: diff -r f223f8223d4a -r 7e25716c3744 ProgTutorial/Base.thy --- a/ProgTutorial/Base.thy Sun Feb 19 01:33:47 2012 +0000 +++ b/ProgTutorial/Base.thy Tue Mar 20 09:39:44 2012 +0000 @@ -1,6 +1,9 @@ theory Base imports Main "~~/src/HOL/Library/LaTeXsugar" +keywords "ML" "setup" "local_setup" :: thy_decl and + "ML_prf" :: prf_decl and + "ML_val" :: diag uses ("output_tutorial.ML") ("antiquote_setup.ML") @@ -92,8 +95,7 @@ ML {* val _ = - Outer_Syntax.command "ML" "eval ML text within theory" - (Keyword.tag "TutorialML" Keyword.thy_decl) + Outer_Syntax.command ("ML", Keyword.tag "TutorialML" Keyword.thy_decl) "eval ML text within theory" (Parse.position Parse.text >> (fn (txt, pos) => Toplevel.generic_theory @@ -104,8 +106,7 @@ ML {* val _ = - Outer_Syntax.command "ML_prf" "ML text within proof" - (Keyword.tag "TutorialMLprf" Keyword.prf_decl) + Outer_Syntax.command ("ML_prf", Keyword.tag "TutorialMLprf" Keyword.prf_decl) "ML text within proof" (Parse.ML_source >> (fn (txt, pos) => Toplevel.proof (Proof.map_context (Context.proof_map (ML_Context.exec (fn () => ML_Context.eval_text true pos txt))) #> propagate_env_prf))) @@ -113,23 +114,20 @@ ML {* val _ = - Outer_Syntax.command "ML_val" "diagnostic ML text" - (Keyword.tag "TutorialML" Keyword.diag) + Outer_Syntax.command ("ML_val", Keyword.tag "TutorialML" Keyword.diag) "diagnostic ML text" (Parse.ML_source >> Isar_Cmd.ml_diag true) *} ML {* val _ = - Outer_Syntax.command "setup" "ML theory setup" - (Keyword.tag_ml Keyword.thy_decl) + Outer_Syntax.command ("setup", Keyword.tag_ml Keyword.thy_decl) "ML theory setup" (Parse.ML_source >> (fn (txt, pos) => (Toplevel.theory (Isar_Cmd.global_setup (txt, pos) #> write_file_setup_blk txt)))) *} ML {* val _ = - Outer_Syntax.local_theory "local_setup" "ML local theory setup" - (Keyword.tag_ml Keyword.thy_decl) + Outer_Syntax.local_theory ("local_setup", Keyword.tag_ml Keyword.thy_decl) "ML local theory setup" (Parse.ML_source >> (fn (txt, pos) => Isar_Cmd.local_setup (txt, pos) #> write_file_lsetup_blk txt)); *} diff -r f223f8223d4a -r 7e25716c3744 ProgTutorial/Helper/Command/Command.thy --- a/ProgTutorial/Helper/Command/Command.thy Sun Feb 19 01:33:47 2012 +0000 +++ b/ProgTutorial/Helper/Command/Command.thy Tue Mar 20 09:39:44 2012 +0000 @@ -1,5 +1,7 @@ theory Command imports Main +keywords "foobar" "foobar_trace" :: thy_decl and + "foobar_goal" "foobar_prove" :: thy_goal begin ML {* @@ -7,7 +9,7 @@ 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 *} @@ -18,8 +20,8 @@ val trace_prop_parser = Parse.prop >> trace_prop val kind = Keyword.thy_decl in - Outer_Syntax.local_theory "foobar_trace" "traces a proposition" - kind trace_prop_parser + Outer_Syntax.local_theory ("foobar_trace", kind) "traces a proposition" + trace_prop_parser end *} @@ -34,8 +36,8 @@ val prove_prop_parser = Parse.prop >> prove_prop val kind = Keyword.thy_goal in - Outer_Syntax.local_theory_to_proof "foobar_goal" "proving a proposition" - kind prove_prop_parser + Outer_Syntax.local_theory_to_proof ("foobar_goal", kind) "proving a proposition" + prove_prop_parser end *} @@ -62,8 +64,8 @@ val parser = Parse_Spec.opt_thm_name ":" -- Parse.ML_source in - Outer_Syntax.local_theory_to_proof "foobar_prove" "proving a proposition" - Keyword.thy_goal (parser >> setup_proof) + Outer_Syntax.local_theory_to_proof ("foobar_prove", Keyword.thy_goal) "proving a proposition" + (parser >> setup_proof) end*} diff -r f223f8223d4a -r 7e25716c3744 ProgTutorial/Package/Ind_Interface.thy --- a/ProgTutorial/Package/Ind_Interface.thy Sun Feb 19 01:33:47 2012 +0000 +++ b/ProgTutorial/Package/Ind_Interface.thy Tue Mar 20 09:39:44 2012 +0000 @@ -1,5 +1,6 @@ theory Ind_Interface imports Ind_Intro Simple_Inductive_Package +keywords "simple_inductive2" :: thy_decl begin section {* Parsing and Typing the Specification\label{sec:interface} *} @@ -133,9 +134,9 @@ spec_parser >> (fn (pred_specs, rule_specs) => add_inductive_cmd pred_specs rule_specs) -val _ = Outer_Syntax.local_theory "simple_inductive2" +val _ = Outer_Syntax.local_theory ("simple_inductive2", Keyword.thy_decl) "definition of simple inductive predicates" - Keyword.thy_decl specification*} + specification*} text {* We call @{ML_ind local_theory in Outer_Syntax} with the kind-indicator diff -r f223f8223d4a -r 7e25716c3744 ProgTutorial/Package/Simple_Inductive_Package.thy --- a/ProgTutorial/Package/Simple_Inductive_Package.thy Sun Feb 19 01:33:47 2012 +0000 +++ b/ProgTutorial/Package/Simple_Inductive_Package.thy Tue Mar 20 09:39:44 2012 +0000 @@ -1,5 +1,6 @@ theory Simple_Inductive_Package imports Main "../Base" +keywords "simple_inductive" :: thy_decl uses "simple_inductive_package.ML" begin diff -r f223f8223d4a -r 7e25716c3744 ProgTutorial/Package/simple_inductive_package.ML --- a/ProgTutorial/Package/simple_inductive_package.ML Sun Feb 19 01:33:47 2012 +0000 +++ b/ProgTutorial/Package/simple_inductive_package.ML Tue Mar 20 09:39:44 2012 +0000 @@ -21,7 +21,7 @@ (* @chunk make_definitions *) fun make_defs ((binding, syn), trm) lthy = let - val arg = ((binding, syn), (Attrib.empty_binding, trm)) + val arg = ((binding, syn), ((Binding.suffix_name "_def" binding, []), trm)) val ((_, (_ , thm)), lthy) = Local_Theory.define arg lthy in (thm, lthy) @@ -236,8 +236,8 @@ (fn (((loc, preds), params), specs) => Toplevel.local_theory loc (add_inductive preds params specs)) -val _ = Outer_Syntax.command "simple_inductive" "define inductive predicates" - Keyword.thy_decl specification +val _ = Outer_Syntax.command ("simple_inductive", Keyword.thy_decl) "define inductive predicates" + specification (* @end *) end; diff -r f223f8223d4a -r 7e25716c3744 ProgTutorial/Parsing.thy --- a/ProgTutorial/Parsing.thy Sun Feb 19 01:33:47 2012 +0000 +++ b/ProgTutorial/Parsing.thy Tue Mar 20 09:39:44 2012 +0000 @@ -475,6 +475,9 @@ 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}. @@ -506,10 +509,10 @@ 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 @@ -960,7 +963,7 @@ 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 {* @@ -997,7 +1000,7 @@ 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 "\"}\\ \isacommand{end} @@ -1098,10 +1101,10 @@ 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 @@ -1124,8 +1127,8 @@ val kind = Keyword.thy_decl in - Outer_Syntax.local_theory "foobar_trace" "traces a proposition" - kind (Parse.prop >> trace_prop) + Outer_Syntax.local_theory ("foobar_trace", kind) "traces a proposition" + (Parse.prop >> trace_prop) end *} text {* @@ -1166,8 +1169,8 @@ val kind = Keyword.thy_goal in - Outer_Syntax.local_theory_to_proof "foobar_goal" "proves a proposition" - kind (Parse.prop >> goal_prop) + Outer_Syntax.local_theory_to_proof ("foobar_goal", kind) "proves a proposition" + (Parse.prop >> goal_prop) end *} text {* @@ -1225,8 +1228,9 @@ val parser = Parse_Spec.opt_thm_name ":" -- Parse.ML_source in - Outer_Syntax.local_theory_to_proof "foobar_prove" "proving a proposition" - Keyword.thy_goal (parser >> setup_proof) + Outer_Syntax.local_theory_to_proof ("foobar_prove", Keyword.thy_goal) + "proving a proposition" + (parser >> setup_proof) end*} (* diff -r f223f8223d4a -r 7e25716c3744 progtutorial.pdf Binary file progtutorial.pdf has changed