--- 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 \<and> True"})) #> snd *}
+ ((@{binding "TrueConj_def"}, []), @{term "True \<and> True"})) #> snd *}
text {*
Now querying the definition you obtain:
--- 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));
*}
--- 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*}
--- 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
--- 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
--- 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;
--- 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 "\<verbclose>"}\\
\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*}
(*
Binary file progtutorial.pdf has changed