--- a/etc/isar-keywords-ZF.el Mon Feb 25 20:11:42 2013 +0100
+++ b/etc/isar-keywords-ZF.el Mon Feb 25 20:55:48 2013 +0100
@@ -270,6 +270,7 @@
"kill"
"kill_thy"
"linear_undo"
+ "pretty_setmargin"
"quit"
"remove_thy"
"undo"
@@ -289,7 +290,6 @@
"help"
"locale_deps"
"pr"
- "pretty_setmargin"
"prf"
"print_abbrevs"
"print_antiquotations"
--- a/etc/isar-keywords.el Mon Feb 25 20:11:42 2013 +0100
+++ b/etc/isar-keywords.el Mon Feb 25 20:55:48 2013 +0100
@@ -367,6 +367,7 @@
"kill"
"kill_thy"
"linear_undo"
+ "pretty_setmargin"
"quit"
"remove_thy"
"undo"
@@ -382,7 +383,6 @@
"code_deps"
"code_thms"
"display_drafts"
- "export_code"
"find_consts"
"find_theorems"
"find_unused_assms"
@@ -392,7 +392,6 @@
"locale_deps"
"nitpick"
"pr"
- "pretty_setmargin"
"prf"
"print_abbrevs"
"print_antiquotations"
@@ -510,6 +509,7 @@
"domain_isomorphism"
"domaindef"
"equivariance"
+ "export_code"
"extract"
"extract_type"
"fixrec"
--- a/lib/scripts/keywords Mon Feb 25 20:11:42 2013 +0100
+++ b/lib/scripts/keywords Mon Feb 25 20:55:48 2013 +0100
@@ -41,7 +41,6 @@
"thy_decl" => "theory-decl",
"thy_script" => "theory-script",
"thy_goal" => "theory-goal",
- "thy_schematic_goal" => "theory-goal",
"qed_block" => "qed-block",
"qed_global" => "qed-global",
"prf_heading2" => "proof-heading",
--- a/src/HOL/Decision_Procs/Cooper.thy Mon Feb 25 20:11:42 2013 +0100
+++ b/src/HOL/Decision_Procs/Cooper.thy Mon Feb 25 20:55:48 2013 +0100
@@ -1994,7 +1994,7 @@
pa (E (A (Imp (Ge (Sub (Bound 0) (Bound 1)))
(E (E (Eq (Sub (Add (Mul 3 (Bound 1)) (Mul 5 (Bound 0))) (Bound 2))))))))"
-ML {* @{code cooper_test} () *}
+ML_val {* @{code cooper_test} () *}
(*code_reflect Cooper_Procedure
functions pa
--- a/src/HOL/Decision_Procs/Ferrack.thy Mon Feb 25 20:11:42 2013 +0100
+++ b/src/HOL/Decision_Procs/Ferrack.thy Mon Feb 25 20:55:48 2013 +0100
@@ -1917,7 +1917,7 @@
"ferrack_test u = linrqe (A (A (Imp (Lt (Sub (Bound 1) (Bound 0)))
(E (Eq (Sub (Add (Bound 0) (Bound 2)) (Bound 1)))))))"
-ML {* @{code ferrack_test} () *}
+ML_val {* @{code ferrack_test} () *}
oracle linr_oracle = {*
let
--- a/src/HOL/Decision_Procs/MIR.thy Mon Feb 25 20:11:42 2013 +0100
+++ b/src/HOL/Decision_Procs/MIR.thy Mon Feb 25 20:55:48 2013 +0100
@@ -5502,17 +5502,15 @@
definition
"problem4 = E (And (Ge (Sub (Bound 1) (Bound 0))) (Eq (Add (Floor (Bound 1)) (Floor (Neg (Bound 0))))))"
-ML {*
- Par_List.map (fn e => e ())
- [fn () => @{code mircfrqe} @{code problem1},
- fn () => @{code mirlfrqe} @{code problem1},
- fn () => @{code mircfrqe} @{code problem2},
- fn () => @{code mirlfrqe} @{code problem2},
- fn () => @{code mircfrqe} @{code problem3},
- fn () => @{code mirlfrqe} @{code problem3},
- fn () => @{code mircfrqe} @{code problem4},
- fn () => @{code mirlfrqe} @{code problem4}]
-*}
+ML_val {* @{code mircfrqe} @{code problem1} *}
+ML_val {* @{code mirlfrqe} @{code problem1} *}
+ML_val {* @{code mircfrqe} @{code problem2} *}
+ML_val {* @{code mirlfrqe} @{code problem2} *}
+ML_val {* @{code mircfrqe} @{code problem3} *}
+ML_val {* @{code mirlfrqe} @{code problem3} *}
+ML_val {* @{code mircfrqe} @{code problem4} *}
+ML_val {* @{code mirlfrqe} @{code problem4} *}
+
(*code_reflect Mir
functions mircfrqe mirlfrqe
--- a/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy Mon Feb 25 20:11:42 2013 +0100
+++ b/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy Mon Feb 25 20:55:48 2013 +0100
@@ -662,7 +662,7 @@
qsort a
}"
-ML {* @{code example} () *}
+ML_val {* @{code example} () *}
export_code qsort checking SML SML_imp OCaml? OCaml_imp? Haskell? Scala Scala_imp
--- a/src/HOL/Imperative_HOL/ex/Linked_Lists.thy Mon Feb 25 20:11:42 2013 +0100
+++ b/src/HOL/Imperative_HOL/ex/Linked_Lists.thy Mon Feb 25 20:55:48 2013 +0100
@@ -996,9 +996,9 @@
code_reserved SML upto
-ML {* @{code test_1} () *}
-ML {* @{code test_2} () *}
-ML {* @{code test_3} () *}
+ML_val {* @{code test_1} () *}
+ML_val {* @{code test_2} () *}
+ML_val {* @{code test_3} () *}
export_code test_1 test_2 test_3 checking SML SML_imp OCaml? OCaml_imp? Haskell? Scala Scala_imp
--- a/src/HOL/List.thy Mon Feb 25 20:11:42 2013 +0100
+++ b/src/HOL/List.thy Mon Feb 25 20:55:48 2013 +0100
@@ -444,7 +444,7 @@
in [(@{syntax_const "_listcompr"}, lc_tr)] end
*}
-ML {*
+ML_val {*
let
val read = Syntax.read_term @{context};
fun check s1 s2 = read s1 aconv read s2 orelse error ("Check failed: " ^ quote s1);
--- a/src/HOL/MicroJava/BV/BVExample.thy Mon Feb 25 20:11:42 2013 +0100
+++ b/src/HOL/MicroJava/BV/BVExample.thy Mon Feb 25 20:55:48 2013 +0100
@@ -480,7 +480,7 @@
definition test2 where
"test2 = test_kil E test_name [] (PrimT Void) 3 2 [] make_list_ins"
-ML {*
+ML_val {*
@{code test1};
@{code test2};
*}
--- a/src/HOL/MicroJava/J/JListExample.thy Mon Feb 25 20:11:42 2013 +0100
+++ b/src/HOL/MicroJava/J/JListExample.thy Mon Feb 25 20:55:48 2013 +0100
@@ -151,7 +151,7 @@
"test = exec_i_i_i_o example_prg (Norm (empty, empty)) E"
by(auto intro: exec_i_i_i_oI intro!: pred_eqI elim: exec_i_i_i_oE simp add: test_def)
-ML {*
+ML_val {*
val SOME ((_, (heap, locs)), _) = Predicate.yield @{code test};
locs @{code l1_name};
locs @{code l2_name};
--- a/src/HOL/MicroJava/JVM/JVMListExample.thy Mon Feb 25 20:11:42 2013 +0100
+++ b/src/HOL/MicroJava/JVM/JVMListExample.thy Mon Feb 25 20:55:48 2013 +0100
@@ -136,7 +136,7 @@
definition
"test = exec (E, start_state E test_name makelist_name)"
-ML {*
+ML_val {*
@{code test};
@{code exec} (@{code E}, @{code the} it);
@{code exec} (@{code E}, @{code the} it);
--- a/src/HOL/Nitpick_Examples/Mini_Nits.thy Mon Feb 25 20:11:42 2013 +0100
+++ b/src/HOL/Nitpick_Examples/Mini_Nits.thy Mon Feb 25 20:55:48 2013 +0100
@@ -25,88 +25,88 @@
val unknown = expect "unknown"
*}
-ML {* genuine 1 @{prop "x = Not"} *}
-ML {* none 1 @{prop "\<exists>x. x = Not"} *}
-ML {* none 1 @{prop "\<not> False"} *}
-ML {* genuine 1 @{prop "\<not> True"} *}
-ML {* none 1 @{prop "\<not> \<not> b \<longleftrightarrow> b"} *}
-ML {* none 1 @{prop True} *}
-ML {* genuine 1 @{prop False} *}
-ML {* genuine 1 @{prop "True \<longleftrightarrow> False"} *}
-ML {* none 1 @{prop "True \<longleftrightarrow> \<not> False"} *}
-ML {* none 5 @{prop "\<forall>x. x = x"} *}
-ML {* none 5 @{prop "\<exists>x. x = x"} *}
-ML {* none 1 @{prop "\<forall>x. x = y"} *}
-ML {* genuine 2 @{prop "\<forall>x. x = y"} *}
-ML {* none 2 @{prop "\<exists>x. x = y"} *}
-ML {* none 2 @{prop "\<forall>x\<Colon>'a \<times> 'a. x = x"} *}
-ML {* none 2 @{prop "\<exists>x\<Colon>'a \<times> 'a. x = y"} *}
-ML {* genuine 2 @{prop "\<forall>x\<Colon>'a \<times> 'a. x = y"} *}
-ML {* none 2 @{prop "\<exists>x\<Colon>'a \<times> 'a. x = y"} *}
-ML {* none 1 @{prop "All = Ex"} *}
-ML {* genuine 2 @{prop "All = Ex"} *}
-ML {* none 1 @{prop "All P = Ex P"} *}
-ML {* genuine 2 @{prop "All P = Ex P"} *}
-ML {* none 5 @{prop "x = y \<longrightarrow> P x = P y"} *}
-ML {* none 5 @{prop "(x\<Colon>'a \<times> 'a) = y \<longrightarrow> P x = P y"} *}
-ML {* none 2 @{prop "(x\<Colon>'a \<times> 'a) = y \<longrightarrow> P x y = P y x"} *}
-ML {* none 5 @{prop "\<exists>x\<Colon>'a \<times> 'a. x = y \<longrightarrow> P x = P y"} *}
-ML {* none 2 @{prop "(x\<Colon>'a \<Rightarrow> 'a) = y \<longrightarrow> P x = P y"} *}
-ML {* none 2 @{prop "\<exists>x\<Colon>'a \<Rightarrow> 'a. x = y \<longrightarrow> P x = P y"} *}
-ML {* genuine 1 @{prop "(op =) X = Ex"} *}
-ML {* none 2 @{prop "\<forall>x::'a \<Rightarrow> 'a. x = x"} *}
-ML {* none 1 @{prop "x = y"} *}
-ML {* genuine 1 @{prop "x \<longleftrightarrow> y"} *}
-ML {* genuine 2 @{prop "x = y"} *}
-ML {* genuine 1 @{prop "X \<subseteq> Y"} *}
-ML {* none 1 @{prop "P \<and> Q \<longleftrightarrow> Q \<and> P"} *}
-ML {* none 1 @{prop "P \<and> Q \<longrightarrow> P"} *}
-ML {* none 1 @{prop "P \<or> Q \<longleftrightarrow> Q \<or> P"} *}
-ML {* genuine 1 @{prop "P \<or> Q \<longrightarrow> P"} *}
-ML {* none 1 @{prop "(P \<longrightarrow> Q) \<longleftrightarrow> (\<not> P \<or> Q)"} *}
-ML {* none 5 @{prop "{a} = {a, a}"} *}
-ML {* genuine 2 @{prop "{a} = {a, b}"} *}
-ML {* genuine 1 @{prop "{a} \<noteq> {a, b}"} *}
-ML {* none 5 @{prop "{}\<^sup>+ = {}"} *}
-ML {* none 5 @{prop "UNIV\<^sup>+ = UNIV"} *}
-ML {* none 5 @{prop "(UNIV \<Colon> ('a \<times> 'b) set) - {} = UNIV"} *}
-ML {* none 5 @{prop "{} - (UNIV \<Colon> ('a \<times> 'b) set) = {}"} *}
-ML {* none 1 @{prop "{(a, b), (b, c)}\<^sup>+ = {(a, b), (a, c), (b, c)}"} *}
-ML {* genuine 2 @{prop "{(a, b), (b, c)}\<^sup>+ = {(a, b), (a, c), (b, c)}"} *}
-ML {* none 5 @{prop "a \<noteq> c \<Longrightarrow> {(a, b), (b, c)}\<^sup>+ = {(a, b), (a, c), (b, c)}"} *}
-ML {* none 5 @{prop "A \<union> B = {x. x \<in> A \<or> x \<in> B}"} *}
-ML {* none 5 @{prop "A \<inter> B = {x. x \<in> A \<and> x \<in> B}"} *}
-ML {* none 5 @{prop "A - B = (\<lambda>x. A x \<and> \<not> B x)"} *}
-ML {* none 5 @{prop "\<exists>a b. (a, b) = (b, a)"} *}
-ML {* genuine 2 @{prop "(a, b) = (b, a)"} *}
-ML {* genuine 2 @{prop "(a, b) \<noteq> (b, a)"} *}
-ML {* none 5 @{prop "\<exists>a b\<Colon>'a \<times> 'a. (a, b) = (b, a)"} *}
-ML {* genuine 2 @{prop "(a\<Colon>'a \<times> 'a, b) = (b, a)"} *}
-ML {* none 5 @{prop "\<exists>a b\<Colon>'a \<times> 'a \<times> 'a. (a, b) = (b, a)"} *}
-ML {* genuine 2 @{prop "(a\<Colon>'a \<times> 'a \<times> 'a, b) \<noteq> (b, a)"} *}
-ML {* none 5 @{prop "\<exists>a b\<Colon>'a \<Rightarrow> 'a. (a, b) = (b, a)"} *}
-ML {* genuine 1 @{prop "(a\<Colon>'a \<Rightarrow> 'a, b) \<noteq> (b, a)"} *}
-ML {* none 5 @{prop "fst (a, b) = a"} *}
-ML {* none 1 @{prop "fst (a, b) = b"} *}
-ML {* genuine 2 @{prop "fst (a, b) = b"} *}
-ML {* genuine 2 @{prop "fst (a, b) \<noteq> b"} *}
-ML {* genuine 2 @{prop "f ((x, z), y) = (x, z)"} *}
-ML {* none 2 @{prop "(ALL x. f x = fst x) \<longrightarrow> f ((x, z), y) = (x, z)"} *}
-ML {* none 5 @{prop "snd (a, b) = b"} *}
-ML {* none 1 @{prop "snd (a, b) = a"} *}
-ML {* genuine 2 @{prop "snd (a, b) = a"} *}
-ML {* genuine 2 @{prop "snd (a, b) \<noteq> a"} *}
-ML {* genuine 1 @{prop P} *}
-ML {* genuine 1 @{prop "(\<lambda>x. P) a"} *}
-ML {* genuine 1 @{prop "(\<lambda>x y z. P y x z) a b c"} *}
-ML {* none 5 @{prop "\<exists>f. f = (\<lambda>x. x) \<and> f y = y"} *}
-ML {* genuine 1 @{prop "\<exists>f. f p \<noteq> p \<and> (\<forall>a b. f (a, b) = (a, b))"} *}
-ML {* none 2 @{prop "\<exists>f. \<forall>a b. f (a, b) = (a, b)"} *}
-ML {* none 3 @{prop "f = (\<lambda>a b. (b, a)) \<longrightarrow> f x y = (y, x)"} *}
-ML {* genuine 2 @{prop "f = (\<lambda>a b. (b, a)) \<longrightarrow> f x y = (x, y)"} *}
-ML {* none 5 @{prop "f = (\<lambda>x. f x)"} *}
-ML {* none 5 @{prop "f = (\<lambda>x. f x\<Colon>'a \<Rightarrow> bool)"} *}
-ML {* none 5 @{prop "f = (\<lambda>x y. f x y)"} *}
-ML {* none 5 @{prop "f = (\<lambda>x y. f x y\<Colon>'a \<Rightarrow> bool)"} *}
+ML_val {* genuine 1 @{prop "x = Not"} *}
+ML_val {* none 1 @{prop "\<exists>x. x = Not"} *}
+ML_val {* none 1 @{prop "\<not> False"} *}
+ML_val {* genuine 1 @{prop "\<not> True"} *}
+ML_val {* none 1 @{prop "\<not> \<not> b \<longleftrightarrow> b"} *}
+ML_val {* none 1 @{prop True} *}
+ML_val {* genuine 1 @{prop False} *}
+ML_val {* genuine 1 @{prop "True \<longleftrightarrow> False"} *}
+ML_val {* none 1 @{prop "True \<longleftrightarrow> \<not> False"} *}
+ML_val {* none 5 @{prop "\<forall>x. x = x"} *}
+ML_val {* none 5 @{prop "\<exists>x. x = x"} *}
+ML_val {* none 1 @{prop "\<forall>x. x = y"} *}
+ML_val {* genuine 2 @{prop "\<forall>x. x = y"} *}
+ML_val {* none 2 @{prop "\<exists>x. x = y"} *}
+ML_val {* none 2 @{prop "\<forall>x\<Colon>'a \<times> 'a. x = x"} *}
+ML_val {* none 2 @{prop "\<exists>x\<Colon>'a \<times> 'a. x = y"} *}
+ML_val {* genuine 2 @{prop "\<forall>x\<Colon>'a \<times> 'a. x = y"} *}
+ML_val {* none 2 @{prop "\<exists>x\<Colon>'a \<times> 'a. x = y"} *}
+ML_val {* none 1 @{prop "All = Ex"} *}
+ML_val {* genuine 2 @{prop "All = Ex"} *}
+ML_val {* none 1 @{prop "All P = Ex P"} *}
+ML_val {* genuine 2 @{prop "All P = Ex P"} *}
+ML_val {* none 5 @{prop "x = y \<longrightarrow> P x = P y"} *}
+ML_val {* none 5 @{prop "(x\<Colon>'a \<times> 'a) = y \<longrightarrow> P x = P y"} *}
+ML_val {* none 2 @{prop "(x\<Colon>'a \<times> 'a) = y \<longrightarrow> P x y = P y x"} *}
+ML_val {* none 5 @{prop "\<exists>x\<Colon>'a \<times> 'a. x = y \<longrightarrow> P x = P y"} *}
+ML_val {* none 2 @{prop "(x\<Colon>'a \<Rightarrow> 'a) = y \<longrightarrow> P x = P y"} *}
+ML_val {* none 2 @{prop "\<exists>x\<Colon>'a \<Rightarrow> 'a. x = y \<longrightarrow> P x = P y"} *}
+ML_val {* genuine 1 @{prop "(op =) X = Ex"} *}
+ML_val {* none 2 @{prop "\<forall>x::'a \<Rightarrow> 'a. x = x"} *}
+ML_val {* none 1 @{prop "x = y"} *}
+ML_val {* genuine 1 @{prop "x \<longleftrightarrow> y"} *}
+ML_val {* genuine 2 @{prop "x = y"} *}
+ML_val {* genuine 1 @{prop "X \<subseteq> Y"} *}
+ML_val {* none 1 @{prop "P \<and> Q \<longleftrightarrow> Q \<and> P"} *}
+ML_val {* none 1 @{prop "P \<and> Q \<longrightarrow> P"} *}
+ML_val {* none 1 @{prop "P \<or> Q \<longleftrightarrow> Q \<or> P"} *}
+ML_val {* genuine 1 @{prop "P \<or> Q \<longrightarrow> P"} *}
+ML_val {* none 1 @{prop "(P \<longrightarrow> Q) \<longleftrightarrow> (\<not> P \<or> Q)"} *}
+ML_val {* none 5 @{prop "{a} = {a, a}"} *}
+ML_val {* genuine 2 @{prop "{a} = {a, b}"} *}
+ML_val {* genuine 1 @{prop "{a} \<noteq> {a, b}"} *}
+ML_val {* none 5 @{prop "{}\<^sup>+ = {}"} *}
+ML_val {* none 5 @{prop "UNIV\<^sup>+ = UNIV"} *}
+ML_val {* none 5 @{prop "(UNIV \<Colon> ('a \<times> 'b) set) - {} = UNIV"} *}
+ML_val {* none 5 @{prop "{} - (UNIV \<Colon> ('a \<times> 'b) set) = {}"} *}
+ML_val {* none 1 @{prop "{(a, b), (b, c)}\<^sup>+ = {(a, b), (a, c), (b, c)}"} *}
+ML_val {* genuine 2 @{prop "{(a, b), (b, c)}\<^sup>+ = {(a, b), (a, c), (b, c)}"} *}
+ML_val {* none 5 @{prop "a \<noteq> c \<Longrightarrow> {(a, b), (b, c)}\<^sup>+ = {(a, b), (a, c), (b, c)}"} *}
+ML_val {* none 5 @{prop "A \<union> B = {x. x \<in> A \<or> x \<in> B}"} *}
+ML_val {* none 5 @{prop "A \<inter> B = {x. x \<in> A \<and> x \<in> B}"} *}
+ML_val {* none 5 @{prop "A - B = (\<lambda>x. A x \<and> \<not> B x)"} *}
+ML_val {* none 5 @{prop "\<exists>a b. (a, b) = (b, a)"} *}
+ML_val {* genuine 2 @{prop "(a, b) = (b, a)"} *}
+ML_val {* genuine 2 @{prop "(a, b) \<noteq> (b, a)"} *}
+ML_val {* none 5 @{prop "\<exists>a b\<Colon>'a \<times> 'a. (a, b) = (b, a)"} *}
+ML_val {* genuine 2 @{prop "(a\<Colon>'a \<times> 'a, b) = (b, a)"} *}
+ML_val {* none 5 @{prop "\<exists>a b\<Colon>'a \<times> 'a \<times> 'a. (a, b) = (b, a)"} *}
+ML_val {* genuine 2 @{prop "(a\<Colon>'a \<times> 'a \<times> 'a, b) \<noteq> (b, a)"} *}
+ML_val {* none 5 @{prop "\<exists>a b\<Colon>'a \<Rightarrow> 'a. (a, b) = (b, a)"} *}
+ML_val {* genuine 1 @{prop "(a\<Colon>'a \<Rightarrow> 'a, b) \<noteq> (b, a)"} *}
+ML_val {* none 5 @{prop "fst (a, b) = a"} *}
+ML_val {* none 1 @{prop "fst (a, b) = b"} *}
+ML_val {* genuine 2 @{prop "fst (a, b) = b"} *}
+ML_val {* genuine 2 @{prop "fst (a, b) \<noteq> b"} *}
+ML_val {* genuine 2 @{prop "f ((x, z), y) = (x, z)"} *}
+ML_val {* none 2 @{prop "(ALL x. f x = fst x) \<longrightarrow> f ((x, z), y) = (x, z)"} *}
+ML_val {* none 5 @{prop "snd (a, b) = b"} *}
+ML_val {* none 1 @{prop "snd (a, b) = a"} *}
+ML_val {* genuine 2 @{prop "snd (a, b) = a"} *}
+ML_val {* genuine 2 @{prop "snd (a, b) \<noteq> a"} *}
+ML_val {* genuine 1 @{prop P} *}
+ML_val {* genuine 1 @{prop "(\<lambda>x. P) a"} *}
+ML_val {* genuine 1 @{prop "(\<lambda>x y z. P y x z) a b c"} *}
+ML_val {* none 5 @{prop "\<exists>f. f = (\<lambda>x. x) \<and> f y = y"} *}
+ML_val {* genuine 1 @{prop "\<exists>f. f p \<noteq> p \<and> (\<forall>a b. f (a, b) = (a, b))"} *}
+ML_val {* none 2 @{prop "\<exists>f. \<forall>a b. f (a, b) = (a, b)"} *}
+ML_val {* none 3 @{prop "f = (\<lambda>a b. (b, a)) \<longrightarrow> f x y = (y, x)"} *}
+ML_val {* genuine 2 @{prop "f = (\<lambda>a b. (b, a)) \<longrightarrow> f x y = (x, y)"} *}
+ML_val {* none 5 @{prop "f = (\<lambda>x. f x)"} *}
+ML_val {* none 5 @{prop "f = (\<lambda>x. f x\<Colon>'a \<Rightarrow> bool)"} *}
+ML_val {* none 5 @{prop "f = (\<lambda>x y. f x y)"} *}
+ML_val {* none 5 @{prop "f = (\<lambda>x y. f x y\<Colon>'a \<Rightarrow> bool)"} *}
end
--- a/src/HOL/Nitpick_Examples/Mono_Nits.thy Mon Feb 25 20:11:42 2013 +0100
+++ b/src/HOL/Nitpick_Examples/Mono_Nits.thy Mon Feb 25 20:55:48 2013 +0100
@@ -67,78 +67,78 @@
ML {* Nitpick_Mono.trace := false *}
-ML {* const @{term "A\<Colon>('a\<Rightarrow>'b)"} *}
-ML {* const @{term "(A\<Colon>'a set) = A"} *}
-ML {* const @{term "(A\<Colon>'a set set) = A"} *}
-ML {* const @{term "(\<lambda>x\<Colon>'a set. a \<in> x)"} *}
-ML {* const @{term "{{a\<Colon>'a}} = C"} *}
-ML {* const @{term "{f\<Colon>'a\<Rightarrow>nat} = {g\<Colon>'a\<Rightarrow>nat}"} *}
-ML {* const @{term "A \<union> (B\<Colon>'a set)"} *}
-ML {* const @{term "\<lambda>A B x\<Colon>'a. A x \<or> B x"} *}
-ML {* const @{term "P (a\<Colon>'a)"} *}
-ML {* const @{term "\<lambda>a\<Colon>'a. b (c (d\<Colon>'a)) (e\<Colon>'a) (f\<Colon>'a)"} *}
-ML {* const @{term "\<forall>A\<Colon>'a set. a \<in> A"} *}
-ML {* const @{term "\<forall>A\<Colon>'a set. P A"} *}
-ML {* const @{term "P \<or> Q"} *}
-ML {* const @{term "A \<union> B = (C\<Colon>'a set)"} *}
-ML {* const @{term "(\<lambda>A B x\<Colon>'a. A x \<or> B x) A B = C"} *}
-ML {* const @{term "(if P then (A\<Colon>'a set) else B) = C"} *}
-ML {* const @{term "let A = (C\<Colon>'a set) in A \<union> B"} *}
-ML {* const @{term "THE x\<Colon>'b. P x"} *}
-ML {* const @{term "(\<lambda>x\<Colon>'a. False)"} *}
-ML {* const @{term "(\<lambda>x\<Colon>'a. True)"} *}
-ML {* const @{term "(\<lambda>x\<Colon>'a. False) = (\<lambda>x\<Colon>'a. False)"} *}
-ML {* const @{term "(\<lambda>x\<Colon>'a. True) = (\<lambda>x\<Colon>'a. True)"} *}
-ML {* const @{term "Let (a\<Colon>'a) A"} *}
-ML {* const @{term "A (a\<Colon>'a)"} *}
-ML {* const @{term "insert (a\<Colon>'a) A = B"} *}
-ML {* const @{term "- (A\<Colon>'a set)"} *}
-ML {* const @{term "finite (A\<Colon>'a set)"} *}
-ML {* const @{term "\<not> finite (A\<Colon>'a set)"} *}
-ML {* const @{term "finite (A\<Colon>'a set set)"} *}
-ML {* const @{term "\<lambda>a\<Colon>'a. A a \<and> \<not> B a"} *}
-ML {* const @{term "A < (B\<Colon>'a set)"} *}
-ML {* const @{term "A \<le> (B\<Colon>'a set)"} *}
-ML {* const @{term "[a\<Colon>'a]"} *}
-ML {* const @{term "[a\<Colon>'a set]"} *}
-ML {* const @{term "[A \<union> (B\<Colon>'a set)]"} *}
-ML {* const @{term "[A \<union> (B\<Colon>'a set)] = [C]"} *}
-ML {* const @{term "{(\<lambda>x\<Colon>'a. x = a)} = C"} *}
-ML {* const @{term "(\<lambda>a\<Colon>'a. \<not> A a) = B"} *}
-ML {* const @{prop "\<forall>F f g (h\<Colon>'a set). F f \<and> F g \<and> \<not> f a \<and> g a \<longrightarrow> \<not> f a"} *}
-ML {* const @{term "\<lambda>A B x\<Colon>'a. A x \<and> B x \<and> A = B"} *}
-ML {* const @{term "p = (\<lambda>(x\<Colon>'a) (y\<Colon>'a). P x \<or> \<not> Q y)"} *}
-ML {* const @{term "p = (\<lambda>(x\<Colon>'a) (y\<Colon>'a). p x y \<Colon> bool)"} *}
-ML {* const @{term "p = (\<lambda>A B x. A x \<and> \<not> B x) (\<lambda>x. True) (\<lambda>y. x \<noteq> y)"} *}
-ML {* const @{term "p = (\<lambda>y. x \<noteq> y)"} *}
-ML {* const @{term "(\<lambda>x. (p\<Colon>'a\<Rightarrow>bool\<Rightarrow>bool) x False)"} *}
-ML {* const @{term "(\<lambda>x y. (p\<Colon>'a\<Rightarrow>'a\<Rightarrow>bool\<Rightarrow>bool) x y False)"} *}
-ML {* const @{term "f = (\<lambda>x\<Colon>'a. P x \<longrightarrow> Q x)"} *}
-ML {* const @{term "\<forall>a\<Colon>'a. P a"} *}
+ML_val {* const @{term "A\<Colon>('a\<Rightarrow>'b)"} *}
+ML_val {* const @{term "(A\<Colon>'a set) = A"} *}
+ML_val {* const @{term "(A\<Colon>'a set set) = A"} *}
+ML_val {* const @{term "(\<lambda>x\<Colon>'a set. a \<in> x)"} *}
+ML_val {* const @{term "{{a\<Colon>'a}} = C"} *}
+ML_val {* const @{term "{f\<Colon>'a\<Rightarrow>nat} = {g\<Colon>'a\<Rightarrow>nat}"} *}
+ML_val {* const @{term "A \<union> (B\<Colon>'a set)"} *}
+ML_val {* const @{term "\<lambda>A B x\<Colon>'a. A x \<or> B x"} *}
+ML_val {* const @{term "P (a\<Colon>'a)"} *}
+ML_val {* const @{term "\<lambda>a\<Colon>'a. b (c (d\<Colon>'a)) (e\<Colon>'a) (f\<Colon>'a)"} *}
+ML_val {* const @{term "\<forall>A\<Colon>'a set. a \<in> A"} *}
+ML_val {* const @{term "\<forall>A\<Colon>'a set. P A"} *}
+ML_val {* const @{term "P \<or> Q"} *}
+ML_val {* const @{term "A \<union> B = (C\<Colon>'a set)"} *}
+ML_val {* const @{term "(\<lambda>A B x\<Colon>'a. A x \<or> B x) A B = C"} *}
+ML_val {* const @{term "(if P then (A\<Colon>'a set) else B) = C"} *}
+ML_val {* const @{term "let A = (C\<Colon>'a set) in A \<union> B"} *}
+ML_val {* const @{term "THE x\<Colon>'b. P x"} *}
+ML_val {* const @{term "(\<lambda>x\<Colon>'a. False)"} *}
+ML_val {* const @{term "(\<lambda>x\<Colon>'a. True)"} *}
+ML_val {* const @{term "(\<lambda>x\<Colon>'a. False) = (\<lambda>x\<Colon>'a. False)"} *}
+ML_val {* const @{term "(\<lambda>x\<Colon>'a. True) = (\<lambda>x\<Colon>'a. True)"} *}
+ML_val {* const @{term "Let (a\<Colon>'a) A"} *}
+ML_val {* const @{term "A (a\<Colon>'a)"} *}
+ML_val {* const @{term "insert (a\<Colon>'a) A = B"} *}
+ML_val {* const @{term "- (A\<Colon>'a set)"} *}
+ML_val {* const @{term "finite (A\<Colon>'a set)"} *}
+ML_val {* const @{term "\<not> finite (A\<Colon>'a set)"} *}
+ML_val {* const @{term "finite (A\<Colon>'a set set)"} *}
+ML_val {* const @{term "\<lambda>a\<Colon>'a. A a \<and> \<not> B a"} *}
+ML_val {* const @{term "A < (B\<Colon>'a set)"} *}
+ML_val {* const @{term "A \<le> (B\<Colon>'a set)"} *}
+ML_val {* const @{term "[a\<Colon>'a]"} *}
+ML_val {* const @{term "[a\<Colon>'a set]"} *}
+ML_val {* const @{term "[A \<union> (B\<Colon>'a set)]"} *}
+ML_val {* const @{term "[A \<union> (B\<Colon>'a set)] = [C]"} *}
+ML_val {* const @{term "{(\<lambda>x\<Colon>'a. x = a)} = C"} *}
+ML_val {* const @{term "(\<lambda>a\<Colon>'a. \<not> A a) = B"} *}
+ML_val {* const @{prop "\<forall>F f g (h\<Colon>'a set). F f \<and> F g \<and> \<not> f a \<and> g a \<longrightarrow> \<not> f a"} *}
+ML_val {* const @{term "\<lambda>A B x\<Colon>'a. A x \<and> B x \<and> A = B"} *}
+ML_val {* const @{term "p = (\<lambda>(x\<Colon>'a) (y\<Colon>'a). P x \<or> \<not> Q y)"} *}
+ML_val {* const @{term "p = (\<lambda>(x\<Colon>'a) (y\<Colon>'a). p x y \<Colon> bool)"} *}
+ML_val {* const @{term "p = (\<lambda>A B x. A x \<and> \<not> B x) (\<lambda>x. True) (\<lambda>y. x \<noteq> y)"} *}
+ML_val {* const @{term "p = (\<lambda>y. x \<noteq> y)"} *}
+ML_val {* const @{term "(\<lambda>x. (p\<Colon>'a\<Rightarrow>bool\<Rightarrow>bool) x False)"} *}
+ML_val {* const @{term "(\<lambda>x y. (p\<Colon>'a\<Rightarrow>'a\<Rightarrow>bool\<Rightarrow>bool) x y False)"} *}
+ML_val {* const @{term "f = (\<lambda>x\<Colon>'a. P x \<longrightarrow> Q x)"} *}
+ML_val {* const @{term "\<forall>a\<Colon>'a. P a"} *}
-ML {* nonconst @{term "\<forall>P (a\<Colon>'a). P a"} *}
-ML {* nonconst @{term "THE x\<Colon>'a. P x"} *}
-ML {* nonconst @{term "SOME x\<Colon>'a. P x"} *}
-ML {* nonconst @{term "(\<lambda>A B x\<Colon>'a. A x \<or> B x) = myunion"} *}
-ML {* nonconst @{term "(\<lambda>x\<Colon>'a. False) = (\<lambda>x\<Colon>'a. True)"} *}
-ML {* nonconst @{prop "\<forall>F f g (h\<Colon>'a set). F f \<and> F g \<and> \<not> a \<in> f \<and> a \<in> g \<longrightarrow> F h"} *}
+ML_val {* nonconst @{term "\<forall>P (a\<Colon>'a). P a"} *}
+ML_val {* nonconst @{term "THE x\<Colon>'a. P x"} *}
+ML_val {* nonconst @{term "SOME x\<Colon>'a. P x"} *}
+ML_val {* nonconst @{term "(\<lambda>A B x\<Colon>'a. A x \<or> B x) = myunion"} *}
+ML_val {* nonconst @{term "(\<lambda>x\<Colon>'a. False) = (\<lambda>x\<Colon>'a. True)"} *}
+ML_val {* nonconst @{prop "\<forall>F f g (h\<Colon>'a set). F f \<and> F g \<and> \<not> a \<in> f \<and> a \<in> g \<longrightarrow> F h"} *}
-ML {* mono @{prop "Q (\<forall>x\<Colon>'a set. P x)"} *}
-ML {* mono @{prop "P (a\<Colon>'a)"} *}
-ML {* mono @{prop "{a} = {b\<Colon>'a}"} *}
-ML {* mono @{prop "(\<lambda>x. x = a) = (\<lambda>y. y = (b\<Colon>'a))"} *}
-ML {* mono @{prop "(a\<Colon>'a) \<in> P \<and> P \<union> P = P"} *}
-ML {* mono @{prop "\<forall>F\<Colon>'a set set. P"} *}
-ML {* mono @{prop "\<not> (\<forall>F f g (h\<Colon>'a set). F f \<and> F g \<and> \<not> a \<in> f \<and> a \<in> g \<longrightarrow> F h)"} *}
-ML {* mono @{prop "\<not> Q (\<forall>x\<Colon>'a set. P x)"} *}
-ML {* mono @{prop "\<not> (\<forall>x\<Colon>'a. P x)"} *}
-ML {* mono @{prop "myall P = (P = (\<lambda>x\<Colon>'a. True))"} *}
-ML {* mono @{prop "myall P = (P = (\<lambda>x\<Colon>'a. False))"} *}
-ML {* mono @{prop "\<forall>x\<Colon>'a. P x"} *}
-ML {* mono @{term "(\<lambda>A B x\<Colon>'a. A x \<or> B x) \<noteq> myunion"} *}
+ML_val {* mono @{prop "Q (\<forall>x\<Colon>'a set. P x)"} *}
+ML_val {* mono @{prop "P (a\<Colon>'a)"} *}
+ML_val {* mono @{prop "{a} = {b\<Colon>'a}"} *}
+ML_val {* mono @{prop "(\<lambda>x. x = a) = (\<lambda>y. y = (b\<Colon>'a))"} *}
+ML_val {* mono @{prop "(a\<Colon>'a) \<in> P \<and> P \<union> P = P"} *}
+ML_val {* mono @{prop "\<forall>F\<Colon>'a set set. P"} *}
+ML_val {* mono @{prop "\<not> (\<forall>F f g (h\<Colon>'a set). F f \<and> F g \<and> \<not> a \<in> f \<and> a \<in> g \<longrightarrow> F h)"} *}
+ML_val {* mono @{prop "\<not> Q (\<forall>x\<Colon>'a set. P x)"} *}
+ML_val {* mono @{prop "\<not> (\<forall>x\<Colon>'a. P x)"} *}
+ML_val {* mono @{prop "myall P = (P = (\<lambda>x\<Colon>'a. True))"} *}
+ML_val {* mono @{prop "myall P = (P = (\<lambda>x\<Colon>'a. False))"} *}
+ML_val {* mono @{prop "\<forall>x\<Colon>'a. P x"} *}
+ML_val {* mono @{term "(\<lambda>A B x\<Colon>'a. A x \<or> B x) \<noteq> myunion"} *}
-ML {* nonmono @{prop "A = (\<lambda>x::'a. True) \<and> A = (\<lambda>x. False)"} *}
-ML {* nonmono @{prop "\<forall>F f g (h\<Colon>'a set). F f \<and> F g \<and> \<not> a \<in> f \<and> a \<in> g \<longrightarrow> F h"} *}
+ML_val {* nonmono @{prop "A = (\<lambda>x::'a. True) \<and> A = (\<lambda>x. False)"} *}
+ML_val {* nonmono @{prop "\<forall>F f g (h\<Colon>'a set). F f \<and> F g \<and> \<not> a \<in> f \<and> a \<in> g \<longrightarrow> F h"} *}
ML {*
val preproc_timeout = SOME (seconds 5.0)
@@ -200,12 +200,12 @@
*}
(*
-ML {* check_theory @{theory AVL2} *}
-ML {* check_theory @{theory Fun} *}
-ML {* check_theory @{theory Huffman} *}
-ML {* check_theory @{theory List} *}
-ML {* check_theory @{theory Map} *}
-ML {* check_theory @{theory Relation} *}
+ML_val {* check_theory @{theory AVL2} *}
+ML_val {* check_theory @{theory Fun} *}
+ML_val {* check_theory @{theory Huffman} *}
+ML_val {* check_theory @{theory List} *}
+ML_val {* check_theory @{theory Map} *}
+ML_val {* check_theory @{theory Relation} *}
*)
ML {* getenv "ISABELLE_TMP" *}
--- a/src/HOL/Predicate_Compile_Examples/Specialisation_Examples.thy Mon Feb 25 20:11:42 2013 +0100
+++ b/src/HOL/Predicate_Compile_Examples/Specialisation_Examples.thy Mon Feb 25 20:55:48 2013 +0100
@@ -15,7 +15,7 @@
"greater_than_index xs = (\<forall>i x. nth_el' xs i = Some x --> x > i)"
code_pred (expected_modes: i => bool) [inductify, skip_proof, specialise] greater_than_index .
-ML {* Core_Data.intros_of @{context} @{const_name specialised_nth_el'P} *}
+ML_val {* Core_Data.intros_of @{context} @{const_name specialised_nth_el'P} *}
thm greater_than_index.equation
@@ -44,7 +44,7 @@
thm max_of_my_SucP.equation
-ML {* Core_Data.intros_of @{context} @{const_name specialised_max_natP} *}
+ML_val {* Core_Data.intros_of @{context} @{const_name specialised_max_natP} *}
values "{x. max_of_my_SucP x 6}"
--- a/src/HOL/Proofs/Extraction/Higman_Extraction.thy Mon Feb 25 20:11:42 2013 +0100
+++ b/src/HOL/Proofs/Extraction/Higman_Extraction.thy Mon Feb 25 20:55:48 2013 +0100
@@ -88,7 +88,7 @@
| "f2 (Suc (Suc 0)) = [B, A]"
| "f2 _ = []"
-ML {*
+ML_val {*
local
val higman_idx = @{code higman_idx};
val g1 = @{code g1};
--- a/src/HOL/Proofs/Extraction/Pigeonhole.thy Mon Feb 25 20:11:42 2013 +0100
+++ b/src/HOL/Proofs/Extraction/Pigeonhole.thy Mon Feb 25 20:55:48 2013 +0100
@@ -243,14 +243,14 @@
definition
"test'' u = pigeonhole 8 (List.nth [0, 1, 2, 3, 4, 5, 6, 3, 7, 8])"
-ML "timeit (@{code test} 10)"
-ML "timeit (@{code test'} 10)"
-ML "timeit (@{code test} 20)"
-ML "timeit (@{code test'} 20)"
-ML "timeit (@{code test} 25)"
-ML "timeit (@{code test'} 25)"
-ML "timeit (@{code test} 500)"
-ML "timeit @{code test''}"
+ML_val "timeit (@{code test} 10)"
+ML_val "timeit (@{code test'} 10)"
+ML_val "timeit (@{code test} 20)"
+ML_val "timeit (@{code test'} 20)"
+ML_val "timeit (@{code test} 25)"
+ML_val "timeit (@{code test'} 25)"
+ML_val "timeit (@{code test} 500)"
+ML_val "timeit @{code test''}"
end
--- a/src/HOL/Proofs/Extraction/Warshall.thy Mon Feb 25 20:11:42 2013 +0100
+++ b/src/HOL/Proofs/Extraction/Warshall.thy Mon Feb 25 20:55:48 2013 +0100
@@ -256,6 +256,6 @@
@{thm [display] warshall_correctness [no_vars]}
*}
-ML "@{code warshall}"
+ML_val "@{code warshall}"
end
--- a/src/HOL/Quickcheck_Examples/Hotel_Example.thy Mon Feb 25 20:11:42 2013 +0100
+++ b/src/HOL/Quickcheck_Examples/Hotel_Example.thy Mon Feb 25 20:55:48 2013 +0100
@@ -92,7 +92,7 @@
setup {* Predicate_Compile_Data.ignore_consts [@{const_name Set.member},
@{const_name "issued"}, @{const_name "cards"}, @{const_name "isin"},
@{const_name Collect}, @{const_name insert}] *}
-ML {* Core_Data.force_modes_and_compilations *}
+ML_val {* Core_Data.force_modes_and_compilations *}
fun find_first :: "('a => 'b option) => 'a list => 'b option"
where
--- a/src/HOL/Quickcheck_Examples/Quickcheck_Interfaces.thy Mon Feb 25 20:11:42 2013 +0100
+++ b/src/HOL/Quickcheck_Examples/Quickcheck_Interfaces.thy Mon Feb 25 20:55:48 2013 +0100
@@ -33,16 +33,16 @@
fun check_upto f i j = if i > j then true else f i andalso check_upto f (i + 1) j
*}
-ML {*
+ML_val {*
map (fn test => check_upto test 0 1) testers
*}
-ML {*
+ML_val {*
map (fn test => check_upto test 0 2) testers
*}
-ML {*
+ML_val {*
map (fn test => check_upto test 0 3) testers
*}
-ML {*
+ML_val {*
map (fn test => check_upto test 0 7) testers
*}
--- a/src/Pure/Isar/keyword.ML Mon Feb 25 20:11:42 2013 +0100
+++ b/src/Pure/Isar/keyword.ML Mon Feb 25 20:55:48 2013 +0100
@@ -22,7 +22,6 @@
val thy_load_files: string list -> T
val thy_script: T
val thy_goal: T
- val thy_schematic_goal: T
val qed: T
val qed_block: T
val qed_global: T
@@ -66,7 +65,6 @@
val is_proof_body: string -> bool
val is_theory_goal: string -> bool
val is_proof_goal: string -> bool
- val is_schematic_goal: string -> bool
val is_qed: string -> bool
val is_qed_global: string -> bool
end;
@@ -104,7 +102,6 @@
fun thy_load_files files = Keyword {kind = "thy_load", files = files, tags = []};
val thy_script = kind "thy_script";
val thy_goal = kind "thy_goal";
-val thy_schematic_goal = kind "thy_schematic_goal";
val qed = kind "qed";
val qed_block = kind "qed_block";
val qed_global = kind "qed_global";
@@ -123,7 +120,7 @@
val kinds =
[control, diag, thy_begin, thy_end, thy_heading1, thy_heading2, thy_heading3, thy_heading4,
- thy_load, thy_decl, thy_script, thy_goal, thy_schematic_goal, qed, qed_block, qed_global,
+ thy_load, thy_decl, thy_script, thy_goal, qed, qed_block, qed_global,
prf_heading2, prf_heading3, prf_heading4, prf_goal, prf_block, prf_open,
prf_close, prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_script];
@@ -253,7 +250,7 @@
val is_theory = command_category
[thy_begin, thy_end, thy_heading1, thy_heading2, thy_heading3, thy_heading4,
- thy_load, thy_decl, thy_script, thy_goal, thy_schematic_goal];
+ thy_load, thy_decl, thy_script, thy_goal];
val is_proof = command_category
[qed, qed_block, qed_global, prf_heading2, prf_heading3, prf_heading4,
@@ -264,9 +261,8 @@
[diag, prf_heading2, prf_heading3, prf_heading4, prf_block, prf_open,
prf_close, prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_script];
-val is_theory_goal = command_category [thy_goal, thy_schematic_goal];
+val is_theory_goal = command_category [thy_goal];
val is_proof_goal = command_category [prf_goal, prf_asm_goal];
-val is_schematic_goal = command_category [thy_schematic_goal];
val is_qed = command_category [qed, qed_block];
val is_qed_global = command_category [qed_global];
--- a/src/Pure/Isar/keyword.scala Mon Feb 25 20:11:42 2013 +0100
+++ b/src/Pure/Isar/keyword.scala Mon Feb 25 20:55:48 2013 +0100
@@ -24,7 +24,6 @@
val THY_LOAD = "thy_load"
val THY_SCRIPT = "thy_script"
val THY_GOAL = "thy_goal"
- val THY_SCHEMATIC_GOAL = "thy_schematic_goal"
val QED = "qed"
val QED_BLOCK = "qed_block"
val QED_GLOBAL = "qed_global"
@@ -49,7 +48,7 @@
val diag = Set(DIAG)
val theory =
Set(THY_BEGIN, THY_END, THY_HEADING1, THY_HEADING2, THY_HEADING3, THY_HEADING4,
- THY_DECL, THY_SCRIPT, THY_GOAL, THY_SCHEMATIC_GOAL)
+ THY_DECL, THY_SCRIPT, THY_GOAL)
val theory1 = Set(THY_BEGIN, THY_END)
val theory2 = Set(THY_DECL, THY_GOAL)
val proof =
--- a/src/Pure/Isar/outer_syntax.ML Mon Feb 25 20:11:42 2013 +0100
+++ b/src/Pure/Isar/outer_syntax.ML Mon Feb 25 20:55:48 2013 +0100
@@ -35,9 +35,7 @@
type isar
val isar: TextIO.instream -> bool -> isar
val span_cmts: Token.T list -> Token.T list
- val read_span: outer_syntax -> Token.T list -> Toplevel.transition * bool
- val read_element: outer_syntax -> (unit -> theory) -> Thy_Syntax.span Thy_Syntax.element ->
- (Toplevel.transition * Toplevel.transition list) list
+ val read_span: outer_syntax -> Token.T list -> Toplevel.transition
end;
structure Outer_Syntax: OUTER_SYNTAX =
@@ -295,7 +293,7 @@
end;
-(* read toplevel commands -- fail-safe *)
+(* read command span -- fail-safe *)
fun read_span outer_syntax toks =
let
@@ -319,30 +317,16 @@
val (is_malformed, token_reports) = Thy_Syntax.reports_of_tokens toks;
val _ = Position.reports_text (token_reports @ maps command_reports toks);
in
- if is_malformed then (Toplevel.malformed pos "Malformed command syntax", true)
+ if is_malformed then Toplevel.malformed pos "Malformed command syntax"
else
(case Source.exhaust (toplevel_source false NONE (K commands) (Source.of_list toks)) of
[tr] =>
if Keyword.is_control (Toplevel.name_of tr) then
- (Toplevel.malformed pos "Illegal control command", true)
- else (tr, true)
- | [] => (Toplevel.ignored (Position.set_range (Command.range toks)), false)
- | _ => (Toplevel.malformed proper_range "Exactly one command expected", true))
- handle ERROR msg => (Toplevel.malformed proper_range msg, true)
- end;
-
-fun read_element outer_syntax init (Thy_Syntax.Element (head, opt_proof)) =
- let
- val read = read_span outer_syntax o Thy_Syntax.span_content;
- val (tr, proper_head) = read head |>> Toplevel.modify_init init;
- val proof_trs =
- (case opt_proof of
- NONE => []
- | SOME (a, b) => map read (maps Thy_Syntax.flat_element a @ [b]) |> filter #2 |> map #1);
- in
- if proper_head andalso
- not (Keyword.is_schematic_goal (Toplevel.name_of tr)) then [(tr, proof_trs)]
- else map (rpair []) (if proper_head then tr :: proof_trs else proof_trs)
+ Toplevel.malformed pos "Illegal control command"
+ else tr
+ | [] => Toplevel.ignored (Position.set_range (Command.range toks))
+ | _ => Toplevel.malformed proper_range "Exactly one command expected")
+ handle ERROR msg => Toplevel.malformed proper_range msg
end;
end;
--- a/src/Pure/Isar/token.ML Mon Feb 25 20:11:42 2013 +0100
+++ b/src/Pure/Isar/token.ML Mon Feb 25 20:55:48 2013 +0100
@@ -32,6 +32,7 @@
val is_command: T -> bool
val is_name: T -> bool
val is_proper: T -> bool
+ val is_improper: T -> bool
val is_semicolon: T -> bool
val is_comment: T -> bool
val is_begin_ignore: T -> bool
@@ -172,6 +173,8 @@
| is_proper (Token (_, (Comment, _), _)) = false
| is_proper _ = true;
+val is_improper = not o is_proper;
+
fun is_semicolon (Token (_, (Keyword, ";"), _)) = true
| is_semicolon _ = false;
--- a/src/Pure/Isar/toplevel.ML Mon Feb 25 20:11:42 2013 +0100
+++ b/src/Pure/Isar/toplevel.ML Mon Feb 25 20:55:48 2013 +0100
@@ -51,6 +51,7 @@
val keep': (bool -> state -> unit) -> transition -> transition
val imperative: (unit -> unit) -> transition -> transition
val ignored: Position.T -> transition
+ val is_ignored: transition -> bool
val malformed: Position.T -> string -> transition
val is_malformed: transition -> bool
val generic_theory: (generic_theory -> generic_theory) -> transition -> transition
@@ -94,7 +95,7 @@
val put_timing: Time.time -> transition -> transition
val transition: bool -> transition -> state -> (state * (exn * string) option) option
val command: transition -> state -> state
- val proof_result: bool -> transition * transition list -> state ->
+ val element_result: transition Thy_Syntax.element -> state ->
(transition * state) list future * state
end;
@@ -414,6 +415,7 @@
fun imperative f = keep (fn _ => f ());
fun ignored pos = empty |> name "<ignored>" |> position pos |> imperative I;
+fun is_ignored tr = name_of tr = "<ignored>";
val malformed_name = "<malformed>";
fun malformed pos msg =
@@ -692,10 +694,6 @@
if Exn.is_interrupt exn then reraise exn else raise Runtime.EXCURSION_FAIL (exn, info)
| NONE => raise Runtime.EXCURSION_FAIL (Runtime.TERMINATE, at_command tr));
-fun command_result tr st =
- let val st' = command tr st
- in ((tr, st'), st') end;
-
(* scheduled proof result *)
@@ -706,13 +704,26 @@
fun init _ = empty;
);
-fun proof_result immediate (tr, proof_trs) st =
- let val st' = command tr st in
- if immediate orelse null proof_trs orelse not (can proof_of st') orelse
- Proof.is_relevant (proof_of st')
+fun element_result (Thy_Syntax.Element (head_tr, opt_proof)) st =
+ let
+ val future_enabled = Goal.future_enabled ();
+
+ fun atom_result tr st =
+ let val st' = command tr st
+ in ((tr, st'), st') end;
+
+ val proof_trs =
+ (case opt_proof of
+ NONE => []
+ | SOME (a, b) => (maps Thy_Syntax.flat_element a @ [b]) |> filter_out is_ignored);
+
+ val st' = command head_tr st;
+ in
+ if not future_enabled orelse is_ignored head_tr orelse
+ null proof_trs orelse not (can proof_of st') orelse Proof.is_relevant (proof_of st')
then
- let val (results, st'') = fold_map command_result proof_trs st'
- in (Future.value ((tr, st') :: results), st'') end
+ let val (results, st'') = fold_map atom_result proof_trs st'
+ in (Future.value (if is_ignored head_tr then results else (head_tr, st') :: results), st'') end
else
let
val (body_trs, end_tr) = split_last proof_trs;
@@ -730,15 +741,15 @@
let val (result, result_state) =
(case st' of State (SOME (Proof (_, (_, orig_gthy))), prev)
=> State (SOME (Proof (Proof_Node.init prf, (finish, orig_gthy))), prev))
- |> fold_map command_result body_trs ||> command end_tr;
+ |> fold_map atom_result body_trs ||> command end_tr;
in (result, presentation_context_of result_state) end))
#-> Result.put;
val st'' = st'
- |> command (tr |> set_print false |> reset_trans |> end_proof (K future_proof));
+ |> command (head_tr |> set_print false |> reset_trans |> end_proof (K future_proof));
val result =
Result.get (presentation_context_of st'')
- |> Future.map (fn body => (tr, st') :: body @ [(end_tr, st'')]);
+ |> Future.map (fn body => (head_tr, st') :: body @ [(end_tr, st'')]);
in (result, st'') end
end;
--- a/src/Pure/PIDE/command.ML Mon Feb 25 20:11:42 2013 +0100
+++ b/src/Pure/PIDE/command.ML Mon Feb 25 20:55:48 2013 +0100
@@ -23,7 +23,7 @@
(* span range *)
val range = Token.position_range_of;
-val proper_range = Token.position_range_of o #1 o take_suffix Token.is_space;
+val proper_range = Token.position_range_of o #1 o take_suffix Token.is_improper;
(* memo results *)
--- a/src/Pure/PIDE/document.ML Mon Feb 25 20:11:42 2013 +0100
+++ b/src/Pure/PIDE/document.ML Mon Feb 25 20:55:48 2013 +0100
@@ -268,9 +268,8 @@
val id_string = print_id id;
val span = Lazy.lazy (fn () =>
Position.setmp_thread_data (Position.id_only id_string)
- (fn () =>
- Thy_Syntax.parse_tokens
- (#1 (Outer_Syntax.get_syntax ())) (Position.id id_string) text) ());
+ (fn () => Thy_Syntax.parse_tokens (Keyword.get_lexicons ()) (Position.id id_string) text)
+ ());
val _ =
Position.setmp_thread_data (Position.id_only id_string)
(fn () => Output.status (Markup.markup_only Markup.accepted)) ();
@@ -453,7 +452,7 @@
(fn () =>
let
val tr =
- #1 (Outer_Syntax.read_span (#2 (Outer_Syntax.get_syntax ())) span)
+ Outer_Syntax.read_span (#2 (Outer_Syntax.get_syntax ())) span
|> modify_init
|> Toplevel.put_id exec_id'_string;
val cmts = Outer_Syntax.span_cmts span;
--- a/src/Pure/ProofGeneral/pgip_parser.ML Mon Feb 25 20:11:42 2013 +0100
+++ b/src/Pure/ProofGeneral/pgip_parser.ML Mon Feb 25 20:55:48 2013 +0100
@@ -65,7 +65,6 @@
|> command Keyword.thy_decl thy_decl
|> command Keyword.thy_script thy_decl
|> command Keyword.thy_goal goal
- |> command Keyword.thy_schematic_goal goal
|> command Keyword.qed closegoal
|> command Keyword.qed_block closegoal
|> command Keyword.qed_global (fn text => [D.Giveupgoal {text = text}])
--- a/src/Pure/Pure.thy Mon Feb 25 20:11:42 2013 +0100
+++ b/src/Pure/Pure.thy Mon Feb 25 20:55:48 2013 +0100
@@ -50,7 +50,7 @@
and "overloading" :: thy_decl
and "code_datatype" :: thy_decl
and "theorem" "lemma" "corollary" :: thy_goal
- and "schematic_theorem" "schematic_lemma" "schematic_corollary" :: thy_schematic_goal
+ and "schematic_theorem" "schematic_lemma" "schematic_corollary" :: thy_goal
and "notepad" :: thy_decl
and "have" :: prf_goal % "proof"
and "hence" :: prf_goal % "proof" == "then have"
@@ -75,7 +75,7 @@
and "finally" "ultimately" :: prf_chain % "proof"
and "back" :: prf_script % "proof"
and "Isabelle.command" :: control
- and "pretty_setmargin" "help" "print_commands" "print_configs"
+ and "help" "print_commands" "print_configs"
"print_context" "print_theory" "print_syntax" "print_abbrevs"
"print_theorems" "print_locales" "print_classes" "print_locale"
"print_interps" "print_dependencies" "print_attributes"
@@ -88,7 +88,7 @@
and "pwd" :: diag
and "use_thy" "remove_thy" "kill_thy" :: control
and "display_drafts" "print_drafts" "pr" :: diag
- and "disable_pr" "enable_pr" "commit" "quit" "exit" :: control
+ and "pretty_setmargin" "disable_pr" "enable_pr" "commit" "quit" "exit" :: control
and "welcome" :: diag
and "init_toplevel" "linear_undo" "undo" "undos_proof" "cannot_undo" "kill" :: control
and "end" :: thy_end % "theory"
--- a/src/Pure/ROOT.ML Mon Feb 25 20:11:42 2013 +0100
+++ b/src/Pure/ROOT.ML Mon Feb 25 20:55:48 2013 +0100
@@ -208,6 +208,7 @@
(*theory sources*)
use "Thy/thy_header.ML";
+use "Thy/thy_syntax.ML";
use "Thy/html.ML";
use "Thy/latex.ML";
@@ -257,7 +258,6 @@
use "System/isabelle_system.ML";
use "Thy/term_style.ML";
use "Thy/thy_output.ML";
-use "Thy/thy_syntax.ML";
use "PIDE/command.ML";
use "Isar/outer_syntax.ML";
use "General/graph_display.ML";
--- a/src/Pure/System/session.ML Mon Feb 25 20:11:42 2013 +0100
+++ b/src/Pure/System/session.ML Mon Feb 25 20:55:48 2013 +0100
@@ -67,14 +67,8 @@
(* finish *)
-fun finish_futures () =
- (case map_filter Task_Queue.group_status (Goal.reset_futures ()) of
- [] => ()
- | exns => raise Par_Exn.make exns);
-
fun finish () =
- (Future.shutdown ();
- finish_futures ();
+ (Goal.shutdown_futures ();
Thy_Info.finish ();
Present.finish ();
Keyword.status ();
--- a/src/Pure/Thy/thy_load.ML Mon Feb 25 20:11:42 2013 +0100
+++ b/src/Pure/Thy/thy_load.ML Mon Feb 25 20:55:48 2013 +0100
@@ -216,26 +216,24 @@
fun excursion last_timing init elements =
let
- val immediate = not (Goal.future_enabled ());
+ fun prepare_span span =
+ Thy_Syntax.span_content span
+ |> Outer_Syntax.read_span (#2 (Outer_Syntax.get_syntax ()))
+ |> Toplevel.modify_init init
+ |> (fn tr => Toplevel.put_timing (last_timing tr) tr);
- fun put_timing tr = Toplevel.put_timing (last_timing tr) tr;
- fun put_timings (tr, trs) = (put_timing tr, map put_timing trs);
-
- fun proof_result (tr, trs) (st, _) =
+ fun element_result span_elem (st, _) =
let
- val (result, st') = Toplevel.proof_result immediate (tr, trs) st;
- val pos' = Toplevel.pos_of (List.last (tr :: trs));
- in (result, (st', pos')) end;
-
- fun element_result elem x =
- fold_map (proof_result o put_timings)
- (Outer_Syntax.read_element (#2 (Outer_Syntax.get_syntax ())) init elem) x;
+ val elem = Thy_Syntax.map_element prepare_span span_elem;
+ val (results, st') = Toplevel.element_result elem st;
+ val pos' = Toplevel.pos_of (Thy_Syntax.last_element elem);
+ in (results, (st', pos')) end;
val (results, (end_state, end_pos)) =
fold_map element_result elements (Toplevel.toplevel, Position.none);
val thy = Toplevel.end_theory end_pos end_state;
- in (flat results, thy) end;
+ in (results, thy) end;
fun load_thy last_timing update_time master_dir header text_pos text parents =
let
--- a/src/Pure/Thy/thy_output.ML Mon Feb 25 20:11:42 2013 +0100
+++ b/src/Pure/Thy/thy_output.ML Mon Feb 25 20:55:48 2013 +0100
@@ -235,7 +235,7 @@
fun basic_token pred (BasicToken tok) = pred tok
| basic_token _ _ = false;
-val improper_token = basic_token (not o Token.is_proper);
+val improper_token = basic_token Token.is_improper;
val comment_token = basic_token Token.is_comment;
val blank_token = basic_token Token.is_blank;
val newline_token = basic_token Token.is_newline;
--- a/src/Pure/Thy/thy_syntax.ML Mon Feb 25 20:11:42 2013 +0100
+++ b/src/Pure/Thy/thy_syntax.ML Mon Feb 25 20:55:48 2013 +0100
@@ -18,6 +18,7 @@
datatype 'a element = Element of 'a * ('a element list * 'a) option
val map_element: ('a -> 'b) -> 'a element -> 'b element
val flat_element: 'a element -> 'a list
+ val last_element: 'a element -> 'a
val parse_elements: span list -> span element list
end;
@@ -118,7 +119,7 @@
fun make_span toks =
if not (null toks) andalso Token.is_command (hd toks) then
Span (Command (Token.content_of (hd toks), Token.position_of (hd toks)), toks)
- else if forall (not o Token.is_proper) toks then Span (Ignored, toks)
+ else if forall Token.is_improper toks then Span (Ignored, toks)
else Span (Malformed, toks);
fun flush (result, span) = if null span then (result, span) else (rev span :: result, []);
@@ -148,6 +149,9 @@
fun flat_element (Element (a, NONE)) = [a]
| flat_element (Element (a, SOME (elems, b))) = a :: maps flat_element elems @ [b];
+fun last_element (Element (a, NONE)) = a
+ | last_element (Element (_, SOME (_, b))) = b;
+
(* scanning spans *)
--- a/src/Pure/goal.ML Mon Feb 25 20:11:42 2013 +0100
+++ b/src/Pure/goal.ML Mon Feb 25 20:55:48 2013 +0100
@@ -28,6 +28,7 @@
val fork: int -> (unit -> 'a) -> 'a future
val peek_futures: serial -> unit future list
val reset_futures: unit -> Future.group list
+ val shutdown_futures: unit -> unit
val future_enabled_level: int -> bool
val future_enabled: unit -> bool
val future_enabled_nested: int -> bool
@@ -178,6 +179,12 @@
Synchronized.change_result forked_proofs (fn (m, groups, tab) =>
(Future.forked_proofs := 0; (groups, (0, [], Inttab.empty))));
+fun shutdown_futures () =
+ (Future.shutdown ();
+ (case map_filter Task_Queue.group_status (reset_futures ()) of
+ [] => ()
+ | exns => raise Par_Exn.make exns));
+
end;
--- a/src/Tools/Code_Generator.thy Mon Feb 25 20:11:42 2013 +0100
+++ b/src/Tools/Code_Generator.thy Mon Feb 25 20:55:48 2013 +0100
@@ -7,8 +7,8 @@
theory Code_Generator
imports Pure
keywords
- "value" "print_codeproc" "code_thms" "code_deps" "export_code" :: diag and
- "code_class" "code_instance" "code_type"
+ "value" "print_codeproc" "code_thms" "code_deps" :: diag and
+ "export_code" "code_class" "code_instance" "code_type"
"code_const" "code_reserved" "code_include" "code_modulename"
"code_abort" "code_monad" "code_reflect" :: thy_decl and
"datatypes" "functions" "module_name" "file" "checking"