--- a/NEWS Tue Mar 18 09:39:07 2014 -0700
+++ b/NEWS Tue Mar 18 21:02:33 2014 +0100
@@ -465,10 +465,8 @@
theory merge). Note that the softer Thm.eq_thm_prop is often more
appropriate than Thm.eq_thm.
-* Simplified programming interface to define ML antiquotations (to
-make it more close to the analogous Thy_Output.antiquotation). See
-ML_Context.antiquotation and structure ML_Antiquotation. Minor
-INCOMPATIBILITY.
+* Simplified programming interface to define ML antiquotations, see
+structure ML_Antiquotation. Minor INCOMPATIBILITY.
* ML antiquotation @{here} refers to its source position, which is
occasionally useful for experimentation and diagnostic purposes.
--- a/src/CCL/CCL.thy Tue Mar 18 09:39:07 2014 -0700
+++ b/src/CCL/CCL.thy Tue Mar 18 21:02:33 2014 +0100
@@ -295,9 +295,9 @@
val XH_to_Ds = map XH_to_D
val XH_to_Es = map XH_to_E;
-bind_thms ("ccl_rews", @{thms caseBs} @ @{thms ccl_injs} @ ccl_dstncts);
-bind_thms ("ccl_dstnctsEs", ccl_dstncts RL [@{thm notE}]);
-bind_thms ("ccl_injDs", XH_to_Ds @{thms ccl_injs});
+ML_Thms.bind_thms ("ccl_rews", @{thms caseBs} @ @{thms ccl_injs} @ ccl_dstncts);
+ML_Thms.bind_thms ("ccl_dstnctsEs", ccl_dstncts RL [@{thm notE}]);
+ML_Thms.bind_thms ("ccl_injDs", XH_to_Ds @{thms ccl_injs});
*}
lemmas [simp] = ccl_rews
--- a/src/CCL/Term.thy Tue Mar 18 09:39:07 2014 -0700
+++ b/src/CCL/Term.thy Tue Mar 18 21:02:33 2014 +0100
@@ -286,7 +286,7 @@
subsection {* Constructors are distinct *}
ML {*
-bind_thms ("term_dstncts",
+ML_Thms.bind_thms ("term_dstncts",
mkall_dstnct_thms @{context} @{thms data_defs} (@{thms ccl_injs} @ @{thms term_injs})
[["bot","inl","inr"], ["bot","zero","succ"], ["bot","nil","cons"]]);
*}
@@ -305,7 +305,7 @@
subsection {* Rewriting and Proving *}
ML {*
- bind_thms ("term_injDs", XH_to_Ds @{thms term_injs});
+ ML_Thms.bind_thms ("term_injDs", XH_to_Ds @{thms term_injs});
*}
lemmas term_rews = termBs term_injs term_dstncts ccl_porews term_porews
--- a/src/CCL/Type.thy Tue Mar 18 09:39:07 2014 -0700
+++ b/src/CCL/Type.thy Tue Mar 18 21:02:33 2014 +0100
@@ -101,7 +101,7 @@
unfolding simp_type_defs by blast+
ML {*
-bind_thms ("case_rls", XH_to_Es @{thms XHs});
+ML_Thms.bind_thms ("case_rls", XH_to_Es @{thms XHs});
*}
@@ -262,7 +262,7 @@
lemmas iXHs = NatXH ListXH
-ML {* bind_thms ("icase_rls", XH_to_Es @{thms iXHs}) *}
+ML {* ML_Thms.bind_thms ("icase_rls", XH_to_Es @{thms iXHs}) *}
subsection {* Type Rules *}
@@ -340,7 +340,7 @@
(* - intro rules are type rules for canonical terms *)
(* - elim rules are case rules (no non-canonical terms appear) *)
-ML {* bind_thms ("XHEs", XH_to_Es @{thms XHs}) *}
+ML {* ML_Thms.bind_thms ("XHEs", XH_to_Es @{thms XHs}) *}
lemmas [intro!] = SubtypeI canTs icanTs
and [elim!] = SubtypeE XHEs
--- a/src/Doc/Codegen/Setup.thy Tue Mar 18 09:39:07 2014 -0700
+++ b/src/Doc/Codegen/Setup.thy Tue Mar 18 21:02:33 2014 +0100
@@ -9,7 +9,7 @@
(* FIXME avoid writing into source directory *)
ML {*
- Isabelle_System.mkdirs (Path.append (Thy_Load.master_directory @{theory}) (Path.basic "examples"))
+ Isabelle_System.mkdirs (Path.append (Resources.master_directory @{theory}) (Path.basic "examples"))
*}
ML_file "../antiquote_setup.ML"
--- a/src/Doc/IsarImplementation/ML.thy Tue Mar 18 09:39:07 2014 -0700
+++ b/src/Doc/IsarImplementation/ML.thy Tue Mar 18 21:02:33 2014 +0100
@@ -627,8 +627,8 @@
\begin{mldecls}
@{index_ML ML_Context.the_generic_context: "unit -> Context.generic"} \\
@{index_ML "Context.>>": "(Context.generic -> Context.generic) -> unit"} \\
- @{index_ML bind_thms: "string * thm list -> unit"} \\
- @{index_ML bind_thm: "string * thm -> unit"} \\
+ @{index_ML ML_Thms.bind_thms: "string * thm list -> unit"} \\
+ @{index_ML ML_Thms.bind_thm: "string * thm -> unit"} \\
\end{mldecls}
\begin{description}
@@ -642,12 +642,12 @@
\item @{ML "Context.>>"}~@{text f} applies context transformation
@{text f} to the implicit context of the ML toplevel.
- \item @{ML bind_thms}~@{text "(name, thms)"} stores a list of
+ \item @{ML ML_Thms.bind_thms}~@{text "(name, thms)"} stores a list of
theorems produced in ML both in the (global) theory context and the
ML toplevel, associating it with the provided name. Theorems are
put into a global ``standard'' format before being stored.
- \item @{ML bind_thm} is similar to @{ML bind_thms} but refers to a
+ \item @{ML ML_Thms.bind_thm} is similar to @{ML ML_Thms.bind_thms} but refers to a
singleton fact.
\end{description}
--- a/src/Doc/Tutorial/ToyList/ToyList_Test.thy Tue Mar 18 09:39:07 2014 -0700
+++ b/src/Doc/Tutorial/ToyList/ToyList_Test.thy Tue Mar 18 21:02:33 2014 +0100
@@ -5,7 +5,7 @@
ML {* (* FIXME somewhat non-standard, fragile *)
let
val texts =
- map (File.read o Path.append (Thy_Load.master_directory @{theory}) o Path.explode)
+ map (File.read o Path.append (Resources.master_directory @{theory}) o Path.explode)
["ToyList1", "ToyList2"];
val trs = Outer_Syntax.parse Position.start (implode texts);
val end_state = fold (Toplevel.command_exception false) trs Toplevel.toplevel;
--- a/src/Doc/antiquote_setup.ML Tue Mar 18 09:39:07 2014 -0700
+++ b/src/Doc/antiquote_setup.ML Tue Mar 18 21:02:33 2014 +0100
@@ -152,7 +152,7 @@
val _ =
Theory.setup (Thy_Output.antiquotation @{binding thy_file} (Scan.lift Args.name)
(fn {context = ctxt, ...} =>
- fn name => (Thy_Load.check_thy Path.current name; Thy_Output.output ctxt [Pretty.str name])));
+ fn name => (Resources.check_thy Path.current name; Thy_Output.output ctxt [Pretty.str name])));
(* Isabelle/jEdit elements *)
--- a/src/FOLP/IFOLP.thy Tue Mar 18 09:39:07 2014 -0700
+++ b/src/FOLP/IFOLP.thy Tue Mar 18 21:02:33 2014 +0100
@@ -411,7 +411,7 @@
done
(*NOT PROVED
-bind_thm ("ex1_cong", prove_goal (the_context ())
+ML_Thms.bind_thm ("ex1_cong", prove_goal (the_context ())
"(!!x.f(x):P(x) <-> Q(x)) ==> ?p:(EX! x.P(x)) <-> (EX! x.Q(x))"
(fn prems =>
[ (REPEAT (eresolve_tac [ex1E, spec RS mp] 1 ORELSE ares_tac [iffI,ex1I] 1
--- a/src/HOL/Bali/AxSem.thy Tue Mar 18 09:39:07 2014 -0700
+++ b/src/HOL/Bali/AxSem.thy Tue Mar 18 21:02:33 2014 +0100
@@ -1006,7 +1006,7 @@
apply (auto simp add: type_ok_def)
done
-ML {* bind_thms ("ax_Abrupts", sum3_instantiate @{context} @{thm ax_derivs.Abrupt}) *}
+ML {* ML_Thms.bind_thms ("ax_Abrupts", sum3_instantiate @{context} @{thm ax_derivs.Abrupt}) *}
declare ax_Abrupts [intro!]
lemmas ax_Normal_cases = ax_cases [of _ _ _ normal]
--- a/src/HOL/Bali/Eval.thy Tue Mar 18 09:39:07 2014 -0700
+++ b/src/HOL/Bali/Eval.thy Tue Mar 18 21:02:33 2014 +0100
@@ -745,7 +745,7 @@
*)
ML {*
-bind_thm ("eval_induct", rearrange_prems
+ML_Thms.bind_thm ("eval_induct", rearrange_prems
[0,1,2,8,4,30,31,27,15,16,
17,18,19,20,21,3,5,25,26,23,6,
7,11,9,13,14,12,22,10,28,
@@ -881,7 +881,7 @@
| _ => SOME (mk_meta_eq @{thm eval_stmt_eq})) *}
ML {*
-bind_thms ("AbruptIs", sum3_instantiate @{context} @{thm eval.Abrupt})
+ML_Thms.bind_thms ("AbruptIs", sum3_instantiate @{context} @{thm eval.Abrupt})
*}
declare halloc.Abrupt [intro!] eval.Abrupt [intro!] AbruptIs [intro!]
--- a/src/HOL/Bali/Evaln.thy Tue Mar 18 09:39:07 2014 -0700
+++ b/src/HOL/Bali/Evaln.thy Tue Mar 18 21:02:33 2014 +0100
@@ -292,7 +292,7 @@
(_ $ _ $ _ $ _ $ _ $ (Const _ $ _) $ _) => NONE
| _ => SOME (mk_meta_eq @{thm evaln_stmt_eq})) *}
-ML {* bind_thms ("evaln_AbruptIs", sum3_instantiate @{context} @{thm evaln.Abrupt}) *}
+ML {* ML_Thms.bind_thms ("evaln_AbruptIs", sum3_instantiate @{context} @{thm evaln.Abrupt}) *}
declare evaln_AbruptIs [intro!]
lemma evaln_Callee: "G\<turnstile>Norm s\<midarrow>In1l (Callee l e)\<succ>\<midarrow>n\<rightarrow> (v,s') = False"
--- a/src/HOL/Bali/Example.thy Tue Mar 18 09:39:07 2014 -0700
+++ b/src/HOL/Bali/Example.thy Tue Mar 18 21:02:33 2014 +0100
@@ -894,7 +894,7 @@
declare member_is_static_simp [simp]
declare wt.Skip [rule del] wt.Init [rule del]
-ML {* bind_thms ("wt_intros", map (rewrite_rule @{context} @{thms id_def}) @{thms wt.intros}) *}
+ML {* ML_Thms.bind_thms ("wt_intros", map (rewrite_rule @{context} @{thms id_def}) @{thms wt.intros}) *}
lemmas wtIs = wt_Call wt_Super wt_FVar wt_StatRef wt_intros
lemmas daIs = assigned.select_convs da_Skip da_NewC da_Lit da_Super da.intros
@@ -1187,7 +1187,7 @@
declare BaseCl_def [simp] ExtCl_def [simp] Ext_foo_def [simp]
Base_foo_defs [simp]
-ML {* bind_thms ("eval_intros", map
+ML {* ML_Thms.bind_thms ("eval_intros", map
(simplify (@{context} delsimps @{thms Skip_eq} addsimps @{thms lvar_def}) o
rewrite_rule @{context} [@{thm assign_def}, @{thm Let_def}]) @{thms eval.intros}) *}
lemmas eval_Is = eval_Init eval_StatRef AbruptIs eval_intros
--- a/src/HOL/Bali/Term.thy Tue Mar 18 09:39:07 2014 -0700
+++ b/src/HOL/Bali/Term.thy Tue Mar 18 21:02:33 2014 +0100
@@ -262,7 +262,7 @@
is_stmt :: "term \<Rightarrow> bool"
where "is_stmt t = (\<exists>c. t=In1r c)"
-ML {* bind_thms ("is_stmt_rews", sum3_instantiate @{context} @{thm is_stmt_def}) *}
+ML {* ML_Thms.bind_thms ("is_stmt_rews", sum3_instantiate @{context} @{thm is_stmt_def}) *}
declare is_stmt_rews [simp]
--- a/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy Tue Mar 18 09:39:07 2014 -0700
+++ b/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy Tue Mar 18 21:02:33 2014 +0100
@@ -68,43 +68,43 @@
subsection{* Degrees and heads and coefficients *}
-fun degree:: "poly \<Rightarrow> nat"
+fun degree :: "poly \<Rightarrow> nat"
where
"degree (CN c 0 p) = 1 + degree p"
| "degree p = 0"
-fun head:: "poly \<Rightarrow> poly"
+fun head :: "poly \<Rightarrow> poly"
where
"head (CN c 0 p) = head p"
| "head p = p"
(* More general notions of degree and head *)
-fun degreen:: "poly \<Rightarrow> nat \<Rightarrow> nat"
+fun degreen :: "poly \<Rightarrow> nat \<Rightarrow> nat"
where
"degreen (CN c n p) = (\<lambda>m. if n = m then 1 + degreen p n else 0)"
| "degreen p = (\<lambda>m. 0)"
-fun headn:: "poly \<Rightarrow> nat \<Rightarrow> poly"
+fun headn :: "poly \<Rightarrow> nat \<Rightarrow> poly"
where
"headn (CN c n p) = (\<lambda>m. if n \<le> m then headn p m else CN c n p)"
| "headn p = (\<lambda>m. p)"
-fun coefficients:: "poly \<Rightarrow> poly list"
+fun coefficients :: "poly \<Rightarrow> poly list"
where
"coefficients (CN c 0 p) = c # coefficients p"
| "coefficients p = [p]"
-fun isconstant:: "poly \<Rightarrow> bool"
+fun isconstant :: "poly \<Rightarrow> bool"
where
"isconstant (CN c 0 p) = False"
| "isconstant p = True"
-fun behead:: "poly \<Rightarrow> poly"
+fun behead :: "poly \<Rightarrow> poly"
where
"behead (CN c 0 p) = (let p' = behead p in if p' = 0\<^sub>p then c else CN c 0 p')"
| "behead p = 0\<^sub>p"
-fun headconst:: "poly \<Rightarrow> Num"
+fun headconst :: "poly \<Rightarrow> Num"
where
"headconst (CN c n p) = headconst p"
| "headconst (C n) = n"
@@ -679,11 +679,11 @@
shows "isnpolyh p n0 \<Longrightarrow> isnpolyh q n1 \<Longrightarrow> p *\<^sub>p q = 0\<^sub>p \<longleftrightarrow> p = 0\<^sub>p \<or> q = 0\<^sub>p"
using polymul_properties(2) by blast
-lemma polymul_degreen: (* FIXME duplicate? *)
+lemma polymul_degreen:
assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})"
shows "isnpolyh p n0 \<Longrightarrow> isnpolyh q n1 \<Longrightarrow> m \<le> min n0 n1 \<Longrightarrow>
degreen (p *\<^sub>p q) m = (if p = 0\<^sub>p \<or> q = 0\<^sub>p then 0 else degreen p m + degreen q m)"
- using polymul_properties(3) by blast
+ by (fact polymul_properties(3))
lemma polymul_norm:
assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})"
@@ -852,10 +852,10 @@
by (simp add: shift1_def)
lemma shift1_isnpoly:
- assumes pn: "isnpoly p"
- and pnz: "p \<noteq> 0\<^sub>p"
+ assumes "isnpoly p"
+ and "p \<noteq> 0\<^sub>p"
shows "isnpoly (shift1 p) "
- using pn pnz by (simp add: shift1_def isnpoly_def)
+ using assms by (simp add: shift1_def isnpoly_def)
lemma shift1_nz[simp]:"shift1 p \<noteq> 0\<^sub>p"
by (simp add: shift1_def)
@@ -864,10 +864,10 @@
by (induct n arbitrary: p) (auto simp add: shift1_isnpoly funpow_swap1)
lemma funpow_isnpolyh:
- assumes f: "\<And>p. isnpolyh p n \<Longrightarrow> isnpolyh (f p) n"
- and np: "isnpolyh p n"
+ assumes "\<And>p. isnpolyh p n \<Longrightarrow> isnpolyh (f p) n"
+ and "isnpolyh p n"
shows "isnpolyh (funpow k f p) n"
- using f np by (induct k arbitrary: p) auto
+ using assms by (induct k arbitrary: p) auto
lemma funpow_shift1:
"(Ipoly bs (funpow n shift1 p) :: 'a :: {field_char_0,field_inverse_zero}) =
@@ -886,10 +886,10 @@
by (induct p rule: poly_cmul.induct) (auto simp add: field_simps)
lemma behead:
- assumes np: "isnpolyh p n"
+ assumes "isnpolyh p n"
shows "Ipoly bs (Add (Mul (head p) (Pw (Bound 0) (degree p))) (behead p)) =
(Ipoly bs p :: 'a :: {field_char_0,field_inverse_zero})"
- using np
+ using assms
proof (induct p arbitrary: n rule: behead.induct)
case (1 c p n)
then have pn: "isnpolyh p n" by simp
@@ -902,12 +902,12 @@
qed (auto simp add: Let_def)
lemma behead_isnpolyh:
- assumes np: "isnpolyh p n"
+ assumes "isnpolyh p n"
shows "isnpolyh (behead p) n"
- using np by (induct p rule: behead.induct) (auto simp add: Let_def isnpolyh_mono)
+ using assms by (induct p rule: behead.induct) (auto simp add: Let_def isnpolyh_mono)
-subsection{* Miscellaneous lemmas about indexes, decrementation, substitution etc ... *}
+subsection {* Miscellaneous lemmas about indexes, decrementation, substitution etc ... *}
lemma isnpolyh_polybound0: "isnpolyh p (Suc n) \<Longrightarrow> polybound0 p"
proof (induct p arbitrary: n rule: poly.induct, auto)
@@ -938,28 +938,27 @@
by (induct p arbitrary: n0 rule: head.induct) (auto intro: isnpolyh_polybound0)
lemma polybound0_I:
- assumes nb: "polybound0 a"
+ assumes "polybound0 a"
shows "Ipoly (b # bs) a = Ipoly (b' # bs) a"
- using nb
- by (induct a rule: poly.induct) auto
+ using assms by (induct a rule: poly.induct) auto
lemma polysubst0_I: "Ipoly (b # bs) (polysubst0 a t) = Ipoly ((Ipoly (b # bs) a) # bs) t"
by (induct t) simp_all
lemma polysubst0_I':
- assumes nb: "polybound0 a"
+ assumes "polybound0 a"
shows "Ipoly (b # bs) (polysubst0 a t) = Ipoly ((Ipoly (b' # bs) a) # bs) t"
- by (induct t) (simp_all add: polybound0_I[OF nb, where b="b" and b'="b'"])
+ by (induct t) (simp_all add: polybound0_I[OF assms, where b="b" and b'="b'"])
lemma decrpoly:
- assumes nb: "polybound0 t"
+ assumes "polybound0 t"
shows "Ipoly (x # bs) t = Ipoly bs (decrpoly t)"
- using nb by (induct t rule: decrpoly.induct) simp_all
+ using assms by (induct t rule: decrpoly.induct) simp_all
lemma polysubst0_polybound0:
- assumes nb: "polybound0 t"
+ assumes "polybound0 t"
shows "polybound0 (polysubst0 t a)"
- using nb by (induct a rule: poly.induct) auto
+ using assms by (induct a rule: poly.induct) auto
lemma degree0_polybound0: "isnpolyh p n \<Longrightarrow> degree p = 0 \<Longrightarrow> polybound0 p"
by (induct p arbitrary: n rule: degree.induct) (auto simp add: isnpolyh_polybound0)
@@ -1034,10 +1033,10 @@
lemma wf_bs_insensitive: "length bs = length bs' \<Longrightarrow> wf_bs bs p = wf_bs bs' p"
unfolding wf_bs_def by simp
-lemma wf_bs_insensitive': "wf_bs (x#bs) p = wf_bs (y#bs) p"
+lemma wf_bs_insensitive': "wf_bs (x # bs) p = wf_bs (y # bs) p"
unfolding wf_bs_def by simp
-lemma wf_bs_coefficients': "\<forall>c \<in> set (coefficients p). wf_bs bs c \<Longrightarrow> wf_bs (x#bs) p"
+lemma wf_bs_coefficients': "\<forall>c \<in> set (coefficients p). wf_bs bs c \<Longrightarrow> wf_bs (x # bs) p"
by (induct p rule: coefficients.induct) (auto simp add: wf_bs_def)
lemma coefficients_Nil[simp]: "coefficients p \<noteq> []"
@@ -1046,11 +1045,11 @@
lemma coefficients_head: "last (coefficients p) = head p"
by (induct p rule: coefficients.induct) auto
-lemma wf_bs_decrpoly: "wf_bs bs (decrpoly p) \<Longrightarrow> wf_bs (x#bs) p"
+lemma wf_bs_decrpoly: "wf_bs bs (decrpoly p) \<Longrightarrow> wf_bs (x # bs) p"
unfolding wf_bs_def by (induct p rule: decrpoly.induct) auto
lemma length_le_list_ex: "length xs \<le> n \<Longrightarrow> \<exists>ys. length (xs @ ys) = n"
- apply (rule exI[where x="replicate (n - length xs) z"])
+ apply (rule exI[where x="replicate (n - length xs) z" for z])
apply simp
done
@@ -1481,7 +1480,8 @@
lemma funpow_shift1_head: "isnpolyh p n0 \<Longrightarrow> p\<noteq> 0\<^sub>p \<Longrightarrow> head (funpow k shift1 p) = head p"
proof (induct k arbitrary: n0 p)
case 0
- then show ?case by auto
+ then show ?case
+ by auto
next
case (Suc k n0 p)
then have "isnpolyh (shift1 p) 0"
@@ -1522,7 +1522,6 @@
shows "head (p +\<^sub>p q) = (if degree p < degree q then head q else head p)"
using np nq deg
apply (induct p q arbitrary: n0 n1 rule: polyadd.induct)
- using np
apply simp_all
apply (case_tac n', simp, simp)
apply (case_tac n, simp, simp)
@@ -1646,7 +1645,7 @@
lemma polyneg_degree: "isnpolyh p n \<Longrightarrow> degree (polyneg p) = degree p"
by (induct p arbitrary: n rule: degree.induct) auto
-lemma polyneg_head: "isnpolyh p n \<Longrightarrow> head(polyneg p) = polyneg (head p)"
+lemma polyneg_head: "isnpolyh p n \<Longrightarrow> head (polyneg p) = polyneg (head p)"
by (induct p arbitrary: n rule: degree.induct) auto
@@ -1657,8 +1656,9 @@
and np: "isnpolyh p n0"
and ns: "isnpolyh s n1"
and ap: "head p = a"
- and ndp: "degree p = n" and pnz: "p \<noteq> 0\<^sub>p"
- shows "polydivide_aux a n p k s = (k',r) \<longrightarrow> k' \<ge> k \<and> (degree r = 0 \<or> degree r < degree p) \<and>
+ and ndp: "degree p = n"
+ and pnz: "p \<noteq> 0\<^sub>p"
+ shows "polydivide_aux a n p k s = (k', r) \<longrightarrow> k' \<ge> k \<and> (degree r = 0 \<or> degree r < degree p) \<and>
(\<exists>nr. isnpolyh r nr) \<and> (\<exists>q n1. isnpolyh q n1 \<and> (polypow (k' - k) a) *\<^sub>p s = p *\<^sub>p q +\<^sub>p r)"
using ns
proof (induct "degree s" arbitrary: s k k' r n1 rule: less_induct)
@@ -1718,7 +1718,8 @@
have nr: "isnpolyh (s -\<^sub>p ?p') 0"
using polysub_normh[OF ns np'] by simp
from degree_polysub_samehead[OF ns np' headsp' degsp']
- have "degree (s -\<^sub>p ?p') < degree s \<or> s -\<^sub>p ?p' = 0\<^sub>p" by simp
+ have "degree (s -\<^sub>p ?p') < degree s \<or> s -\<^sub>p ?p' = 0\<^sub>p"
+ by simp
moreover
{
assume deglt:"degree (s -\<^sub>p ?p') < degree s"
@@ -1798,7 +1799,7 @@
using isnpolyh_unique[OF ns polymul_normh[OF nxdn np]]
by blast
{
- assume h1: "polydivide_aux a n p k s = (k',r)"
+ assume h1: "polydivide_aux a n p k s = (k', r)"
from polydivide_aux.simps sz dn' ba
have eq: "polydivide_aux a n p k s = polydivide_aux a n p k (s -\<^sub>p ?p')"
by (simp add: Let_def)
@@ -1877,11 +1878,11 @@
by (simp add: field_simps)
}
then have ieq:"\<forall>bs :: 'a::{field_char_0,field_inverse_zero} list.
- Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) =
- Ipoly bs (p *\<^sub>p (q +\<^sub>p (a ^\<^sub>p (k' - Suc k) *\<^sub>p ?b *\<^sub>p ?xdn)) +\<^sub>p r)"
+ Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) =
+ Ipoly bs (p *\<^sub>p (q +\<^sub>p (a ^\<^sub>p (k' - Suc k) *\<^sub>p ?b *\<^sub>p ?xdn)) +\<^sub>p r)"
by auto
let ?q = "q +\<^sub>p (a ^\<^sub>p (k' - Suc k) *\<^sub>p ?b *\<^sub>p ?xdn)"
- from polyadd_normh[OF nq polymul_normh[OF polymul_normh[OF polypow_normh[OF head_isnpolyh[OF np], where k="k' - Suc k"] head_isnpolyh[OF ns], simplified ap ] nxdn]]
+ from polyadd_normh[OF nq polymul_normh[OF polymul_normh[OF polypow_normh[OF head_isnpolyh[OF np], where k="k' - Suc k"] head_isnpolyh[OF ns], simplified ap] nxdn]]
have nqw: "isnpolyh ?q 0"
by simp
from ieq isnpolyh_unique[OF polymul_normh[OF polypow_normh[OF head_isnpolyh[OF np], where k="k' - k"] ns, simplified ap] polyadd_normh[OF polymul_normh[OF np nqw] nr]]
@@ -1979,13 +1980,13 @@
definition "isnonconstant p \<longleftrightarrow> \<not> isconstant p"
lemma isnonconstant_pnormal_iff:
- assumes nc: "isnonconstant p"
+ assumes "isnonconstant p"
shows "pnormal (polypoly bs p) \<longleftrightarrow> Ipoly bs (head p) \<noteq> 0"
proof
let ?p = "polypoly bs p"
assume H: "pnormal ?p"
have csz: "coefficients p \<noteq> []"
- using nc by (cases p) auto
+ using assms by (cases p) auto
from coefficients_head[of p] last_map[OF csz, of "Ipoly bs"] pnormal_last_nonzero[OF H]
show "Ipoly bs (head p) \<noteq> 0"
by (simp add: polypoly_def)
@@ -1993,7 +1994,7 @@
assume h: "\<lparr>head p\<rparr>\<^sub>p\<^bsup>bs\<^esup> \<noteq> 0"
let ?p = "polypoly bs p"
have csz: "coefficients p \<noteq> []"
- using nc by (cases p) auto
+ using assms by (cases p) auto
then have pz: "?p \<noteq> []"
by (simp add: polypoly_def)
then have lg: "length ?p > 0"
@@ -2013,18 +2014,18 @@
done
lemma isnonconstant_nonconstant:
- assumes inc: "isnonconstant p"
+ assumes "isnonconstant p"
shows "nonconstant (polypoly bs p) \<longleftrightarrow> Ipoly bs (head p) \<noteq> 0"
proof
let ?p = "polypoly bs p"
assume nc: "nonconstant ?p"
- from isnonconstant_pnormal_iff[OF inc, of bs] nc
+ from isnonconstant_pnormal_iff[OF assms, of bs] nc
show "\<lparr>head p\<rparr>\<^sub>p\<^bsup>bs\<^esup> \<noteq> 0"
unfolding nonconstant_def by blast
next
let ?p = "polypoly bs p"
assume h: "\<lparr>head p\<rparr>\<^sub>p\<^bsup>bs\<^esup> \<noteq> 0"
- from isnonconstant_pnormal_iff[OF inc, of bs] h
+ from isnonconstant_pnormal_iff[OF assms, of bs] h
have pn: "pnormal ?p"
by blast
{
@@ -2032,8 +2033,8 @@
assume H: "?p = [x]"
from H have "length (coefficients p) = 1"
unfolding polypoly_def by auto
- with isnonconstant_coefficients_length[OF inc]
- have False by arith
+ with isnonconstant_coefficients_length[OF assms]
+ have False by arith
}
then show "nonconstant ?p"
using pn unfolding nonconstant_def by blast
@@ -2047,26 +2048,26 @@
done
lemma degree_degree:
- assumes inc: "isnonconstant p"
+ assumes "isnonconstant p"
shows "degree p = Polynomial_List.degree (polypoly bs p) \<longleftrightarrow> \<lparr>head p\<rparr>\<^sub>p\<^bsup>bs\<^esup> \<noteq> 0"
proof
let ?p = "polypoly bs p"
assume H: "degree p = Polynomial_List.degree ?p"
- from isnonconstant_coefficients_length[OF inc] have pz: "?p \<noteq> []"
+ from isnonconstant_coefficients_length[OF assms] have pz: "?p \<noteq> []"
unfolding polypoly_def by auto
- from H degree_coefficients[of p] isnonconstant_coefficients_length[OF inc]
+ from H degree_coefficients[of p] isnonconstant_coefficients_length[OF assms]
have lg: "length (pnormalize ?p) = length ?p"
unfolding Polynomial_List.degree_def polypoly_def by simp
then have "pnormal ?p"
using pnormal_length[OF pz] by blast
- with isnonconstant_pnormal_iff[OF inc] show "\<lparr>head p\<rparr>\<^sub>p\<^bsup>bs\<^esup> \<noteq> 0"
+ with isnonconstant_pnormal_iff[OF assms] show "\<lparr>head p\<rparr>\<^sub>p\<^bsup>bs\<^esup> \<noteq> 0"
by blast
next
let ?p = "polypoly bs p"
assume H: "\<lparr>head p\<rparr>\<^sub>p\<^bsup>bs\<^esup> \<noteq> 0"
- with isnonconstant_pnormal_iff[OF inc] have "pnormal ?p"
+ with isnonconstant_pnormal_iff[OF assms] have "pnormal ?p"
by blast
- with degree_coefficients[of p] isnonconstant_coefficients_length[OF inc]
+ with degree_coefficients[of p] isnonconstant_coefficients_length[OF assms]
show "degree p = Polynomial_List.degree ?p"
unfolding polypoly_def pnormal_def Polynomial_List.degree_def by auto
qed
@@ -2077,7 +2078,7 @@
primrec swap :: "nat \<Rightarrow> nat \<Rightarrow> poly \<Rightarrow> poly"
where
"swap n m (C x) = C x"
-| "swap n m (Bound k) = Bound (if k = n then m else if k=m then n else k)"
+| "swap n m (Bound k) = Bound (if k = n then m else if k = m then n else k)"
| "swap n m (Neg t) = Neg (swap n m t)"
| "swap n m (Add s t) = Add (swap n m s) (swap n m t)"
| "swap n m (Sub s t) = Sub (swap n m s) (swap n m t)"
--- a/src/HOL/SMT_Examples/boogie.ML Tue Mar 18 09:39:07 2014 -0700
+++ b/src/HOL/SMT_Examples/boogie.ML Tue Mar 18 21:02:33 2014 +0100
@@ -317,7 +317,7 @@
val _ =
Outer_Syntax.command @{command_spec "boogie_file"}
"prove verification condition from .b2i file"
- (Thy_Load.provide_parse_files "boogie_file" >> (fn files =>
+ (Resources.provide_parse_files "boogie_file" >> (fn files =>
Toplevel.theory (fn thy =>
let
val ([{lines, ...}], thy') = files thy;
--- a/src/HOL/SPARK/Tools/spark_commands.ML Tue Mar 18 09:39:07 2014 -0700
+++ b/src/HOL/SPARK/Tools/spark_commands.ML Tue Mar 18 21:02:33 2014 +0100
@@ -12,7 +12,7 @@
val ([{src_path, lines = vc_lines, pos = vc_pos, ...}: Token.file,
{lines = fdl_lines, pos = fdl_pos, ...},
{lines = rls_lines, pos = rls_pos, ...}], thy') = files thy;
- val base = fst (Path.split_ext (File.full_path (Thy_Load.master_directory thy') src_path));
+ val base = fst (Path.split_ext (File.full_path (Resources.master_directory thy') src_path));
in
SPARK_VCs.set_vcs
(snd (Fdl_Parser.parse_declarations fdl_pos (cat_lines fdl_lines)))
@@ -24,7 +24,7 @@
(* FIXME *)
fun spark_open_old (vc_name, prfx) thy =
let
- val ((vc_path, vc_id), vc_text) = Thy_Load.load_file thy (Path.explode vc_name);
+ val ((vc_path, vc_id), vc_text) = Resources.load_file thy (Path.explode vc_name);
val (base, header) =
(case Path.split_ext vc_path of
(base, "vcg") => (base, Fdl_Lexer.vcg_header >> K ())
@@ -117,13 +117,13 @@
val _ =
Outer_Syntax.command @{command_spec "spark_open_vcg"}
"open a new SPARK environment and load a SPARK-generated .vcg file"
- (Parse.parname -- Thy_Load.provide_parse_files "spark_open_vcg"
+ (Parse.parname -- Resources.provide_parse_files "spark_open_vcg"
>> (Toplevel.theory o spark_open Fdl_Lexer.vcg_header));
val _ =
Outer_Syntax.command @{command_spec "spark_open_siv"}
"open a new SPARK environment and load a SPARK-generated .siv file"
- (Parse.parname -- Thy_Load.provide_parse_files "spark_open_siv"
+ (Parse.parname -- Resources.provide_parse_files "spark_open_siv"
>> (Toplevel.theory o spark_open Fdl_Lexer.siv_header));
val pfun_type = Scan.option
--- a/src/HOL/Tools/SMT/smt_config.ML Tue Mar 18 09:39:07 2014 -0700
+++ b/src/HOL/Tools/SMT/smt_config.ML Tue Mar 18 21:02:33 2014 +0100
@@ -198,7 +198,7 @@
if name = "" then NONE
else
Path.explode name
- |> Path.append (Thy_Load.master_directory (Context.theory_of context))
+ |> Path.append (Resources.master_directory (Context.theory_of context))
|> SOME o Cache_IO.unsynchronized_init)
val certificates_of = Certificates.get o Context.Proof
--- a/src/HOL/Tools/SMT2/smt2_config.ML Tue Mar 18 09:39:07 2014 -0700
+++ b/src/HOL/Tools/SMT2/smt2_config.ML Tue Mar 18 21:02:33 2014 +0100
@@ -195,7 +195,7 @@
if name = "" then NONE
else
Path.explode name
- |> Path.append (Thy_Load.master_directory (Context.theory_of context))
+ |> Path.append (Resources.master_directory (Context.theory_of context))
|> SOME o Cache_IO.unsynchronized_init)
val certificates_of = Certificates.get o Context.Proof
--- a/src/HOL/Tools/recdef.ML Tue Mar 18 09:39:07 2014 -0700
+++ b/src/HOL/Tools/recdef.ML Tue Mar 18 21:02:33 2014 +0100
@@ -290,7 +290,7 @@
val hints =
@{keyword "("} |--
- Parse.!!! (Parse.position @{keyword "hints"} -- Args.parse --| @{keyword ")"})
+ Parse.!!! (Parse.position @{keyword "hints"} -- Parse.args --| @{keyword ")"})
>> uncurry Args.src;
val recdef_decl =
--- a/src/HOL/UNITY/Comp/Alloc.thy Tue Mar 18 09:39:07 2014 -0700
+++ b/src/HOL/UNITY/Comp/Alloc.thy Tue Mar 18 21:02:33 2014 +0100
@@ -425,7 +425,7 @@
apply (rule fst_o_funPair)
done
-ML {* bind_thms ("fst_o_client_map'", make_o_equivs @{context} @{thm fst_o_client_map}) *}
+ML {* ML_Thms.bind_thms ("fst_o_client_map'", make_o_equivs @{context} @{thm fst_o_client_map}) *}
declare fst_o_client_map' [simp]
lemma snd_o_client_map: "snd o client_map = clientState_d.dummy"
@@ -433,7 +433,7 @@
apply (rule snd_o_funPair)
done
-ML {* bind_thms ("snd_o_client_map'", make_o_equivs @{context} @{thm snd_o_client_map}) *}
+ML {* ML_Thms.bind_thms ("snd_o_client_map'", make_o_equivs @{context} @{thm snd_o_client_map}) *}
declare snd_o_client_map' [simp]
@@ -443,28 +443,28 @@
apply record_auto
done
-ML {* bind_thms ("client_o_sysOfAlloc'", make_o_equivs @{context} @{thm client_o_sysOfAlloc}) *}
+ML {* ML_Thms.bind_thms ("client_o_sysOfAlloc'", make_o_equivs @{context} @{thm client_o_sysOfAlloc}) *}
declare client_o_sysOfAlloc' [simp]
lemma allocGiv_o_sysOfAlloc_eq: "allocGiv o sysOfAlloc = allocGiv"
apply record_auto
done
-ML {* bind_thms ("allocGiv_o_sysOfAlloc_eq'", make_o_equivs @{context} @{thm allocGiv_o_sysOfAlloc_eq}) *}
+ML {* ML_Thms.bind_thms ("allocGiv_o_sysOfAlloc_eq'", make_o_equivs @{context} @{thm allocGiv_o_sysOfAlloc_eq}) *}
declare allocGiv_o_sysOfAlloc_eq' [simp]
lemma allocAsk_o_sysOfAlloc_eq: "allocAsk o sysOfAlloc = allocAsk"
apply record_auto
done
-ML {* bind_thms ("allocAsk_o_sysOfAlloc_eq'", make_o_equivs @{context} @{thm allocAsk_o_sysOfAlloc_eq}) *}
+ML {* ML_Thms.bind_thms ("allocAsk_o_sysOfAlloc_eq'", make_o_equivs @{context} @{thm allocAsk_o_sysOfAlloc_eq}) *}
declare allocAsk_o_sysOfAlloc_eq' [simp]
lemma allocRel_o_sysOfAlloc_eq: "allocRel o sysOfAlloc = allocRel"
apply record_auto
done
-ML {* bind_thms ("allocRel_o_sysOfAlloc_eq'", make_o_equivs @{context} @{thm allocRel_o_sysOfAlloc_eq}) *}
+ML {* ML_Thms.bind_thms ("allocRel_o_sysOfAlloc_eq'", make_o_equivs @{context} @{thm allocRel_o_sysOfAlloc_eq}) *}
declare allocRel_o_sysOfAlloc_eq' [simp]
@@ -474,49 +474,49 @@
apply record_auto
done
-ML {* bind_thms ("client_o_sysOfClient'", make_o_equivs @{context} @{thm client_o_sysOfClient}) *}
+ML {* ML_Thms.bind_thms ("client_o_sysOfClient'", make_o_equivs @{context} @{thm client_o_sysOfClient}) *}
declare client_o_sysOfClient' [simp]
lemma allocGiv_o_sysOfClient_eq: "allocGiv o sysOfClient = allocGiv o snd "
apply record_auto
done
-ML {* bind_thms ("allocGiv_o_sysOfClient_eq'", make_o_equivs @{context} @{thm allocGiv_o_sysOfClient_eq}) *}
+ML {* ML_Thms.bind_thms ("allocGiv_o_sysOfClient_eq'", make_o_equivs @{context} @{thm allocGiv_o_sysOfClient_eq}) *}
declare allocGiv_o_sysOfClient_eq' [simp]
lemma allocAsk_o_sysOfClient_eq: "allocAsk o sysOfClient = allocAsk o snd "
apply record_auto
done
-ML {* bind_thms ("allocAsk_o_sysOfClient_eq'", make_o_equivs @{context} @{thm allocAsk_o_sysOfClient_eq}) *}
+ML {* ML_Thms.bind_thms ("allocAsk_o_sysOfClient_eq'", make_o_equivs @{context} @{thm allocAsk_o_sysOfClient_eq}) *}
declare allocAsk_o_sysOfClient_eq' [simp]
lemma allocRel_o_sysOfClient_eq: "allocRel o sysOfClient = allocRel o snd "
apply record_auto
done
-ML {* bind_thms ("allocRel_o_sysOfClient_eq'", make_o_equivs @{context} @{thm allocRel_o_sysOfClient_eq}) *}
+ML {* ML_Thms.bind_thms ("allocRel_o_sysOfClient_eq'", make_o_equivs @{context} @{thm allocRel_o_sysOfClient_eq}) *}
declare allocRel_o_sysOfClient_eq' [simp]
lemma allocGiv_o_inv_sysOfAlloc_eq: "allocGiv o inv sysOfAlloc = allocGiv"
apply (simp add: o_def)
done
-ML {* bind_thms ("allocGiv_o_inv_sysOfAlloc_eq'", make_o_equivs @{context} @{thm allocGiv_o_inv_sysOfAlloc_eq}) *}
+ML {* ML_Thms.bind_thms ("allocGiv_o_inv_sysOfAlloc_eq'", make_o_equivs @{context} @{thm allocGiv_o_inv_sysOfAlloc_eq}) *}
declare allocGiv_o_inv_sysOfAlloc_eq' [simp]
lemma allocAsk_o_inv_sysOfAlloc_eq: "allocAsk o inv sysOfAlloc = allocAsk"
apply (simp add: o_def)
done
-ML {* bind_thms ("allocAsk_o_inv_sysOfAlloc_eq'", make_o_equivs @{context} @{thm allocAsk_o_inv_sysOfAlloc_eq}) *}
+ML {* ML_Thms.bind_thms ("allocAsk_o_inv_sysOfAlloc_eq'", make_o_equivs @{context} @{thm allocAsk_o_inv_sysOfAlloc_eq}) *}
declare allocAsk_o_inv_sysOfAlloc_eq' [simp]
lemma allocRel_o_inv_sysOfAlloc_eq: "allocRel o inv sysOfAlloc = allocRel"
apply (simp add: o_def)
done
-ML {* bind_thms ("allocRel_o_inv_sysOfAlloc_eq'", make_o_equivs @{context} @{thm allocRel_o_inv_sysOfAlloc_eq}) *}
+ML {* ML_Thms.bind_thms ("allocRel_o_inv_sysOfAlloc_eq'", make_o_equivs @{context} @{thm allocRel_o_inv_sysOfAlloc_eq}) *}
declare allocRel_o_inv_sysOfAlloc_eq' [simp]
lemma rel_inv_client_map_drop_map: "(rel o inv client_map o drop_map i o inv sysOfClient) =
@@ -524,7 +524,7 @@
apply (simp add: o_def drop_map_def)
done
-ML {* bind_thms ("rel_inv_client_map_drop_map'", make_o_equivs @{context} @{thm rel_inv_client_map_drop_map}) *}
+ML {* ML_Thms.bind_thms ("rel_inv_client_map_drop_map'", make_o_equivs @{context} @{thm rel_inv_client_map_drop_map}) *}
declare rel_inv_client_map_drop_map [simp]
lemma ask_inv_client_map_drop_map: "(ask o inv client_map o drop_map i o inv sysOfClient) =
@@ -532,7 +532,7 @@
apply (simp add: o_def drop_map_def)
done
-ML {* bind_thms ("ask_inv_client_map_drop_map'", make_o_equivs @{context} @{thm ask_inv_client_map_drop_map}) *}
+ML {* ML_Thms.bind_thms ("ask_inv_client_map_drop_map'", make_o_equivs @{context} @{thm ask_inv_client_map_drop_map}) *}
declare ask_inv_client_map_drop_map [simp]
@@ -549,13 +549,13 @@
@{thm Client} |> simplify (@{context} addsimps @{thms client_spec_simps})
|> list_of_Int;
-bind_thm ("Client_Increasing_ask", Client_Increasing_ask);
-bind_thm ("Client_Increasing_rel", Client_Increasing_rel);
-bind_thm ("Client_Bounded", Client_Bounded);
-bind_thm ("Client_Progress", Client_Progress);
-bind_thm ("Client_AllowedActs", Client_AllowedActs);
-bind_thm ("Client_preserves_giv", Client_preserves_giv);
-bind_thm ("Client_preserves_dummy", Client_preserves_dummy);
+ML_Thms.bind_thm ("Client_Increasing_ask", Client_Increasing_ask);
+ML_Thms.bind_thm ("Client_Increasing_rel", Client_Increasing_rel);
+ML_Thms.bind_thm ("Client_Bounded", Client_Bounded);
+ML_Thms.bind_thm ("Client_Progress", Client_Progress);
+ML_Thms.bind_thm ("Client_AllowedActs", Client_AllowedActs);
+ML_Thms.bind_thm ("Client_preserves_giv", Client_preserves_giv);
+ML_Thms.bind_thm ("Client_preserves_dummy", Client_preserves_dummy);
*}
declare
@@ -579,13 +579,13 @@
@{thm Network} |> simplify (@{context} addsimps @{thms network_spec_simps})
|> list_of_Int;
-bind_thm ("Network_Ask", Network_Ask);
-bind_thm ("Network_Giv", Network_Giv);
-bind_thm ("Network_Rel", Network_Rel);
-bind_thm ("Network_AllowedActs", Network_AllowedActs);
-bind_thm ("Network_preserves_allocGiv", Network_preserves_allocGiv);
-bind_thm ("Network_preserves_rel", Network_preserves_rel);
-bind_thm ("Network_preserves_ask", Network_preserves_ask);
+ML_Thms.bind_thm ("Network_Ask", Network_Ask);
+ML_Thms.bind_thm ("Network_Giv", Network_Giv);
+ML_Thms.bind_thm ("Network_Rel", Network_Rel);
+ML_Thms.bind_thm ("Network_AllowedActs", Network_AllowedActs);
+ML_Thms.bind_thm ("Network_preserves_allocGiv", Network_preserves_allocGiv);
+ML_Thms.bind_thm ("Network_preserves_rel", Network_preserves_rel);
+ML_Thms.bind_thm ("Network_preserves_ask", Network_preserves_ask);
*}
declare Network_preserves_allocGiv [iff]
@@ -610,13 +610,13 @@
@{thm Alloc} |> simplify (@{context} addsimps @{thms alloc_spec_simps})
|> list_of_Int;
-bind_thm ("Alloc_Increasing_0", Alloc_Increasing_0);
-bind_thm ("Alloc_Safety", Alloc_Safety);
-bind_thm ("Alloc_Progress", Alloc_Progress);
-bind_thm ("Alloc_AllowedActs", Alloc_AllowedActs);
-bind_thm ("Alloc_preserves_allocRel", Alloc_preserves_allocRel);
-bind_thm ("Alloc_preserves_allocAsk", Alloc_preserves_allocAsk);
-bind_thm ("Alloc_preserves_dummy", Alloc_preserves_dummy);
+ML_Thms.bind_thm ("Alloc_Increasing_0", Alloc_Increasing_0);
+ML_Thms.bind_thm ("Alloc_Safety", Alloc_Safety);
+ML_Thms.bind_thm ("Alloc_Progress", Alloc_Progress);
+ML_Thms.bind_thm ("Alloc_AllowedActs", Alloc_AllowedActs);
+ML_Thms.bind_thm ("Alloc_preserves_allocRel", Alloc_preserves_allocRel);
+ML_Thms.bind_thm ("Alloc_preserves_allocAsk", Alloc_preserves_allocAsk);
+ML_Thms.bind_thm ("Alloc_preserves_dummy", Alloc_preserves_dummy);
*}
text{*Strip off the INT in the guarantees postcondition*}
@@ -808,7 +808,7 @@
ML {*
-bind_thms ("System_Increasing'", list_of_Int @{thm System_Increasing})
+ML_Thms.bind_thms ("System_Increasing'", list_of_Int @{thm System_Increasing})
*}
declare System_Increasing' [intro!]
--- a/src/Pure/Isar/args.ML Tue Mar 18 09:39:07 2014 -0700
+++ b/src/Pure/Isar/args.ML Tue Mar 18 21:02:33 2014 +0100
@@ -61,12 +61,8 @@
val type_name: {proper: bool, strict: bool} -> string context_parser
val const: {proper: bool, strict: bool} -> string context_parser
val goal_spec: ((int -> tactic) -> tactic) context_parser
- val parse: Token.T list parser
- val parse1: (string -> bool) -> Token.T list parser
val attribs: (xstring * Position.T -> string) -> src list parser
val opt_attribs: (xstring * Position.T -> string) -> src list parser
- val thm_name: (xstring * Position.T -> string) -> string -> (binding * src list) parser
- val opt_thm_name: (xstring * Position.T -> string) -> string -> (binding * src list) parser
val syntax_generic: 'a context_parser -> src -> Context.generic -> 'a * Context.generic
val syntax: 'a context_parser -> src -> Proof.context -> 'a * Proof.context
end;
@@ -151,21 +147,19 @@
(* basic *)
-fun token atom = Scan.ahead Parse.not_eof --| atom;
-
-val ident = token
+val ident = Parse.token
(Parse.short_ident || Parse.long_ident || Parse.sym_ident || Parse.term_var ||
Parse.type_ident || Parse.type_var || Parse.number);
-val string = token (Parse.string || Parse.verbatim);
-val alt_string = token Parse.alt_string;
-val symbolic = token (Parse.keyword_with Token.ident_or_symbolic);
+val string = Parse.token (Parse.string || Parse.verbatim);
+val alt_string = Parse.token Parse.alt_string;
+val symbolic = Parse.token (Parse.keyword_with Token.ident_or_symbolic);
fun $$$ x =
- (ident || token Parse.keyword) :|-- (fn tok =>
+ (ident || Parse.token Parse.keyword) :|-- (fn tok =>
let val y = Token.content_of tok in
if x = y
- then (Token.assign (SOME (Token.Literal Markup.quasi_keyword)) tok; Scan.succeed x)
+ then (Token.assign (SOME (Token.Literal (false, Markup.quasi_keyword))) tok; Scan.succeed x)
else Scan.fail
end);
@@ -185,7 +179,7 @@
fun mode s = Scan.optional (parens ($$$ s) >> K true) false;
fun maybe scan = $$$ "_" >> K NONE || scan >> SOME;
-val cartouche = token Parse.cartouche;
+val cartouche = Parse.token Parse.cartouche;
val cartouche_inner_syntax = cartouche >> Token.inner_syntax_of;
val cartouche_source_position = cartouche >> Token.source_position_of;
@@ -257,63 +251,22 @@
Parse.nat >> (fn i => fn tac => tac i) ||
$$$ "!" >> K ALLGOALS;
-val goal = $$$ "[" |-- Parse.!!! (from_to --| $$$ "]");
+val goal = Parse.keyword_improper "[" |-- Parse.!!! (from_to --| Parse.keyword_improper "]");
fun goal_spec x = Scan.lift (Scan.optional goal (fn tac => tac 1)) x;
-(* arguments within outer syntax *)
-
-val argument_kinds =
- [Token.Ident, Token.LongIdent, Token.SymIdent, Token.Var, Token.TypeIdent, Token.TypeVar,
- Token.Nat, Token.Float, Token.String, Token.AltString, Token.Cartouche, Token.Verbatim];
-
-fun parse_args is_symid =
- let
- fun argument blk =
- Parse.group (fn () => "argument")
- (Scan.one (fn tok =>
- let val kind = Token.kind_of tok in
- member (op =) argument_kinds kind orelse
- Token.keyword_with is_symid tok orelse
- (blk andalso Token.keyword_with (fn s => s = ",") tok)
- end));
-
- fun args blk x = Scan.optional (args1 blk) [] x
- and args1 blk x =
- ((Scan.repeat1
- (Scan.repeat1 (argument blk) ||
- argsp "(" ")" ||
- argsp "[" "]")) >> flat) x
- and argsp l r x =
- (token (Parse.$$$ l) ::: Parse.!!! (args true @@@ (token (Parse.$$$ r) >> single))) x;
- in (args, args1) end;
-
-val parse = #1 (parse_args Token.ident_or_symbolic) false;
-fun parse1 is_symid = #2 (parse_args is_symid) false;
-
-
(* attributes *)
fun attribs check =
let
fun intern tok = check (Token.content_of tok, Token.pos_of tok);
val attrib_name = internal_text || (symbolic || named) >> evaluate Token.Text intern;
- val attrib = Parse.position attrib_name -- Parse.!!! parse >> uncurry src;
+ val attrib = Parse.position attrib_name -- Parse.!!! Parse.args >> uncurry src;
in $$$ "[" |-- Parse.!!! (Parse.list attrib --| $$$ "]") end;
fun opt_attribs check = Scan.optional (attribs check) [];
-(* theorem specifications *)
-
-fun thm_name check_attrib s = binding -- opt_attribs check_attrib --| $$$ s;
-
-fun opt_thm_name check_attrib s =
- Scan.optional
- ((binding -- opt_attribs check_attrib || attribs check_attrib >> pair Binding.empty) --| $$$ s)
- (Binding.empty, []);
-
-
(** syntax wrapper **)
--- a/src/Pure/Isar/class.ML Tue Mar 18 09:39:07 2014 -0700
+++ b/src/Pure/Isar/class.ML Tue Mar 18 21:02:33 2014 +0100
@@ -666,9 +666,9 @@
default_intro_tac ctxt facts;
val _ = Theory.setup
- (Method.setup (Binding.name "intro_classes") (Scan.succeed (K (METHOD intro_classes_tac)))
+ (Method.setup @{binding intro_classes} (Scan.succeed (K (METHOD intro_classes_tac)))
"back-chain introduction rules of classes" #>
- Method.setup (Binding.name "default") (Attrib.thms >> (METHOD oo default_tac))
+ Method.setup @{binding default} (Attrib.thms >> (METHOD oo default_tac))
"apply some intro/elim rule");
end;
--- a/src/Pure/Isar/code.ML Tue Mar 18 09:39:07 2014 -0700
+++ b/src/Pure/Isar/code.ML Tue Mar 18 21:02:33 2014 +0100
@@ -1285,7 +1285,7 @@
|| Scan.succeed (mk_attribute add_eqn_maybe_abs);
in
Datatype_Interpretation.init
- #> Attrib.setup (Binding.name "code") (Scan.lift code_attribute_parser)
+ #> Attrib.setup @{binding code} (Scan.lift code_attribute_parser)
"declare theorems for code generation"
end);
--- a/src/Pure/Isar/context_rules.ML Tue Mar 18 09:39:07 2014 -0700
+++ b/src/Pure/Isar/context_rules.ML Tue Mar 18 21:02:33 2014 +0100
@@ -209,13 +209,13 @@
Scan.option Parse.nat) >> (fn (f, n) => f n)) x;
val _ = Theory.setup
- (Attrib.setup (Binding.name "intro") (add intro_bang intro intro_query)
+ (Attrib.setup @{binding intro} (add intro_bang intro intro_query)
"declaration of introduction rule" #>
- Attrib.setup (Binding.name "elim") (add elim_bang elim elim_query)
+ Attrib.setup @{binding elim} (add elim_bang elim elim_query)
"declaration of elimination rule" #>
- Attrib.setup (Binding.name "dest") (add dest_bang dest dest_query)
+ Attrib.setup @{binding dest} (add dest_bang dest dest_query)
"declaration of destruction rule" #>
- Attrib.setup (Binding.name "rule") (Scan.lift Args.del >> K rule_del)
+ Attrib.setup @{binding rule} (Scan.lift Args.del >> K rule_del)
"remove declaration of intro/elim/dest rule");
end;
--- a/src/Pure/Isar/isar_cmd.ML Tue Mar 18 09:39:07 2014 -0700
+++ b/src/Pure/Isar/isar_cmd.ML Tue Mar 18 21:02:33 2014 +0100
@@ -247,9 +247,9 @@
handle Toplevel.UNDEF => error "No goal present";
val _ = Theory.setup
- (ML_Antiquotation.value (Binding.qualify true "Isar" (Binding.name "state"))
+ (ML_Antiquotation.value (Binding.qualify true "Isar" @{binding state})
(Scan.succeed "Isar_Cmd.diag_state ML_context") #>
- ML_Antiquotation.value (Binding.qualify true "Isar" (Binding.name "goal"))
+ ML_Antiquotation.value (Binding.qualify true "Isar" @{binding goal})
(Scan.succeed "Isar_Cmd.diag_goal ML_context"));
--- a/src/Pure/Isar/locale.ML Tue Mar 18 09:39:07 2014 -0700
+++ b/src/Pure/Isar/locale.ML Tue Mar 18 21:02:33 2014 +0100
@@ -622,9 +622,9 @@
val try_intro_locales_tac= gen_intro_locales_tac Method.try_intros_tac;
val _ = Theory.setup
- (Method.setup (Binding.name "intro_locales") (Scan.succeed (METHOD o try_intro_locales_tac false))
+ (Method.setup @{binding intro_locales} (Scan.succeed (METHOD o try_intro_locales_tac false))
"back-chain introduction rules of locales without unfolding predicates" #>
- Method.setup (Binding.name "unfold_locales") (Scan.succeed (METHOD o try_intro_locales_tac true))
+ Method.setup @{binding unfold_locales} (Scan.succeed (METHOD o try_intro_locales_tac true))
"back-chain all introduction rules of locales");
--- a/src/Pure/Isar/method.ML Tue Mar 18 09:39:07 2014 -0700
+++ b/src/Pure/Isar/method.ML Tue Mar 18 21:02:33 2014 +0100
@@ -201,7 +201,7 @@
(* rule etc. -- single-step refinements *)
-val rule_trace = Attrib.setup_config_bool (Binding.name "rule_trace") (fn _ => false);
+val rule_trace = Attrib.setup_config_bool @{binding rule_trace} (fn _ => false);
fun trace ctxt rules =
if Config.get ctxt rule_trace andalso not (null rules) then
@@ -458,7 +458,7 @@
Select_Goals (combinator_info [pos1, pos2], n, m)) ||
meth4) x
and meth2 x =
- (Parse.position Parse.xname -- Args.parse1 is_symid_meth >> (Source o uncurry Args.src) ||
+ (Parse.position Parse.xname -- Parse.args1 is_symid_meth >> (Source o uncurry Args.src) ||
meth3) x
and meth1 x =
(Parse.enum1_positions "," meth2
@@ -478,38 +478,38 @@
(* theory setup *)
val _ = Theory.setup
- (setup (Binding.name "fail") (Scan.succeed (K fail)) "force failure" #>
- setup (Binding.name "succeed") (Scan.succeed (K succeed)) "succeed" #>
- setup (Binding.name "-") (Scan.succeed (K insert_facts))
+ (setup @{binding fail} (Scan.succeed (K fail)) "force failure" #>
+ setup @{binding succeed} (Scan.succeed (K succeed)) "succeed" #>
+ setup @{binding "-"} (Scan.succeed (K insert_facts))
"do nothing (insert current facts only)" #>
- setup (Binding.name "insert") (Attrib.thms >> (K o insert))
+ setup @{binding insert} (Attrib.thms >> (K o insert))
"insert theorems, ignoring facts (improper)" #>
- setup (Binding.name "intro") (Attrib.thms >> (K o intro))
+ setup @{binding intro} (Attrib.thms >> (K o intro))
"repeatedly apply introduction rules" #>
- setup (Binding.name "elim") (Attrib.thms >> (K o elim))
+ setup @{binding elim} (Attrib.thms >> (K o elim))
"repeatedly apply elimination rules" #>
- setup (Binding.name "unfold") (Attrib.thms >> unfold_meth) "unfold definitions" #>
- setup (Binding.name "fold") (Attrib.thms >> fold_meth) "fold definitions" #>
- setup (Binding.name "atomize") (Scan.lift (Args.mode "full") >> atomize)
+ setup @{binding unfold} (Attrib.thms >> unfold_meth) "unfold definitions" #>
+ setup @{binding fold} (Attrib.thms >> fold_meth) "fold definitions" #>
+ setup @{binding atomize} (Scan.lift (Args.mode "full") >> atomize)
"present local premises as object-level statements" #>
- setup (Binding.name "rule") (Attrib.thms >> (fn ths => fn ctxt => some_rule ctxt ths))
+ setup @{binding rule} (Attrib.thms >> (fn ths => fn ctxt => some_rule ctxt ths))
"apply some intro/elim rule" #>
- setup (Binding.name "erule") (xrule_meth erule) "apply rule in elimination manner (improper)" #>
- setup (Binding.name "drule") (xrule_meth drule) "apply rule in destruct manner (improper)" #>
- setup (Binding.name "frule") (xrule_meth frule) "apply rule in forward manner (improper)" #>
- setup (Binding.name "this") (Scan.succeed (K this)) "apply current facts as rules" #>
- setup (Binding.name "fact") (Attrib.thms >> fact) "composition by facts from context" #>
- setup (Binding.name "assumption") (Scan.succeed assumption)
+ setup @{binding erule} (xrule_meth erule) "apply rule in elimination manner (improper)" #>
+ setup @{binding drule} (xrule_meth drule) "apply rule in destruct manner (improper)" #>
+ setup @{binding frule} (xrule_meth frule) "apply rule in forward manner (improper)" #>
+ setup @{binding this} (Scan.succeed (K this)) "apply current facts as rules" #>
+ setup @{binding fact} (Attrib.thms >> fact) "composition by facts from context" #>
+ setup @{binding assumption} (Scan.succeed assumption)
"proof by assumption, preferring facts" #>
- setup (Binding.name "rename_tac") (Args.goal_spec -- Scan.lift (Scan.repeat1 Args.name) >>
+ setup @{binding rename_tac} (Args.goal_spec -- Scan.lift (Scan.repeat1 Args.name) >>
(fn (quant, xs) => K (SIMPLE_METHOD'' quant (rename_tac xs))))
"rename parameters of goal" #>
- setup (Binding.name "rotate_tac") (Args.goal_spec -- Scan.lift (Scan.optional Parse.int 1) >>
+ setup @{binding rotate_tac} (Args.goal_spec -- Scan.lift (Scan.optional Parse.int 1) >>
(fn (quant, i) => K (SIMPLE_METHOD'' quant (rotate_tac i))))
"rotate assumptions of goal" #>
- setup (Binding.name "tactic") (Scan.lift Args.name_source_position >> tactic)
+ setup @{binding tactic} (Scan.lift Args.name_source_position >> tactic)
"ML tactic as proof method" #>
- setup (Binding.name "raw_tactic") (Scan.lift Args.name_source_position >> raw_tactic)
+ setup @{binding raw_tactic} (Scan.lift Args.name_source_position >> raw_tactic)
"ML tactic as raw proof method");
--- a/src/Pure/Isar/outer_syntax.ML Tue Mar 18 09:39:07 2014 -0700
+++ b/src/Pure/Isar/outer_syntax.ML Tue Mar 18 21:02:33 2014 +0100
@@ -288,7 +288,7 @@
fun isar in_stream term : isar =
Source.tty in_stream
|> Symbol.source
- |> Source.map_filter (fn "\\<^newline>" => SOME "\n" | s => SOME s) (*Proof General legacy*)
+ |> Source.map_filter (fn "\<^newline>" => SOME "\n" | s => SOME s) (*Proof General legacy*)
|> Token.source {do_recover = SOME true} Keyword.get_lexicons Position.none
|> toplevel_source term (SOME true) lookup_commands_dynamic;
--- a/src/Pure/Isar/parse.ML Tue Mar 18 09:39:07 2014 -0700
+++ b/src/Pure/Isar/parse.ML Tue Mar 18 21:02:33 2014 +0100
@@ -15,6 +15,7 @@
val triple2: 'a * ('b * 'c) -> 'a * 'b * 'c
val triple_swap: ('a * 'b) * 'c -> ('a * 'c) * 'b
val not_eof: Token.T parser
+ val token: 'a parser -> Token.T parser
val position: 'a parser -> ('a * Position.T) parser
val source_position: 'a parser -> Symbol_Pos.source parser
val inner_syntax: 'a parser -> string parser
@@ -37,6 +38,8 @@
val eof: string parser
val command_name: string -> string parser
val keyword_with: (string -> bool) -> string parser
+ val keyword_markup: bool * Markup.T -> string -> string parser
+ val keyword_improper: string -> string parser
val $$$ : string -> string parser
val reserved: string -> string parser
val semicolon: string parser
@@ -104,6 +107,8 @@
val termp: (string * string list) parser
val target: (xstring * Position.T) parser
val opt_target: (xstring * Position.T) option parser
+ val args: Token.T list parser
+ val args1: (string -> bool) -> Token.T list parser
end;
structure Parse: PARSE =
@@ -168,6 +173,8 @@
val not_eof = RESET_VALUE (Scan.one Token.not_eof);
+fun token atom = Scan.ahead not_eof --| atom;
+
fun position scan = (Scan.ahead not_eof >> Token.pos_of) -- scan >> Library.swap;
fun source_position atom = Scan.ahead atom |-- not_eof >> Token.source_position_of;
fun inner_syntax atom = Scan.ahead atom |-- not_eof >> Token.inner_syntax_of;
@@ -193,17 +200,20 @@
val sync = kind Token.Sync;
val eof = kind Token.EOF;
-fun keyword_with pred = RESET_VALUE (Scan.one (Token.keyword_with pred) >> Token.content_of);
-
fun command_name x =
group (fn () => Token.str_of_kind Token.Command ^ " " ^ quote x)
(RESET_VALUE (Scan.one (fn tok => Token.is_command tok andalso Token.content_of tok = x)))
>> Token.content_of;
-fun $$$ x =
+fun keyword_with pred = RESET_VALUE (Scan.one (Token.keyword_with pred) >> Token.content_of);
+
+fun keyword_markup markup x =
group (fn () => Token.str_of_kind Token.Keyword ^ " " ^ quote x)
(Scan.ahead not_eof -- keyword_with (fn y => x = y))
- >> (fn (tok, x) => (Token.assign (SOME (Token.Literal Markup.quasi_keyword)) tok; x));
+ >> (fn (tok, x) => (Token.assign (SOME (Token.Literal markup)) tok; x));
+
+val keyword_improper = keyword_markup (true, Markup.improper);
+val $$$ = keyword_markup (false, Markup.quasi_keyword);
fun reserved x =
group (fn () => "reserved identifier " ^ quote x)
@@ -393,6 +403,42 @@
val target = ($$$ "(" -- $$$ "in") |-- !!! (position xname --| $$$ ")");
val opt_target = Scan.option target;
+
+(* arguments within outer syntax *)
+
+local
+
+val argument_kinds =
+ [Token.Ident, Token.LongIdent, Token.SymIdent, Token.Var, Token.TypeIdent, Token.TypeVar,
+ Token.Nat, Token.Float, Token.String, Token.AltString, Token.Cartouche, Token.Verbatim];
+
+fun arguments is_symid =
+ let
+ fun argument blk =
+ group (fn () => "argument")
+ (Scan.one (fn tok =>
+ let val kind = Token.kind_of tok in
+ member (op =) argument_kinds kind orelse
+ Token.keyword_with is_symid tok orelse
+ (blk andalso Token.keyword_with (fn s => s = ",") tok)
+ end));
+
+ fun args blk x = Scan.optional (args1 blk) [] x
+ and args1 blk x =
+ ((Scan.repeat1
+ (Scan.repeat1 (argument blk) ||
+ argsp "(" ")" ||
+ argsp "[" "]")) >> flat) x
+ and argsp l r x = (token ($$$ l) ::: !!! (args true @@@ (token ($$$ r) >> single))) x;
+ in (args, args1) end;
+
+in
+
+val args = #1 (arguments Token.ident_or_symbolic) false;
+fun args1 is_symid = #2 (arguments is_symid) false;
+
+end;
+
end;
type 'a parser = 'a Parse.parser;
--- a/src/Pure/Isar/parse.scala Tue Mar 18 09:39:07 2014 -0700
+++ b/src/Pure/Isar/parse.scala Tue Mar 18 21:02:33 2014 +0100
@@ -64,7 +64,7 @@
def path: Parser[String] =
atom("file name/path specification", tok => tok.is_name && Path.is_wellformed(tok.content))
def theory_name: Parser[String] =
- atom("theory name", tok => tok.is_name && Thy_Load.is_wellformed(tok.content))
+ atom("theory name", tok => tok.is_name && Path.is_wellformed(tok.content))
private def tag_name: Parser[String] =
atom("tag name", tok =>
--- a/src/Pure/Isar/parse_spec.ML Tue Mar 18 09:39:07 2014 -0700
+++ b/src/Pure/Isar/parse_spec.ML Tue Mar 18 21:02:33 2014 +0100
@@ -37,7 +37,7 @@
(* theorem specifications *)
-val attrib = Parse.position Parse.liberal_name -- Parse.!!! Args.parse >> uncurry Args.src;
+val attrib = Parse.position Parse.liberal_name -- Parse.!!! Parse.args >> uncurry Args.src;
val attribs = Parse.$$$ "[" |-- Parse.list attrib --| Parse.$$$ "]";
val opt_attribs = Scan.optional attribs [];
--- a/src/Pure/Isar/proof_context.ML Tue Mar 18 09:39:07 2014 -0700
+++ b/src/Pure/Isar/proof_context.ML Tue Mar 18 21:02:33 2014 +0100
@@ -1204,8 +1204,9 @@
fun check_case ctxt (name, pos) fxs =
let
- val (_, ((Rule_Cases.Case {fixes, assumes, binds, cases}, _), _)) =
+ val (_, ((Rule_Cases.Case {fixes, assumes, binds, cases}, is_proper), _)) =
Name_Space.check (Context.Proof ctxt) (cases_of ctxt) (name, pos);
+ val _ = if is_proper then () else Context_Position.report ctxt pos Markup.improper;
fun replace (opt_x :: xs) ((y, T) :: ys) = (the_default y opt_x, T) :: replace xs ys
| replace [] ys = ys
--- a/src/Pure/Isar/token.ML Tue Mar 18 09:39:07 2014 -0700
+++ b/src/Pure/Isar/token.ML Tue Mar 18 21:02:33 2014 +0100
@@ -12,7 +12,7 @@
Error of string | Sync | EOF
type file = {src_path: Path.T, lines: string list, digest: SHA1.digest, pos: Position.T}
datatype value =
- Literal of Markup.T | Text of string | Typ of typ | Term of term | Fact of thm list |
+ Literal of bool * Markup.T | Text of string | Typ of typ | Term of term | Fact of thm list |
Attribute of morphism -> attribute | Files of file Exn.result list
type T
val str_of_kind: kind -> string
@@ -42,7 +42,7 @@
val inner_syntax_of: T -> string
val source_position_of: T -> Symbol_Pos.source
val content_of: T -> string
- val keyword_markup: Markup.T -> string -> Markup.T
+ val keyword_markup: bool * Markup.T -> string -> Markup.T
val completion_report: T -> Position.report_text list
val report: T -> Position.report_text
val markup: T -> Markup.T
@@ -87,7 +87,7 @@
type file = {src_path: Path.T, lines: string list, digest: SHA1.digest, pos: Position.T};
datatype value =
- Literal of Markup.T |
+ Literal of bool * Markup.T |
Text of string |
Typ of typ |
Term of term |
@@ -255,8 +255,8 @@
in
-fun keyword_markup keyword x =
- if Symbol.is_ascii_identifier x then keyword else Markup.delimiter;
+fun keyword_markup (important, keyword) x =
+ if important orelse Symbol.is_ascii_identifier x then keyword else Markup.delimiter;
fun completion_report tok =
if is_kind Keyword tok
@@ -265,7 +265,7 @@
fun report tok =
if is_kind Keyword tok then
- ((pos_of tok, keyword_markup Markup.keyword2 (content_of tok)), "")
+ ((pos_of tok, keyword_markup (false, Markup.keyword2) (content_of tok)), "")
else
let val (m, text) = token_kind_markup (kind_of tok)
in ((pos_of tok, m), text) end;
--- a/src/Pure/ML/ml_antiquotation.ML Tue Mar 18 09:39:07 2014 -0700
+++ b/src/Pure/ML/ml_antiquotation.ML Tue Mar 18 21:02:33 2014 +0100
@@ -1,13 +1,15 @@
(* Title: Pure/ML/ml_antiquotation.ML
Author: Makarius
-Convenience operations for common ML antiquotations. Miscellaneous
-predefined antiquotations.
+ML antiquotations.
*)
signature ML_ANTIQUOTATION =
sig
val variant: string -> Proof.context -> string * Proof.context
+ val declaration: binding -> 'a context_parser ->
+ (Args.src -> 'a -> Proof.context -> ML_Context.decl * Proof.context) ->
+ theory -> theory
val inline: binding -> string context_parser -> theory -> theory
val value: binding -> string context_parser -> theory -> theory
end;
@@ -15,9 +17,7 @@
structure ML_Antiquotation: ML_ANTIQUOTATION =
struct
-(** generic tools **)
-
-(* ML names *)
+(* unique names *)
val init_context = ML_Syntax.reserved |> Name.declare "ML_context";
@@ -35,13 +35,19 @@
in (b, ctxt') end;
-(* specific antiquotations *)
+(* define antiquotations *)
+
+fun declaration name scan body =
+ ML_Context.add_antiquotation name
+ (fn src => fn orig_ctxt =>
+ let val (x, _) = Args.syntax scan src orig_ctxt
+ in body src x orig_ctxt end);
fun inline name scan =
- ML_Context.antiquotation name scan (fn _ => fn s => fn ctxt => (K ("", s), ctxt));
+ declaration name scan (fn _ => fn s => fn ctxt => (K ("", s), ctxt));
fun value name scan =
- ML_Context.antiquotation name scan (fn _ => fn s => fn ctxt =>
+ declaration name scan (fn _ => fn s => fn ctxt =>
let
val (a, ctxt') = variant (Binding.name_of name) ctxt;
val env = "val " ^ a ^ " = " ^ s ^ ";\n";
@@ -49,11 +55,10 @@
in (K (env, body), ctxt') end);
-
-(** misc antiquotations **)
+(* basic antiquotations *)
val _ = Theory.setup
- (ML_Context.antiquotation (Binding.name "here") (Scan.succeed ())
+ (declaration (Binding.name "here") (Scan.succeed ())
(fn src => fn () => fn ctxt =>
let
val (a, ctxt') = variant "position" ctxt;
@@ -62,163 +67,8 @@
val body = "Isabelle." ^ a;
in (K (env, body), ctxt') end) #>
- inline (Binding.name "assert")
- (Scan.succeed "(fn b => if b then () else raise General.Fail \"Assertion failed\")") #>
-
- inline (Binding.name "make_string") (Scan.succeed ml_make_string) #>
-
- value (Binding.name "option") (Scan.lift (Parse.position Args.name) >> (fn (name, pos) =>
- (Options.default_typ name handle ERROR msg => error (msg ^ Position.here pos);
- ML_Syntax.print_string name))) #>
-
value (Binding.name "binding")
- (Scan.lift (Parse.position Args.name) >> ML_Syntax.make_binding) #>
-
- value (Binding.name "theory")
- (Args.context -- Scan.lift (Parse.position Args.name) >> (fn (ctxt, (name, pos)) =>
- (Context_Position.report ctxt pos
- (Theory.get_markup (Context.get_theory (Proof_Context.theory_of ctxt) name));
- "Context.get_theory (Proof_Context.theory_of ML_context) " ^ ML_Syntax.print_string name))
- || Scan.succeed "Proof_Context.theory_of ML_context") #>
-
- value (Binding.name "theory_context")
- (Args.context -- Scan.lift (Parse.position Args.name) >> (fn (ctxt, (name, pos)) =>
- (Context_Position.report ctxt pos
- (Theory.get_markup (Context.get_theory (Proof_Context.theory_of ctxt) name));
- "Proof_Context.get_global (Proof_Context.theory_of ML_context) " ^
- ML_Syntax.print_string name))) #>
-
- inline (Binding.name "context") (Scan.succeed "Isabelle.ML_context") #>
-
- inline (Binding.name "typ") (Args.typ >> (ML_Syntax.atomic o ML_Syntax.print_typ)) #>
- inline (Binding.name "term") (Args.term >> (ML_Syntax.atomic o ML_Syntax.print_term)) #>
- inline (Binding.name "prop") (Args.prop >> (ML_Syntax.atomic o ML_Syntax.print_term)) #>
-
- value (Binding.name "ctyp") (Args.typ >> (fn T =>
- "Thm.ctyp_of (Proof_Context.theory_of ML_context) " ^
- ML_Syntax.atomic (ML_Syntax.print_typ T))) #>
-
- value (Binding.name "cterm") (Args.term >> (fn t =>
- "Thm.cterm_of (Proof_Context.theory_of ML_context) " ^
- ML_Syntax.atomic (ML_Syntax.print_term t))) #>
-
- value (Binding.name "cprop") (Args.prop >> (fn t =>
- "Thm.cterm_of (Proof_Context.theory_of ML_context) " ^
- ML_Syntax.atomic (ML_Syntax.print_term t))) #>
-
- value (Binding.name "cpat")
- (Args.context --
- Scan.lift Args.name_inner_syntax >> uncurry Proof_Context.read_term_pattern >> (fn t =>
- "Thm.cterm_of (Proof_Context.theory_of ML_context) " ^
- ML_Syntax.atomic (ML_Syntax.print_term t))));
-
-
-(* type classes *)
-
-fun class syn = Args.context -- Scan.lift Args.name_inner_syntax >> (fn (ctxt, s) =>
- Proof_Context.read_class ctxt s
- |> syn ? Lexicon.mark_class
- |> ML_Syntax.print_string);
-
-val _ = Theory.setup
- (inline (Binding.name "class") (class false) #>
- inline (Binding.name "class_syntax") (class true) #>
-
- inline (Binding.name "sort")
- (Args.context -- Scan.lift Args.name_inner_syntax >> (fn (ctxt, s) =>
- ML_Syntax.atomic (ML_Syntax.print_sort (Syntax.read_sort ctxt s)))));
-
-
-(* type constructors *)
-
-fun type_name kind check = Args.context -- Scan.lift (Parse.position Args.name_inner_syntax)
- >> (fn (ctxt, (s, pos)) =>
- let
- val Type (c, _) = Proof_Context.read_type_name {proper = true, strict = false} ctxt s;
- val decl = Type.the_decl (Proof_Context.tsig_of ctxt) (c, pos);
- val res =
- (case try check (c, decl) of
- SOME res => res
- | NONE => error ("Not a " ^ kind ^ ": " ^ quote c ^ Position.here pos));
- in ML_Syntax.print_string res end);
-
-val _ = Theory.setup
- (inline (Binding.name "type_name")
- (type_name "logical type" (fn (c, Type.LogicalType _) => c)) #>
- inline (Binding.name "type_abbrev")
- (type_name "type abbreviation" (fn (c, Type.Abbreviation _) => c)) #>
- inline (Binding.name "nonterminal")
- (type_name "nonterminal" (fn (c, Type.Nonterminal) => c)) #>
- inline (Binding.name "type_syntax")
- (type_name "type" (fn (c, _) => Lexicon.mark_type c)));
-
-
-(* constants *)
-
-fun const_name check = Args.context -- Scan.lift (Parse.position Args.name_inner_syntax)
- >> (fn (ctxt, (s, pos)) =>
- let
- val Const (c, _) = Proof_Context.read_const {proper = true, strict = false} ctxt s;
- val res = check (Proof_Context.consts_of ctxt, c)
- handle TYPE (msg, _, _) => error (msg ^ Position.here pos);
- in ML_Syntax.print_string res end);
-
-val _ = Theory.setup
- (inline (Binding.name "const_name")
- (const_name (fn (consts, c) => (Consts.the_const consts c; c))) #>
- inline (Binding.name "const_abbrev")
- (const_name (fn (consts, c) => (Consts.the_abbreviation consts c; c))) #>
- inline (Binding.name "const_syntax")
- (const_name (fn (_, c) => Lexicon.mark_const c)) #>
-
- inline (Binding.name "syntax_const")
- (Args.context -- Scan.lift (Parse.position Args.name) >> (fn (ctxt, (c, pos)) =>
- if is_some (Syntax.lookup_const (Proof_Context.syn_of ctxt) c)
- then ML_Syntax.print_string c
- else error ("Unknown syntax const: " ^ quote c ^ Position.here pos))) #>
-
- inline (Binding.name "const")
- (Args.context -- Scan.lift Args.name_inner_syntax -- Scan.optional
- (Scan.lift (Args.$$$ "(") |-- Parse.enum1' "," Args.typ --| Scan.lift (Args.$$$ ")")) []
- >> (fn ((ctxt, raw_c), Ts) =>
- let
- val Const (c, _) =
- Proof_Context.read_const {proper = true, strict = true} ctxt raw_c;
- val consts = Proof_Context.consts_of ctxt;
- val n = length (Consts.typargs consts (c, Consts.type_scheme consts c));
- val _ = length Ts <> n andalso
- error ("Constant requires " ^ string_of_int n ^ " type argument(s): " ^
- quote c ^ enclose "(" ")" (commas (replicate n "_")));
- val const = Const (c, Consts.instance consts (c, Ts));
- in ML_Syntax.atomic (ML_Syntax.print_term const) end)));
-
-
-(* outer syntax *)
-
-fun with_keyword f =
- Args.theory -- Scan.lift (Parse.position Parse.string) >> (fn (thy, (name, pos)) =>
- (f ((name, Thy_Header.the_keyword thy name), pos)
- handle ERROR msg => error (msg ^ Position.here pos)));
-
-val _ = Theory.setup
- (value (Binding.name "keyword")
- (with_keyword
- (fn ((name, NONE), _) => "Parse.$$$ " ^ ML_Syntax.print_string name
- | ((name, SOME _), pos) =>
- error ("Expected minor keyword " ^ quote name ^ Position.here pos))) #>
- value (Binding.name "command_spec")
- (with_keyword
- (fn ((name, SOME kind), pos) =>
- "Keyword.command_spec " ^ ML_Syntax.atomic
- ((ML_Syntax.print_pair
- (ML_Syntax.print_pair ML_Syntax.print_string
- (ML_Syntax.print_pair
- (ML_Syntax.print_pair ML_Syntax.print_string
- (ML_Syntax.print_list ML_Syntax.print_string))
- (ML_Syntax.print_list ML_Syntax.print_string)))
- ML_Syntax.print_position) ((name, kind), pos))
- | ((name, NONE), pos) =>
- error ("Expected command keyword " ^ quote name ^ Position.here pos))));
+ (Scan.lift (Parse.position Args.name) >> ML_Syntax.make_binding));
end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML/ml_antiquotations.ML Tue Mar 18 21:02:33 2014 +0100
@@ -0,0 +1,167 @@
+(* Title: Pure/ML/ml_antiquotations.ML
+ Author: Makarius
+
+Miscellaneous ML antiquotations.
+*)
+
+structure ML_Antiquotations: sig end =
+struct
+
+val _ = Theory.setup
+ (ML_Antiquotation.inline @{binding assert}
+ (Scan.succeed "(fn b => if b then () else raise General.Fail \"Assertion failed\")") #>
+
+ ML_Antiquotation.inline @{binding make_string} (Scan.succeed ml_make_string) #>
+
+ ML_Antiquotation.value @{binding option} (Scan.lift (Parse.position Args.name) >> (fn (name, pos) =>
+ (Options.default_typ name handle ERROR msg => error (msg ^ Position.here pos);
+ ML_Syntax.print_string name))) #>
+
+ ML_Antiquotation.value @{binding theory}
+ (Args.context -- Scan.lift (Parse.position Args.name) >> (fn (ctxt, (name, pos)) =>
+ (Context_Position.report ctxt pos
+ (Theory.get_markup (Context.get_theory (Proof_Context.theory_of ctxt) name));
+ "Context.get_theory (Proof_Context.theory_of ML_context) " ^ ML_Syntax.print_string name))
+ || Scan.succeed "Proof_Context.theory_of ML_context") #>
+
+ ML_Antiquotation.value @{binding theory_context}
+ (Args.context -- Scan.lift (Parse.position Args.name) >> (fn (ctxt, (name, pos)) =>
+ (Context_Position.report ctxt pos
+ (Theory.get_markup (Context.get_theory (Proof_Context.theory_of ctxt) name));
+ "Proof_Context.get_global (Proof_Context.theory_of ML_context) " ^
+ ML_Syntax.print_string name))) #>
+
+ ML_Antiquotation.inline @{binding context} (Scan.succeed "Isabelle.ML_context") #>
+
+ ML_Antiquotation.inline @{binding typ} (Args.typ >> (ML_Syntax.atomic o ML_Syntax.print_typ)) #>
+ ML_Antiquotation.inline @{binding term} (Args.term >> (ML_Syntax.atomic o ML_Syntax.print_term)) #>
+ ML_Antiquotation.inline @{binding prop} (Args.prop >> (ML_Syntax.atomic o ML_Syntax.print_term)) #>
+
+ ML_Antiquotation.value @{binding ctyp} (Args.typ >> (fn T =>
+ "Thm.ctyp_of (Proof_Context.theory_of ML_context) " ^
+ ML_Syntax.atomic (ML_Syntax.print_typ T))) #>
+
+ ML_Antiquotation.value @{binding cterm} (Args.term >> (fn t =>
+ "Thm.cterm_of (Proof_Context.theory_of ML_context) " ^
+ ML_Syntax.atomic (ML_Syntax.print_term t))) #>
+
+ ML_Antiquotation.value @{binding cprop} (Args.prop >> (fn t =>
+ "Thm.cterm_of (Proof_Context.theory_of ML_context) " ^
+ ML_Syntax.atomic (ML_Syntax.print_term t))) #>
+
+ ML_Antiquotation.value @{binding cpat}
+ (Args.context --
+ Scan.lift Args.name_inner_syntax >> uncurry Proof_Context.read_term_pattern >> (fn t =>
+ "Thm.cterm_of (Proof_Context.theory_of ML_context) " ^
+ ML_Syntax.atomic (ML_Syntax.print_term t))));
+
+
+(* type classes *)
+
+fun class syn = Args.context -- Scan.lift Args.name_inner_syntax >> (fn (ctxt, s) =>
+ Proof_Context.read_class ctxt s
+ |> syn ? Lexicon.mark_class
+ |> ML_Syntax.print_string);
+
+val _ = Theory.setup
+ (ML_Antiquotation.inline @{binding class} (class false) #>
+ ML_Antiquotation.inline @{binding class_syntax} (class true) #>
+
+ ML_Antiquotation.inline @{binding sort}
+ (Args.context -- Scan.lift Args.name_inner_syntax >> (fn (ctxt, s) =>
+ ML_Syntax.atomic (ML_Syntax.print_sort (Syntax.read_sort ctxt s)))));
+
+
+(* type constructors *)
+
+fun type_name kind check = Args.context -- Scan.lift (Parse.position Args.name_inner_syntax)
+ >> (fn (ctxt, (s, pos)) =>
+ let
+ val Type (c, _) = Proof_Context.read_type_name {proper = true, strict = false} ctxt s;
+ val decl = Type.the_decl (Proof_Context.tsig_of ctxt) (c, pos);
+ val res =
+ (case try check (c, decl) of
+ SOME res => res
+ | NONE => error ("Not a " ^ kind ^ ": " ^ quote c ^ Position.here pos));
+ in ML_Syntax.print_string res end);
+
+val _ = Theory.setup
+ (ML_Antiquotation.inline @{binding type_name}
+ (type_name "logical type" (fn (c, Type.LogicalType _) => c)) #>
+ ML_Antiquotation.inline @{binding type_abbrev}
+ (type_name "type abbreviation" (fn (c, Type.Abbreviation _) => c)) #>
+ ML_Antiquotation.inline @{binding nonterminal}
+ (type_name "nonterminal" (fn (c, Type.Nonterminal) => c)) #>
+ ML_Antiquotation.inline @{binding type_syntax}
+ (type_name "type" (fn (c, _) => Lexicon.mark_type c)));
+
+
+(* constants *)
+
+fun const_name check = Args.context -- Scan.lift (Parse.position Args.name_inner_syntax)
+ >> (fn (ctxt, (s, pos)) =>
+ let
+ val Const (c, _) = Proof_Context.read_const {proper = true, strict = false} ctxt s;
+ val res = check (Proof_Context.consts_of ctxt, c)
+ handle TYPE (msg, _, _) => error (msg ^ Position.here pos);
+ in ML_Syntax.print_string res end);
+
+val _ = Theory.setup
+ (ML_Antiquotation.inline @{binding const_name}
+ (const_name (fn (consts, c) => (Consts.the_const consts c; c))) #>
+ ML_Antiquotation.inline @{binding const_abbrev}
+ (const_name (fn (consts, c) => (Consts.the_abbreviation consts c; c))) #>
+ ML_Antiquotation.inline @{binding const_syntax}
+ (const_name (fn (_, c) => Lexicon.mark_const c)) #>
+
+ ML_Antiquotation.inline @{binding syntax_const}
+ (Args.context -- Scan.lift (Parse.position Args.name) >> (fn (ctxt, (c, pos)) =>
+ if is_some (Syntax.lookup_const (Proof_Context.syn_of ctxt) c)
+ then ML_Syntax.print_string c
+ else error ("Unknown syntax const: " ^ quote c ^ Position.here pos))) #>
+
+ ML_Antiquotation.inline @{binding const}
+ (Args.context -- Scan.lift Args.name_inner_syntax -- Scan.optional
+ (Scan.lift (Args.$$$ "(") |-- Parse.enum1' "," Args.typ --| Scan.lift (Args.$$$ ")")) []
+ >> (fn ((ctxt, raw_c), Ts) =>
+ let
+ val Const (c, _) =
+ Proof_Context.read_const {proper = true, strict = true} ctxt raw_c;
+ val consts = Proof_Context.consts_of ctxt;
+ val n = length (Consts.typargs consts (c, Consts.type_scheme consts c));
+ val _ = length Ts <> n andalso
+ error ("Constant requires " ^ string_of_int n ^ " type argument(s): " ^
+ quote c ^ enclose "(" ")" (commas (replicate n "_")));
+ val const = Const (c, Consts.instance consts (c, Ts));
+ in ML_Syntax.atomic (ML_Syntax.print_term const) end)));
+
+
+(* outer syntax *)
+
+fun with_keyword f =
+ Args.theory -- Scan.lift (Parse.position Parse.string) >> (fn (thy, (name, pos)) =>
+ (f ((name, Thy_Header.the_keyword thy name), pos)
+ handle ERROR msg => error (msg ^ Position.here pos)));
+
+val _ = Theory.setup
+ (ML_Antiquotation.value @{binding keyword}
+ (with_keyword
+ (fn ((name, NONE), _) => "Parse.$$$ " ^ ML_Syntax.print_string name
+ | ((name, SOME _), pos) =>
+ error ("Expected minor keyword " ^ quote name ^ Position.here pos))) #>
+ ML_Antiquotation.value @{binding command_spec}
+ (with_keyword
+ (fn ((name, SOME kind), pos) =>
+ "Keyword.command_spec " ^ ML_Syntax.atomic
+ ((ML_Syntax.print_pair
+ (ML_Syntax.print_pair ML_Syntax.print_string
+ (ML_Syntax.print_pair
+ (ML_Syntax.print_pair ML_Syntax.print_string
+ (ML_Syntax.print_list ML_Syntax.print_string))
+ (ML_Syntax.print_list ML_Syntax.print_string)))
+ ML_Syntax.print_position) ((name, kind), pos))
+ | ((name, NONE), pos) =>
+ error ("Expected command keyword " ^ quote name ^ Position.here pos))));
+
+end;
+
--- a/src/Pure/ML/ml_context.ML Tue Mar 18 09:39:07 2014 -0700
+++ b/src/Pure/ML/ml_context.ML Tue Mar 18 21:02:33 2014 +0100
@@ -4,35 +4,25 @@
ML context and antiquotations.
*)
-signature BASIC_ML_CONTEXT =
-sig
- val bind_thm: string * thm -> unit
- val bind_thms: string * thm list -> unit
-end
-
signature ML_CONTEXT =
sig
- include BASIC_ML_CONTEXT
val the_generic_context: unit -> Context.generic
val the_global_context: unit -> theory
val the_local_context: unit -> Proof.context
val thm: xstring -> thm
val thms: xstring -> thm list
val exec: (unit -> unit) -> Context.generic -> Context.generic
- val get_stored_thms: unit -> thm list
- val get_stored_thm: unit -> thm
- val ml_store_thms: string * thm list -> unit
- val ml_store_thm: string * thm -> unit
val check_antiquotation: Proof.context -> xstring * Position.T -> string
+ type decl = Proof.context -> string * string
+ val add_antiquotation: binding -> (Args.src -> Proof.context -> decl * Proof.context) ->
+ theory -> theory
val print_antiquotations: Proof.context -> unit
- type decl = Proof.context -> string * string
- val antiquotation: binding -> 'a context_parser ->
- (Args.src -> 'a -> Proof.context -> decl * Proof.context) -> theory -> theory
val trace_raw: Config.raw
val trace: bool Config.T
val eval_antiquotes: ML_Lex.token Antiquote.antiquote list * Position.T ->
Context.generic option -> (ML_Lex.token list * ML_Lex.token list) * Context.generic option
val eval: bool -> Position.T -> ML_Lex.token Antiquote.antiquote list -> unit
+ val eval_file: bool -> Path.T -> unit
val eval_source: bool -> Symbol_Pos.source -> unit
val eval_in: Proof.context option -> bool -> Position.T ->
ML_Lex.token Antiquote.antiquote list -> unit
@@ -59,41 +49,6 @@
| NONE => error "Missing context after execution");
-(* theorem bindings *)
-
-structure Stored_Thms = Theory_Data
-(
- type T = thm list;
- val empty = [];
- fun extend _ = [];
- fun merge _ = [];
-);
-
-fun get_stored_thms () = Stored_Thms.get (the_global_context ());
-val get_stored_thm = hd o get_stored_thms;
-
-fun ml_store get (name, ths) =
- let
- val ths' = Context.>>> (Context.map_theory_result
- (Global_Theory.store_thms (Binding.name name, ths)));
- val _ = Theory.setup (Stored_Thms.put ths');
- val _ =
- if name = "" then ()
- else if not (ML_Syntax.is_identifier name) then
- error ("Cannot bind theorem(s) " ^ quote name ^ " as ML value")
- else
- ML_Compiler.eval true Position.none
- (ML_Lex.tokenize ("val " ^ name ^ " = " ^ get ^ " ();"));
- val _ = Theory.setup (Stored_Thms.put []);
- in () end;
-
-val ml_store_thms = ml_store "ML_Context.get_stored_thms";
-fun ml_store_thm (name, th) = ml_store "ML_Context.get_stored_thm" (name, [th]);
-
-fun bind_thm (name, thm) = ml_store_thm (name, Drule.export_without_context thm);
-fun bind_thms (name, thms) = ml_store_thms (name, map Drule.export_without_context thms);
-
-
(** ML antiquotations **)
@@ -125,19 +80,13 @@
let val (src', f) = Args.check_src ctxt (get_antiquotations ctxt) src
in f src' ctxt end;
-fun antiquotation name scan body =
- add_antiquotation name
- (fn src => fn orig_ctxt =>
- let val (x, _) = Args.syntax scan src orig_ctxt
- in body src x orig_ctxt end);
-
(* parsing and evaluation *)
local
val antiq =
- Parse.!!! (Parse.position Parse.xname -- Args.parse --| Scan.ahead Parse.eof)
+ Parse.!!! (Parse.position Parse.xname -- Parse.args --| Scan.ahead Parse.eof)
>> uncurry Args.src;
val begin_env0 = ML_Lex.tokenize "structure Isabelle =\nstruct\n";
@@ -220,6 +169,10 @@
(* derived versions *)
+fun eval_file verbose path =
+ let val pos = Path.position path
+ in eval verbose pos (ML_Lex.read pos (File.read path)) end;
+
fun eval_source verbose source =
eval verbose (#pos source) (ML_Lex.read_source source);
@@ -238,5 +191,3 @@
end;
-structure Basic_ML_Context: BASIC_ML_CONTEXT = ML_Context;
-open Basic_ML_Context;
--- a/src/Pure/ML/ml_env.ML Tue Mar 18 09:39:07 2014 -0700
+++ b/src/Pure/ML/ml_env.ML Tue Mar 18 21:02:33 2014 +0100
@@ -20,23 +20,26 @@
structure Env = Generic_Data
(
type T =
- ML_Name_Space.valueVal Symtab.table *
- ML_Name_Space.typeVal Symtab.table *
- ML_Name_Space.fixityVal Symtab.table *
- ML_Name_Space.structureVal Symtab.table *
- ML_Name_Space.signatureVal Symtab.table *
- ML_Name_Space.functorVal Symtab.table;
- val empty = (Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty);
- val extend = I;
+ bool * (*global bootstrap environment*)
+ (ML_Name_Space.valueVal Symtab.table *
+ ML_Name_Space.typeVal Symtab.table *
+ ML_Name_Space.fixityVal Symtab.table *
+ ML_Name_Space.structureVal Symtab.table *
+ ML_Name_Space.signatureVal Symtab.table *
+ ML_Name_Space.functorVal Symtab.table);
+ val empty : T =
+ (true, (Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty));
+ fun extend (_, tabs) : T = (false, tabs);
fun merge
- ((val1, type1, fixity1, structure1, signature1, functor1),
- (val2, type2, fixity2, structure2, signature2, functor2)) : T =
- (Symtab.merge (K true) (val1, val2),
- Symtab.merge (K true) (type1, type2),
- Symtab.merge (K true) (fixity1, fixity2),
- Symtab.merge (K true) (structure1, structure2),
- Symtab.merge (K true) (signature1, signature2),
- Symtab.merge (K true) (functor1, functor2));
+ ((_, (val1, type1, fixity1, structure1, signature1, functor1)),
+ (_, (val2, type2, fixity2, structure2, signature2, functor2))) : T =
+ (false,
+ (Symtab.merge (K true) (val1, val2),
+ Symtab.merge (K true) (type1, type2),
+ Symtab.merge (K true) (fixity1, fixity2),
+ Symtab.merge (K true) (structure1, structure2),
+ Symtab.merge (K true) (signature1, signature2),
+ Symtab.merge (K true) (functor1, functor2)));
);
val inherit = Env.put o Env.get;
@@ -48,18 +51,22 @@
let
fun lookup sel1 sel2 name =
Context.thread_data ()
- |> (fn NONE => NONE | SOME context => Symtab.lookup (sel1 (Env.get context)) name)
+ |> (fn NONE => NONE | SOME context => Symtab.lookup (sel1 (#2 (Env.get context))) name)
|> (fn NONE => sel2 ML_Name_Space.global name | some => some);
fun all sel1 sel2 () =
Context.thread_data ()
- |> (fn NONE => [] | SOME context => Symtab.dest (sel1 (Env.get context)))
+ |> (fn NONE => [] | SOME context => Symtab.dest (sel1 (#2 (Env.get context))))
|> append (sel2 ML_Name_Space.global ())
|> sort_distinct (string_ord o pairself #1);
fun enter ap1 sel2 entry =
if is_some (Context.thread_data ()) then
- Context.>> (Env.map (ap1 (Symtab.update entry)))
+ Context.>> (Env.map (fn (global, tabs) =>
+ let
+ val _ = if global then sel2 ML_Name_Space.global entry else ();
+ val tabs' = ap1 (Symtab.update entry) tabs;
+ in (global, tabs') end))
else sel2 ML_Name_Space.global entry;
in
{lookupVal = lookup #1 #lookupVal,
--- a/src/Pure/ML/ml_thms.ML Tue Mar 18 09:39:07 2014 -0700
+++ b/src/Pure/ML/ml_thms.ML Tue Mar 18 21:02:33 2014 +0100
@@ -8,6 +8,12 @@
sig
val the_attributes: Proof.context -> int -> Args.src list
val the_thmss: Proof.context -> thm list list
+ val get_stored_thms: unit -> thm list
+ val get_stored_thm: unit -> thm
+ val store_thms: string * thm list -> unit
+ val store_thm: string * thm -> unit
+ val bind_thm: string * thm -> unit
+ val bind_thms: string * thm list -> unit
end;
structure ML_Thms: ML_THMS =
@@ -35,7 +41,7 @@
(* attribute source *)
val _ = Theory.setup
- (ML_Context.antiquotation @{binding attributes} (Scan.lift Parse_Spec.attribs)
+ (ML_Antiquotation.declaration @{binding attributes} (Scan.lift Parse_Spec.attribs)
(fn _ => fn raw_srcs => fn ctxt =>
let
val i = serial ();
@@ -68,8 +74,8 @@
in (decl, ctxt'') end;
val _ = Theory.setup
- (ML_Context.antiquotation @{binding thm} (Attrib.thm >> single) (K (thm_binding "thm" true)) #>
- ML_Context.antiquotation @{binding thms} Attrib.thms (K (thm_binding "thms" false)));
+ (ML_Antiquotation.declaration @{binding thm} (Attrib.thm >> single) (K (thm_binding "thm" true)) #>
+ ML_Antiquotation.declaration @{binding thms} Attrib.thms (K (thm_binding "thms" false)));
(* ad-hoc goals *)
@@ -79,7 +85,7 @@
val goal = Scan.unless (by || and_) Args.name_inner_syntax;
val _ = Theory.setup
- (ML_Context.antiquotation @{binding lemma}
+ (ML_Antiquotation.declaration @{binding lemma}
(Scan.lift (Args.mode "open" -- Parse.enum1 "and" (Scan.repeat1 goal) --
(by |-- Method.parse -- Scan.option Method.parse)))
(fn _ => fn ((is_open, raw_propss), (m1, m2)) => fn ctxt =>
@@ -100,5 +106,40 @@
(Facts.named (Proof_Context.full_name ctxt' (Binding.name Auto_Bind.thisN)));
in thm_binding "lemma" (length (flat propss) = 1) thms ctxt end));
+
+(* old-style theorem bindings *)
+
+structure Stored_Thms = Theory_Data
+(
+ type T = thm list;
+ val empty = [];
+ fun extend _ = [];
+ fun merge _ = [];
+);
+
+fun get_stored_thms () = Stored_Thms.get (ML_Context.the_global_context ());
+val get_stored_thm = hd o get_stored_thms;
+
+fun ml_store get (name, ths) =
+ let
+ val ths' = Context.>>> (Context.map_theory_result
+ (Global_Theory.store_thms (Binding.name name, ths)));
+ val _ = Theory.setup (Stored_Thms.put ths');
+ val _ =
+ if name = "" then ()
+ else if not (ML_Syntax.is_identifier name) then
+ error ("Cannot bind theorem(s) " ^ quote name ^ " as ML value")
+ else
+ ML_Compiler.eval true Position.none
+ (ML_Lex.tokenize ("val " ^ name ^ " = " ^ get ^ " ();"));
+ val _ = Theory.setup (Stored_Thms.put []);
+ in () end;
+
+val store_thms = ml_store "ML_Thms.get_stored_thms";
+fun store_thm (name, th) = ml_store "ML_Thms.get_stored_thm" (name, [th]);
+
+fun bind_thm (name, thm) = store_thm (name, Drule.export_without_context thm);
+fun bind_thms (name, thms) = store_thms (name, map Drule.export_without_context thms);
+
end;
--- a/src/Pure/PIDE/document.ML Tue Mar 18 09:39:07 2014 -0700
+++ b/src/Pure/PIDE/document.ML Tue Mar 18 21:02:33 2014 +0100
@@ -443,7 +443,7 @@
NONE => Toplevel.toplevel
| SOME eval => Command.eval_result_state eval)));
val _ = Position.reports (map #2 imports ~~ map Theory.get_markup parents);
- in Thy_Load.begin_theory master_dir header parents end;
+ in Resources.begin_theory master_dir header parents end;
fun check_theory full name node =
is_some (loaded_theory name) orelse
--- a/src/Pure/PIDE/markup.ML Tue Mar 18 09:39:07 2014 -0700
+++ b/src/Pure/PIDE/markup.ML Tue Mar 18 21:02:33 2014 +0100
@@ -105,7 +105,6 @@
val paragraphN: string val paragraph: T
val text_foldN: string val text_fold: T
val commandN: string val command: T
- val operatorN: string val operator: T
val stringN: string val string: T
val altstringN: string val altstring: T
val verbatimN: string val verbatim: T
@@ -117,6 +116,8 @@
val keyword2N: string val keyword2: T
val keyword3N: string val keyword3: T
val quasi_keywordN: string val quasi_keyword: T
+ val improperN: string val improper: T
+ val operatorN: string val operator: T
val elapsedN: string
val cpuN: string
val gcN: string
@@ -427,6 +428,7 @@
val (keyword2N, keyword2) = markup_elem "keyword2";
val (keyword3N, keyword3) = markup_elem "keyword3";
val (quasi_keywordN, quasi_keyword) = markup_elem "quasi_keyword";
+val (improperN, improper) = markup_elem "improper";
val (operatorN, operator) = markup_elem "operator";
val (stringN, string) = markup_elem "string";
val (altstringN, altstring) = markup_elem "altstring";
--- a/src/Pure/PIDE/markup.scala Tue Mar 18 09:39:07 2014 -0700
+++ b/src/Pure/PIDE/markup.scala Tue Mar 18 21:02:33 2014 +0100
@@ -216,6 +216,7 @@
val KEYWORD2 = "keyword2"
val KEYWORD3 = "keyword3"
val QUASI_KEYWORD = "quasi_keyword"
+ val IMPROPER = "improper"
val OPERATOR = "operator"
val STRING = "string"
val ALTSTRING = "altstring"
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/PIDE/resources.ML Tue Mar 18 21:02:33 2014 +0100
@@ -0,0 +1,243 @@
+(* Title: Pure/PIDE/resources.ML
+ Author: Makarius
+
+Resources for theories and auxiliary files.
+*)
+
+signature RESOURCES =
+sig
+ val master_directory: theory -> Path.T
+ val imports_of: theory -> (string * Position.T) list
+ val thy_path: Path.T -> Path.T
+ val check_thy: Path.T -> string ->
+ {master: Path.T * SHA1.digest, text: string, theory_pos: Position.T,
+ imports: (string * Position.T) list, keywords: Thy_Header.keywords}
+ val parse_files: string -> (theory -> Token.file list) parser
+ val provide: Path.T * SHA1.digest -> theory -> theory
+ val provide_parse_files: string -> (theory -> Token.file list * theory) parser
+ val load_file: theory -> Path.T -> (Path.T * SHA1.digest) * string
+ val loaded_files: theory -> Path.T list
+ val loaded_files_current: theory -> bool
+ val begin_theory: Path.T -> Thy_Header.header -> theory list -> theory
+ val load_thy: bool -> (Toplevel.transition -> Time.time option) -> int -> Path.T ->
+ Thy_Header.header -> Position.T -> string -> theory list -> theory * (unit -> unit) * int
+end;
+
+structure Resources: RESOURCES =
+struct
+
+(* manage source files *)
+
+type files =
+ {master_dir: Path.T, (*master directory of theory source*)
+ imports: (string * Position.T) list, (*source specification of imports*)
+ provided: (Path.T * SHA1.digest) list}; (*source path, digest*)
+
+fun make_files (master_dir, imports, provided): files =
+ {master_dir = master_dir, imports = imports, provided = provided};
+
+structure Files = Theory_Data
+(
+ type T = files;
+ val empty = make_files (Path.current, [], []);
+ fun extend _ = empty;
+ fun merge _ = empty;
+);
+
+fun map_files f =
+ Files.map (fn {master_dir, imports, provided} =>
+ make_files (f (master_dir, imports, provided)));
+
+
+val master_directory = #master_dir o Files.get;
+val imports_of = #imports o Files.get;
+
+fun put_deps master_dir imports = map_files (fn _ => (master_dir, imports, []));
+
+
+(* theory files *)
+
+val thy_path = Path.ext "thy";
+
+fun check_file dir file = File.check_file (File.full_path dir file);
+
+fun check_thy dir thy_name =
+ let
+ val path = thy_path (Path.basic thy_name);
+ val master_file = check_file dir path;
+ val text = File.read master_file;
+
+ val {name = (name, pos), imports, keywords} =
+ Thy_Header.read (Path.position master_file) text;
+ val _ = thy_name <> name andalso
+ error ("Bad file name " ^ Path.print path ^ " for theory " ^ quote name ^ Position.here pos);
+ in
+ {master = (master_file, SHA1.digest text), text = text, theory_pos = pos,
+ imports = imports, keywords = keywords}
+ end;
+
+
+(* load files *)
+
+fun parse_files cmd =
+ Scan.ahead Parse.not_eof -- Parse.path >> (fn (tok, name) => fn thy =>
+ (case Token.get_files tok of
+ [] =>
+ let
+ val master_dir = master_directory thy;
+ val pos = Token.pos_of tok;
+ val src_paths = Keyword.command_files cmd (Path.explode name);
+ in map (Command.read_file master_dir pos) src_paths end
+ | files => map Exn.release files));
+
+fun provide (src_path, id) =
+ map_files (fn (master_dir, imports, provided) =>
+ if AList.defined (op =) provided src_path then
+ error ("Duplicate use of source file: " ^ Path.print src_path)
+ else (master_dir, imports, (src_path, id) :: provided));
+
+fun provide_parse_files cmd =
+ parse_files cmd >> (fn files => fn thy =>
+ let
+ val fs = files thy;
+ val thy' = fold (fn {src_path, digest, ...} => provide (src_path, digest)) fs thy;
+ in (fs, thy') end);
+
+fun load_file thy src_path =
+ let
+ val full_path = check_file (master_directory thy) src_path;
+ val text = File.read full_path;
+ val id = SHA1.digest text;
+ in ((full_path, id), text) end;
+
+fun loaded_files_current thy =
+ #provided (Files.get thy) |>
+ forall (fn (src_path, id) =>
+ (case try (load_file thy) src_path of
+ NONE => false
+ | SOME ((_, id'), _) => id = id'));
+
+(*Proof General legacy*)
+fun loaded_files thy =
+ let val {master_dir, provided, ...} = Files.get thy
+ in map (File.full_path master_dir o #1) provided end;
+
+
+(* load theory *)
+
+fun begin_theory master_dir {name, imports, keywords} parents =
+ Theory.begin_theory name parents
+ |> put_deps master_dir imports
+ |> fold Thy_Header.declare_keyword keywords;
+
+fun excursion master_dir last_timing init elements =
+ let
+ fun prepare_span span =
+ Thy_Syntax.span_content span
+ |> Command.read init master_dir []
+ |> (fn tr => Toplevel.put_timing (last_timing tr) tr);
+
+ fun element_result span_elem (st, _) =
+ let
+ 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 (results, thy) end;
+
+fun load_thy document last_timing update_time master_dir header text_pos text parents =
+ let
+ val time = ! Toplevel.timing;
+
+ val {name = (name, _), ...} = header;
+ val _ = Thy_Header.define_keywords header;
+
+ val lexs = Keyword.get_lexicons ();
+ val toks = Thy_Syntax.parse_tokens lexs text_pos text;
+ val spans = Thy_Syntax.parse_spans toks;
+ val elements = Thy_Syntax.parse_elements spans;
+
+ fun init () =
+ begin_theory master_dir header parents
+ |> Present.begin_theory update_time
+ (fn () => HTML.html_mode (implode o map Thy_Syntax.present_span) spans);
+
+ val _ = if time then writeln ("\n**** Starting theory " ^ quote name ^ " ****") else ();
+ val (results, thy) =
+ cond_timeit time "" (fn () => excursion master_dir last_timing init elements);
+ val _ = if time then writeln ("**** Finished theory " ^ quote name ^ " ****\n") else ();
+
+ fun present () =
+ let
+ val res = filter_out (Toplevel.is_ignored o #1) (maps Toplevel.join_results results);
+ val ((minor, _), outer_syntax) = Outer_Syntax.get_syntax ();
+ in
+ if exists (Toplevel.is_skipped_proof o #2) res then
+ warning ("Cannot present theory with skipped proofs: " ^ quote name)
+ else
+ let val tex_source =
+ Thy_Output.present_thy minor Keyword.command_tags
+ (Outer_Syntax.is_markup outer_syntax) res toks
+ |> Buffer.content;
+ in if document then Present.theory_output name tex_source else () end
+ end;
+
+ in (thy, present, size text) end;
+
+
+(* antiquotations *)
+
+local
+
+fun check_path strict ctxt dir (name, pos) =
+ let
+ val _ = Context_Position.report ctxt pos Markup.language_path;
+
+ val path = Path.append dir (Path.explode name)
+ handle ERROR msg => error (msg ^ Position.here pos);
+
+ val _ = Context_Position.report ctxt pos (Markup.path (Path.smart_implode path));
+ val _ =
+ if can Path.expand path andalso File.exists path then ()
+ else
+ let
+ val path' = perhaps (try Path.expand) path;
+ val msg = "Bad file: " ^ Path.print path' ^ Position.here pos;
+ in
+ if strict then error msg
+ else
+ Context_Position.if_visible ctxt Output.report
+ (Markup.markup (Markup.bad |> Markup.properties (Position.properties_of pos)) msg)
+ end;
+ in path end;
+
+fun file_antiq strict ctxt (name, pos) =
+ let
+ val dir = master_directory (Proof_Context.theory_of ctxt);
+ val _ = check_path strict ctxt dir (name, pos);
+ in
+ space_explode "/" name
+ |> map Thy_Output.verb_text
+ |> space_implode (Thy_Output.verb_text "/" ^ "\\discretionary{}{}{}")
+ end;
+
+in
+
+val _ = Theory.setup
+ (Thy_Output.antiquotation @{binding file} (Scan.lift (Parse.position Parse.path))
+ (file_antiq true o #context) #>
+ Thy_Output.antiquotation @{binding file_unchecked} (Scan.lift (Parse.position Parse.path))
+ (file_antiq false o #context) #>
+ ML_Antiquotation.value @{binding path}
+ (Args.context -- Scan.lift (Parse.position Parse.path) >> (fn (ctxt, arg) =>
+ let val path = check_path true ctxt Path.current arg
+ in "Path.explode " ^ ML_Syntax.print_string (Path.implode path) end)));
+
+end;
+
+end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/PIDE/resources.scala Tue Mar 18 21:02:33 2014 +0100
@@ -0,0 +1,105 @@
+/* Title: Pure/PIDE/resources.scala
+ Author: Makarius
+
+Resources for theories and auxiliary files.
+*/
+
+package isabelle
+
+
+import scala.annotation.tailrec
+
+import java.io.{File => JFile}
+
+
+object Resources
+{
+ def thy_path(path: Path): Path = path.ext("thy")
+}
+
+
+class Resources(val loaded_theories: Set[String] = Set.empty, val base_syntax: Outer_Syntax)
+{
+ /* document node names */
+
+ def node_name(raw_path: Path): Document.Node.Name =
+ {
+ val path = raw_path.expand
+ val node = path.implode
+ val theory = Thy_Header.thy_name(node).getOrElse("")
+ val master_dir = if (theory == "") "" else path.dir.implode
+ Document.Node.Name(node, master_dir, theory)
+ }
+
+
+ /* file-system operations */
+
+ def append(dir: String, source_path: Path): String =
+ (Path.explode(dir) + source_path).expand.implode
+
+ def with_thy_text[A](name: Document.Node.Name, f: CharSequence => A): A =
+ {
+ val path = Path.explode(name.node)
+ if (!path.is_file) error("No such file: " + path.toString)
+
+ val text = File.read(path)
+ Symbol.decode_strict(text)
+ f(text)
+ }
+
+
+ /* theory files */
+
+ def body_files_test(syntax: Outer_Syntax, text: String): Boolean =
+ syntax.thy_load_commands.exists({ case (cmd, _) => text.containsSlice(cmd) })
+
+ def body_files(syntax: Outer_Syntax, text: String): List[String] =
+ {
+ val spans = Thy_Syntax.parse_spans(syntax.scan(text))
+ spans.iterator.map(Thy_Syntax.span_files(syntax, _)).flatten.toList
+ }
+
+ def import_name(master: Document.Node.Name, s: String): Document.Node.Name =
+ {
+ val theory = Thy_Header.base_name(s)
+ if (loaded_theories(theory)) Document.Node.Name(theory + ".thy", "", theory)
+ else {
+ val path = Path.explode(s)
+ val node = append(master.master_dir, Resources.thy_path(path))
+ val master_dir = append(master.master_dir, path.dir)
+ Document.Node.Name(node, master_dir, theory)
+ }
+ }
+
+ def check_thy_text(name: Document.Node.Name, text: CharSequence): Document.Node.Header =
+ {
+ try {
+ val header = Thy_Header.read(text)
+
+ val name1 = header.name
+ if (name.theory != name1)
+ error("Bad file name " + Resources.thy_path(Path.basic(name.theory)) +
+ " for theory " + quote(name1))
+
+ val imports = header.imports.map(import_name(name, _))
+ Document.Node.Header(imports, header.keywords, Nil)
+ }
+ catch { case exn: Throwable => Document.Node.bad_header(Exn.message(exn)) }
+ }
+
+ def check_thy(name: Document.Node.Name): Document.Node.Header =
+ with_thy_text(name, check_thy_text(name, _))
+
+
+ /* theory text edits */
+
+ def text_edits(
+ reparse_limit: Int,
+ previous: Document.Version,
+ doc_blobs: Document.Blobs,
+ edits: List[Document.Edit_Text]): (Boolean, List[Document.Edit_Command], Document.Version) =
+ Thy_Syntax.text_edits(this, reparse_limit, previous, doc_blobs, edits)
+
+ def syntax_changed() { }
+}
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/PIDE/session.ML Tue Mar 18 21:02:33 2014 +0100
@@ -0,0 +1,80 @@
+(* Title: Pure/PIDE/session.ML
+ Author: Makarius
+
+Prover session: persistent state of logic image.
+*)
+
+signature SESSION =
+sig
+ val name: unit -> string
+ val welcome: unit -> string
+ val init: bool -> bool -> Path.T -> string -> bool -> string -> (string * string) list ->
+ string -> string * string -> bool * string -> bool -> unit
+ val finish: unit -> unit
+ val protocol_handler: string -> unit
+ val init_protocol_handlers: unit -> unit
+end;
+
+structure Session: SESSION =
+struct
+
+(** session identification -- not thread-safe **)
+
+val session = Unsynchronized.ref {chapter = "Pure", name = "Pure"};
+val session_finished = Unsynchronized.ref false;
+
+fun name () = "Isabelle/" ^ #name (! session);
+
+fun welcome () =
+ if Distribution.is_official then
+ "Welcome to " ^ name () ^ " (" ^ Distribution.version ^ ")"
+ else "Unofficial version of " ^ name () ^ " (" ^ Distribution.version ^ ")";
+
+
+(* init *)
+
+fun init build info info_path doc doc_graph doc_output doc_variants
+ parent (chapter, name) doc_dump verbose =
+ if #name (! session) <> parent orelse not (! session_finished) then
+ error ("Unfinished parent session " ^ quote parent ^ " for " ^ quote name)
+ else
+ let
+ val _ = session := {chapter = chapter, name = name};
+ val _ = session_finished := false;
+ in
+ Present.init build info info_path (if doc = "false" then "" else doc)
+ doc_graph doc_output doc_variants (chapter, name)
+ doc_dump verbose (map Thy_Info.get_theory (Thy_Info.get_names ()))
+ end;
+
+
+(* finish *)
+
+fun finish () =
+ (Execution.shutdown ();
+ Thy_Info.finish ();
+ Present.finish ();
+ Outer_Syntax.check_syntax ();
+ Future.shutdown ();
+ Event_Timer.shutdown ();
+ Future.shutdown ();
+ session_finished := true);
+
+
+
+(** protocol handlers **)
+
+val protocol_handlers = Synchronized.var "protocol_handlers" ([]: string list);
+
+fun protocol_handler name =
+ Synchronized.change protocol_handlers (fn handlers =>
+ (Output.try_protocol_message (Markup.protocol_handler name) "";
+ if not (member (op =) handlers name) then ()
+ else warning ("Redefining protocol handler: " ^ quote name);
+ update (op =) name handlers));
+
+fun init_protocol_handlers () =
+ Synchronized.value protocol_handlers
+ |> List.app (fn name => Output.try_protocol_message (Markup.protocol_handler name) "");
+
+end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/PIDE/session.scala Tue Mar 18 21:02:33 2014 +0100
@@ -0,0 +1,598 @@
+/* Title: Pure/PIDE/session.scala
+ Author: Makarius
+ Options: :folding=explicit:collapseFolds=1:
+
+PIDE editor session, potentially with running prover process.
+*/
+
+package isabelle
+
+
+import java.util.{Timer, TimerTask}
+
+import scala.collection.mutable
+import scala.collection.immutable.Queue
+import scala.actors.TIMEOUT
+import scala.actors.Actor._
+
+
+object Session
+{
+ /* events */
+
+ //{{{
+ case class Statistics(props: Properties.T)
+ case class Global_Options(options: Options)
+ case object Caret_Focus
+ case class Raw_Edits(doc_blobs: Document.Blobs, edits: List[Document.Edit_Text])
+ case class Dialog_Result(id: Document_ID.Generic, serial: Long, result: String)
+ case class Commands_Changed(
+ assignment: Boolean, nodes: Set[Document.Node.Name], commands: Set[Command])
+
+ sealed abstract class Phase
+ case object Inactive extends Phase
+ case object Startup extends Phase // transient
+ case object Failed extends Phase
+ case object Ready extends Phase
+ case object Shutdown extends Phase // transient
+ //}}}
+
+
+ /* protocol handlers */
+
+ type Prover = Isabelle_Process with Protocol
+
+ abstract class Protocol_Handler
+ {
+ def stop(prover: Prover): Unit = {}
+ val functions: Map[String, (Prover, Isabelle_Process.Protocol_Output) => Boolean]
+ }
+
+ class Protocol_Handlers(
+ handlers: Map[String, Session.Protocol_Handler] = Map.empty,
+ functions: Map[String, Isabelle_Process.Protocol_Output => Boolean] = Map.empty)
+ {
+ def get(name: String): Option[Protocol_Handler] = handlers.get(name)
+
+ def add(prover: Prover, name: String): Protocol_Handlers =
+ {
+ val (handlers1, functions1) =
+ handlers.get(name) match {
+ case Some(old_handler) =>
+ System.err.println("Redefining protocol handler: " + name)
+ old_handler.stop(prover)
+ (handlers - name, functions -- old_handler.functions.keys)
+ case None => (handlers, functions)
+ }
+
+ val (handlers2, functions2) =
+ try {
+ val new_handler = Class.forName(name).newInstance.asInstanceOf[Protocol_Handler]
+ val new_functions =
+ for ((a, f) <- new_handler.functions.toList) yield
+ (a, (msg: Isabelle_Process.Protocol_Output) => f(prover, msg))
+
+ val dups = for ((a, _) <- new_functions if functions1.isDefinedAt(a)) yield a
+ if (!dups.isEmpty) error("Duplicate protocol functions: " + commas_quote(dups))
+
+ (handlers1 + (name -> new_handler), functions1 ++ new_functions)
+ }
+ catch {
+ case exn: Throwable =>
+ System.err.println("Failed to initialize protocol handler: " +
+ name + "\n" + Exn.message(exn))
+ (handlers1, functions1)
+ }
+
+ new Protocol_Handlers(handlers2, functions2)
+ }
+
+ def invoke(msg: Isabelle_Process.Protocol_Output): Boolean =
+ msg.properties match {
+ case Markup.Function(a) if functions.isDefinedAt(a) =>
+ try { functions(a)(msg) }
+ catch {
+ case exn: Throwable =>
+ System.err.println("Failed invocation of protocol function: " +
+ quote(a) + "\n" + Exn.message(exn))
+ false
+ }
+ case _ => false
+ }
+
+ def stop(prover: Prover): Protocol_Handlers =
+ {
+ for ((_, handler) <- handlers) handler.stop(prover)
+ new Protocol_Handlers()
+ }
+ }
+}
+
+
+class Session(val resources: Resources)
+{
+ /* global flags */
+
+ @volatile var timing: Boolean = false
+ @volatile var verbose: Boolean = false
+
+
+ /* tuning parameters */
+
+ def output_delay: Time = Time.seconds(0.1) // prover output (markup, common messages)
+ def message_delay: Time = Time.seconds(0.1) // prover input/output messages
+ def prune_delay: Time = Time.seconds(60.0) // prune history -- delete old versions
+ def prune_size: Int = 0 // size of retained history
+ def syslog_limit: Int = 100
+ def reparse_limit: Int = 0
+
+
+ /* pervasive event buses */
+
+ val statistics = new Event_Bus[Session.Statistics]
+ val global_options = new Event_Bus[Session.Global_Options]
+ val caret_focus = new Event_Bus[Session.Caret_Focus.type]
+ val raw_edits = new Event_Bus[Session.Raw_Edits]
+ val commands_changed = new Event_Bus[Session.Commands_Changed]
+ val phase_changed = new Event_Bus[Session.Phase]
+ val syslog_messages = new Event_Bus[Isabelle_Process.Output]
+ val raw_output_messages = new Event_Bus[Isabelle_Process.Output]
+ val all_messages = new Event_Bus[Isabelle_Process.Message] // potential bottle-neck
+ val trace_events = new Event_Bus[Simplifier_Trace.Event.type]
+
+
+ /** buffered command changes (delay_first discipline) **/
+
+ //{{{
+ private case object Stop
+
+ private val (_, commands_changed_buffer) =
+ Simple_Thread.actor("commands_changed_buffer", daemon = true)
+ {
+ var finished = false
+ while (!finished) {
+ receive {
+ case Stop => finished = true; reply(())
+ case changed: Session.Commands_Changed => commands_changed.event(changed)
+ case bad => System.err.println("commands_changed_buffer: ignoring bad message " + bad)
+ }
+ }
+ }
+ //}}}
+
+
+ /** pipelined change parsing **/
+
+ //{{{
+ private case class Text_Edits(
+ previous: Future[Document.Version],
+ doc_blobs: Document.Blobs,
+ text_edits: List[Document.Edit_Text],
+ version_result: Promise[Document.Version])
+
+ private val (_, change_parser) = Simple_Thread.actor("change_parser", daemon = true)
+ {
+ var finished = false
+ while (!finished) {
+ receive {
+ case Stop => finished = true; reply(())
+
+ case Text_Edits(previous, doc_blobs, text_edits, version_result) =>
+ val prev = previous.get_finished
+ val (syntax_changed, doc_edits, version) =
+ Timing.timeit("text_edits", timing) {
+ resources.text_edits(reparse_limit, prev, doc_blobs, text_edits)
+ }
+ version_result.fulfill(version)
+ sender ! Change(doc_blobs, syntax_changed, doc_edits, prev, version)
+
+ case bad => System.err.println("change_parser: ignoring bad message " + bad)
+ }
+ }
+ }
+ //}}}
+
+
+
+ /** main protocol actor **/
+
+ /* global state */
+
+ private val syslog = Volatile(Queue.empty[XML.Elem])
+ def current_syslog(): String = cat_lines(syslog().iterator.map(XML.content))
+
+ @volatile private var _phase: Session.Phase = Session.Inactive
+ private def phase_=(new_phase: Session.Phase)
+ {
+ _phase = new_phase
+ phase_changed.event(new_phase)
+ }
+ def phase = _phase
+ def is_ready: Boolean = phase == Session.Ready
+
+ private val global_state = Volatile(Document.State.init)
+ def current_state(): Document.State = global_state()
+
+ def recent_syntax(): Outer_Syntax =
+ {
+ val version = current_state().recent_finished.version.get_finished
+ if (version.is_init) resources.base_syntax
+ else version.syntax
+ }
+
+ def snapshot(name: Document.Node.Name = Document.Node.Name.empty,
+ pending_edits: List[Text.Edit] = Nil): Document.Snapshot =
+ global_state().snapshot(name, pending_edits)
+
+
+ /* protocol handlers */
+
+ @volatile private var _protocol_handlers = new Session.Protocol_Handlers()
+
+ def protocol_handler(name: String): Option[Session.Protocol_Handler] =
+ _protocol_handlers.get(name)
+
+
+ /* theory files */
+
+ def header_edit(name: Document.Node.Name, header: Document.Node.Header): Document.Edit_Text =
+ {
+ val header1 =
+ if (resources.loaded_theories(name.theory))
+ header.error("Cannot update finished theory " + quote(name.theory))
+ else header
+ (name, Document.Node.Deps(header1))
+ }
+
+
+ /* actor messages */
+
+ private case class Start(args: List[String])
+ private case class Cancel_Exec(exec_id: Document_ID.Exec)
+ private case class Change(
+ doc_blobs: Document.Blobs,
+ syntax_changed: Boolean,
+ doc_edits: List[Document.Edit_Command],
+ previous: Document.Version,
+ version: Document.Version)
+ private case class Protocol_Command(name: String, args: List[String])
+ private case class Messages(msgs: List[Isabelle_Process.Message])
+ private case class Update_Options(options: Options)
+
+ private val (_, session_actor) = Simple_Thread.actor("session_actor", daemon = true)
+ {
+ val this_actor = self
+
+ var prune_next = System.currentTimeMillis() + prune_delay.ms
+
+
+ /* buffered prover messages */
+
+ object receiver
+ {
+ private var buffer = new mutable.ListBuffer[Isabelle_Process.Message]
+
+ private def flush(): Unit = synchronized {
+ if (!buffer.isEmpty) {
+ val msgs = buffer.toList
+ this_actor ! Messages(msgs)
+ buffer = new mutable.ListBuffer[Isabelle_Process.Message]
+ }
+ }
+ def invoke(msg: Isabelle_Process.Message): Unit = synchronized {
+ msg match {
+ case _: Isabelle_Process.Input =>
+ buffer += msg
+ case output: Isabelle_Process.Protocol_Output if output.properties == Markup.Flush =>
+ flush()
+ case output: Isabelle_Process.Output =>
+ buffer += msg
+ if (output.is_syslog)
+ syslog >> (queue =>
+ {
+ val queue1 = queue.enqueue(output.message)
+ if (queue1.length > syslog_limit) queue1.dequeue._2 else queue1
+ })
+ }
+ }
+
+ private val timer = new Timer("session_actor.receiver", true)
+ timer.schedule(new TimerTask { def run = flush }, message_delay.ms, message_delay.ms)
+
+ def cancel() { timer.cancel() }
+ }
+
+ var prover: Option[Session.Prover] = None
+
+
+ /* delayed command changes */
+
+ object delay_commands_changed
+ {
+ private var changed_assignment: Boolean = false
+ private var changed_nodes: Set[Document.Node.Name] = Set.empty
+ private var changed_commands: Set[Command] = Set.empty
+
+ private var flush_time: Option[Long] = None
+
+ def flush_timeout: Long =
+ flush_time match {
+ case None => 5000L
+ case Some(time) => (time - System.currentTimeMillis()) max 0
+ }
+
+ def flush()
+ {
+ if (changed_assignment || !changed_nodes.isEmpty || !changed_commands.isEmpty)
+ commands_changed_buffer !
+ Session.Commands_Changed(changed_assignment, changed_nodes, changed_commands)
+ changed_assignment = false
+ changed_nodes = Set.empty
+ changed_commands = Set.empty
+ flush_time = None
+ }
+
+ def invoke(assign: Boolean, commands: List[Command])
+ {
+ changed_assignment |= assign
+ for (command <- commands) {
+ changed_nodes += command.node_name
+ changed_commands += command
+ }
+ val now = System.currentTimeMillis()
+ flush_time match {
+ case None => flush_time = Some(now + output_delay.ms)
+ case Some(time) => if (now >= time) flush()
+ }
+ }
+ }
+
+
+ /* raw edits */
+
+ def handle_raw_edits(doc_blobs: Document.Blobs, edits: List[Document.Edit_Text])
+ //{{{
+ {
+ prover.get.discontinue_execution()
+
+ val previous = global_state().history.tip.version
+ val version = Future.promise[Document.Version]
+ val change = global_state >>> (_.continue_history(previous, edits, version))
+
+ raw_edits.event(Session.Raw_Edits(doc_blobs, edits))
+ change_parser ! Text_Edits(previous, doc_blobs, edits, version)
+ }
+ //}}}
+
+
+ /* resulting changes */
+
+ def handle_change(change: Change)
+ //{{{
+ {
+ val Change(doc_blobs, syntax_changed, doc_edits, previous, version) = change
+
+ def id_command(command: Command)
+ {
+ for {
+ digest <- command.blobs_digests
+ if !global_state().defined_blob(digest)
+ } {
+ doc_blobs.get(digest) match {
+ case Some(blob) =>
+ global_state >> (_.define_blob(digest))
+ prover.get.define_blob(blob)
+ case None =>
+ System.err.println("Missing blob for SHA1 digest " + digest)
+ }
+ }
+
+ if (!global_state().defined_command(command.id)) {
+ global_state >> (_.define_command(command))
+ prover.get.define_command(command)
+ }
+ }
+ doc_edits foreach {
+ case (_, edit) =>
+ edit foreach { case (c1, c2) => c1 foreach id_command; c2 foreach id_command }
+ }
+
+ val assignment = global_state().the_assignment(previous).check_finished
+ global_state >> (_.define_version(version, assignment))
+ prover.get.update(previous.id, version.id, doc_edits)
+
+ if (syntax_changed) resources.syntax_changed()
+ }
+ //}}}
+
+
+ /* prover output */
+
+ def handle_output(output: Isabelle_Process.Output)
+ //{{{
+ {
+ def bad_output()
+ {
+ if (verbose)
+ System.err.println("Ignoring prover output: " + output.message.toString)
+ }
+
+ def accumulate(state_id: Document_ID.Generic, message: XML.Elem)
+ {
+ try {
+ val st = global_state >>> (_.accumulate(state_id, message))
+ delay_commands_changed.invoke(false, List(st.command))
+ }
+ catch {
+ case _: Document.State.Fail => bad_output()
+ }
+ }
+
+ output match {
+ case msg: Isabelle_Process.Protocol_Output =>
+ val handled = _protocol_handlers.invoke(msg)
+ if (!handled) {
+ msg.properties match {
+ case Markup.Protocol_Handler(name) =>
+ _protocol_handlers = _protocol_handlers.add(prover.get, name)
+
+ case Protocol.Command_Timing(state_id, timing) =>
+ val message = XML.elem(Markup.STATUS, List(XML.Elem(Markup.Timing(timing), Nil)))
+ accumulate(state_id, prover.get.xml_cache.elem(message))
+
+ case Markup.Assign_Update =>
+ msg.text match {
+ case Protocol.Assign_Update(id, update) =>
+ try {
+ val cmds = global_state >>> (_.assign(id, update))
+ delay_commands_changed.invoke(true, cmds)
+ }
+ catch { case _: Document.State.Fail => bad_output() }
+ case _ => bad_output()
+ }
+ // FIXME separate timeout event/message!?
+ if (prover.isDefined && System.currentTimeMillis() > prune_next) {
+ val old_versions = global_state >>> (_.prune_history(prune_size))
+ if (!old_versions.isEmpty) prover.get.remove_versions(old_versions)
+ prune_next = System.currentTimeMillis() + prune_delay.ms
+ }
+
+ case Markup.Removed_Versions =>
+ msg.text match {
+ case Protocol.Removed(removed) =>
+ try {
+ global_state >> (_.removed_versions(removed))
+ }
+ catch { case _: Document.State.Fail => bad_output() }
+ case _ => bad_output()
+ }
+
+ case Markup.ML_Statistics(props) =>
+ statistics.event(Session.Statistics(props))
+
+ case Markup.Task_Statistics(props) =>
+ // FIXME
+
+ case _ => bad_output()
+ }
+ }
+ case _ =>
+ output.properties match {
+ case Position.Id(state_id) =>
+ accumulate(state_id, output.message)
+
+ case _ if output.is_init =>
+ phase = Session.Ready
+
+ case Markup.Return_Code(rc) if output.is_exit =>
+ if (rc == 0) phase = Session.Inactive
+ else phase = Session.Failed
+
+ case _ => raw_output_messages.event(output)
+ }
+ }
+ }
+ //}}}
+
+
+ /* main loop */
+
+ //{{{
+ var finished = false
+ while (!finished) {
+ receiveWithin(delay_commands_changed.flush_timeout) {
+ case TIMEOUT => delay_commands_changed.flush()
+
+ case Start(args) if prover.isEmpty =>
+ if (phase == Session.Inactive || phase == Session.Failed) {
+ phase = Session.Startup
+ prover = Some(new Isabelle_Process(receiver.invoke _, args) with Protocol)
+ }
+
+ case Stop =>
+ if (phase == Session.Ready) {
+ _protocol_handlers = _protocol_handlers.stop(prover.get)
+ global_state >> (_ => Document.State.init) // FIXME event bus!?
+ phase = Session.Shutdown
+ prover.get.terminate
+ prover = None
+ phase = Session.Inactive
+ }
+ finished = true
+ receiver.cancel()
+ reply(())
+
+ case Update_Options(options) if prover.isDefined =>
+ if (is_ready) {
+ prover.get.options(options)
+ handle_raw_edits(Document.Blobs.empty, Nil)
+ }
+ global_options.event(Session.Global_Options(options))
+ reply(())
+
+ case Cancel_Exec(exec_id) if prover.isDefined =>
+ prover.get.cancel_exec(exec_id)
+
+ case Session.Raw_Edits(doc_blobs, edits) if prover.isDefined =>
+ handle_raw_edits(doc_blobs, edits)
+ reply(())
+
+ case Session.Dialog_Result(id, serial, result) if prover.isDefined =>
+ prover.get.dialog_result(serial, result)
+ handle_output(new Isabelle_Process.Output(Protocol.Dialog_Result(id, serial, result)))
+
+ case Protocol_Command(name, args) if prover.isDefined =>
+ prover.get.protocol_command(name, args:_*)
+
+ case Messages(msgs) =>
+ msgs foreach {
+ case input: Isabelle_Process.Input =>
+ all_messages.event(input)
+
+ case output: Isabelle_Process.Output =>
+ if (output.is_stdout || output.is_stderr) raw_output_messages.event(output)
+ else handle_output(output)
+ if (output.is_syslog) syslog_messages.event(output)
+ all_messages.event(output)
+ }
+
+ case change: Change
+ if prover.isDefined && global_state().is_assigned(change.previous) =>
+ handle_change(change)
+
+ case bad if !bad.isInstanceOf[Change] =>
+ System.err.println("session_actor: ignoring bad message " + bad)
+ }
+ }
+ //}}}
+ }
+
+
+ /* actions */
+
+ def start(args: List[String])
+ {
+ session_actor ! Start(args)
+ }
+
+ def stop()
+ {
+ commands_changed_buffer !? Stop
+ change_parser !? Stop
+ session_actor !? Stop
+ }
+
+ def protocol_command(name: String, args: String*)
+ { session_actor ! Protocol_Command(name, args.toList) }
+
+ def cancel_exec(exec_id: Document_ID.Exec) { session_actor ! Cancel_Exec(exec_id) }
+
+ def update(doc_blobs: Document.Blobs, edits: List[Document.Edit_Text])
+ { if (!edits.isEmpty) session_actor !? Session.Raw_Edits(doc_blobs, edits) }
+
+ def update_options(options: Options)
+ { session_actor !? Update_Options(options) }
+
+ def dialog_result(id: Document_ID.Generic, serial: Long, result: String)
+ { session_actor ! Session.Dialog_Result(id, serial, result) }
+}
--- a/src/Pure/Proof/extraction.ML Tue Mar 18 09:39:07 2014 -0700
+++ b/src/Pure/Proof/extraction.ML Tue Mar 18 21:02:33 2014 +0100
@@ -466,9 +466,9 @@
"(realizes (r) (!!x. PROP P (x))) == \
\ (!!x. PROP realizes (r (x)) (PROP P (x)))"] #>
- Attrib.setup (Binding.name "extraction_expand") (Scan.succeed (extraction_expand false))
+ Attrib.setup @{binding extraction_expand} (Scan.succeed (extraction_expand false))
"specify theorems to be expanded during extraction" #>
- Attrib.setup (Binding.name "extraction_expand_def") (Scan.succeed (extraction_expand true))
+ Attrib.setup @{binding extraction_expand_def} (Scan.succeed (extraction_expand true))
"specify definitions to be expanded during extraction");
--- a/src/Pure/Proof/proof_syntax.ML Tue Mar 18 09:39:07 2014 -0700
+++ b/src/Pure/Proof/proof_syntax.ML Tue Mar 18 21:02:33 2014 +0100
@@ -63,9 +63,9 @@
("", idtT --> paramsT, Delimfix "_"),
("", paramT --> paramsT, Delimfix "_")]
|> Sign.add_modesyntax_i (Symbol.xsymbolsN, true)
- [("_Lam", [paramsT, proofT] ---> proofT, Mixfix ("(1\\<^bold>\\<lambda>_./ _)", [0, 3], 3)),
- (Lexicon.mark_const "Appt", [proofT, aT] ---> proofT, Mixfix ("(1_ \\<cdot>/ _)", [4, 5], 4)),
- (Lexicon.mark_const "AppP", [proofT, proofT] ---> proofT, Mixfix ("(1_ \\<bullet>/ _)", [4, 5], 4))]
+ [("_Lam", [paramsT, proofT] ---> proofT, Mixfix ("(1\<^bold>\<lambda>_./ _)", [0, 3], 3)),
+ (Lexicon.mark_const "Appt", [proofT, aT] ---> proofT, Mixfix ("(1_ \<cdot>/ _)", [4, 5], 4)),
+ (Lexicon.mark_const "AppP", [proofT, proofT] ---> proofT, Mixfix ("(1_ \<bullet>/ _)", [4, 5], 4))]
|> Sign.add_trrules (map Syntax.Parse_Print_Rule
[(Ast.mk_appl (Ast.Constant "_Lam")
[Ast.mk_appl (Ast.Constant "_Lam0")
--- a/src/Pure/Pure.thy Tue Mar 18 09:39:07 2014 -0700
+++ b/src/Pure/Pure.thy Tue Mar 18 21:02:33 2014 +0100
@@ -103,6 +103,7 @@
"ProofGeneral.inform_file_retracted" :: control
begin
+ML_file "ML/ml_antiquotations.ML"
ML_file "ML/ml_thms.ML"
ML_file "Isar/isar_syn.ML"
ML_file "Isar/calculation.ML"
--- a/src/Pure/ROOT Tue Mar 18 09:39:07 2014 -0700
+++ b/src/Pure/ROOT Tue Mar 18 21:02:33 2014 +0100
@@ -161,6 +161,8 @@
"PIDE/markup.ML"
"PIDE/protocol.ML"
"PIDE/query_operation.ML"
+ "PIDE/resources.ML"
+ "PIDE/session.ML"
"PIDE/xml.ML"
"PIDE/yxml.ML"
"Proof/extraction.ML"
@@ -189,7 +191,6 @@
"System/isar.ML"
"System/message_channel.ML"
"System/options.ML"
- "System/session.ML"
"System/system_channel.ML"
"Thy/html.ML"
"Thy/latex.ML"
@@ -198,7 +199,6 @@
"Thy/thm_deps.ML"
"Thy/thy_header.ML"
"Thy/thy_info.ML"
- "Thy/thy_load.ML"
"Thy/thy_output.ML"
"Thy/thy_syntax.ML"
"Tools/build.ML"
--- a/src/Pure/ROOT.ML Tue Mar 18 09:39:07 2014 -0700
+++ b/src/Pure/ROOT.ML Tue Mar 18 21:02:33 2014 +0100
@@ -39,7 +39,7 @@
use "ML/ml_lex.ML";
use "ML/ml_parse.ML";
use "General/secure.ML";
-(*^^^^^ end of basic ML bootstrap ^^^^^*)
+(*^^^^^ end of ML bootstrap 0 ^^^^^*)
use "General/integer.ML";
use "General/stack.ML";
use "General/queue.ML";
@@ -211,18 +211,11 @@
use "Syntax/syntax_phases.ML";
use "Isar/local_defs.ML";
-(*proof term operations*)
-use "Proof/reconstruct.ML";
-use "Proof/proof_syntax.ML";
-use "Proof/proof_rewrite_rules.ML";
-use "Proof/proof_checker.ML";
-
(*outer syntax*)
use "Isar/token.ML";
use "Isar/keyword.ML";
use "Isar/parse.ML";
use "Isar/args.ML";
-use "ML/ml_context.ML";
(*theory sources*)
use "Thy/thy_header.ML";
@@ -230,10 +223,15 @@
use "Thy/html.ML";
use "Thy/latex.ML";
+(*ML with context and antiquotations*)
+use "ML/ml_context.ML";
+use "ML/ml_antiquotation.ML";
+val use = ML_Context.eval_file true o Path.explode;
+(*^^^^^ end of ML bootstrap 1 ^^^^^*)
+
(*basic proof engine*)
use "Isar/proof_display.ML";
use "Isar/attrib.ML";
-use "ML/ml_antiquotation.ML";
use "Isar/context_rules.ML";
use "Isar/method.ML";
use "Isar/proof.ML";
@@ -267,6 +265,13 @@
use "Isar/proof_node.ML";
use "Isar/toplevel.ML";
+(*proof term operations*)
+use "Proof/reconstruct.ML";
+use "Proof/proof_syntax.ML";
+use "Proof/proof_rewrite_rules.ML";
+use "Proof/proof_checker.ML";
+use "Proof/extraction.ML";
+
(*theory documents*)
use "System/isabelle_system.ML";
use "Thy/term_style.ML";
@@ -276,7 +281,7 @@
use "Thy/present.ML";
use "PIDE/command.ML";
use "PIDE/query_operation.ML";
-use "Thy/thy_load.ML";
+use "PIDE/resources.ML";
use "Thy/thy_info.ML";
use "PIDE/document.ML";
@@ -286,12 +291,10 @@
use "subgoal.ML";
-use "Proof/extraction.ML";
-
(* Isabelle/Isar system *)
-use "System/session.ML";
+use "PIDE/session.ML";
use "System/command_line.ML";
use "System/system_channel.ML";
use "System/message_channel.ML";
--- a/src/Pure/System/session.ML Tue Mar 18 09:39:07 2014 -0700
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,79 +0,0 @@
-(* Title: Pure/System/session.ML
- Author: Makarius
-
-Session management -- internal state of logic images.
-*)
-
-signature SESSION =
-sig
- val name: unit -> string
- val welcome: unit -> string
- val init: bool -> bool -> Path.T -> string -> bool -> string -> (string * string) list ->
- string -> string * string -> bool * string -> bool -> unit
- val finish: unit -> unit
- val protocol_handler: string -> unit
- val init_protocol_handlers: unit -> unit
-end;
-
-structure Session: SESSION =
-struct
-
-(** session identification -- not thread-safe **)
-
-val session = Unsynchronized.ref {chapter = "Pure", name = "Pure"};
-val session_finished = Unsynchronized.ref false;
-
-fun name () = "Isabelle/" ^ #name (! session);
-
-fun welcome () =
- if Distribution.is_official then
- "Welcome to " ^ name () ^ " (" ^ Distribution.version ^ ")"
- else "Unofficial version of " ^ name () ^ " (" ^ Distribution.version ^ ")";
-
-
-(* init *)
-
-fun init build info info_path doc doc_graph doc_output doc_variants
- parent (chapter, name) doc_dump verbose =
- if #name (! session) <> parent orelse not (! session_finished) then
- error ("Unfinished parent session " ^ quote parent ^ " for " ^ quote name)
- else
- let
- val _ = session := {chapter = chapter, name = name};
- val _ = session_finished := false;
- in
- Present.init build info info_path (if doc = "false" then "" else doc)
- doc_graph doc_output doc_variants (chapter, name)
- doc_dump verbose (map Thy_Info.get_theory (Thy_Info.get_names ()))
- end;
-
-
-(* finish *)
-
-fun finish () =
- (Execution.shutdown ();
- Thy_Info.finish ();
- Present.finish ();
- Outer_Syntax.check_syntax ();
- Future.shutdown ();
- Event_Timer.shutdown ();
- Future.shutdown ();
- session_finished := true);
-
-
-(** protocol handlers **)
-
-val protocol_handlers = Synchronized.var "protocol_handlers" ([]: string list);
-
-fun protocol_handler name =
- Synchronized.change protocol_handlers (fn handlers =>
- (Output.try_protocol_message (Markup.protocol_handler name) "";
- if not (member (op =) handlers name) then ()
- else warning ("Redefining protocol handler: " ^ quote name);
- update (op =) name handlers));
-
-fun init_protocol_handlers () =
- Synchronized.value protocol_handlers
- |> List.app (fn name => Output.try_protocol_message (Markup.protocol_handler name) "");
-
-end;
--- a/src/Pure/System/session.scala Tue Mar 18 09:39:07 2014 -0700
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,598 +0,0 @@
-/* Title: Pure/System/session.scala
- Author: Makarius
- Options: :folding=explicit:collapseFolds=1:
-
-Main Isabelle/Scala session, potentially with running prover process.
-*/
-
-package isabelle
-
-
-import java.util.{Timer, TimerTask}
-
-import scala.collection.mutable
-import scala.collection.immutable.Queue
-import scala.actors.TIMEOUT
-import scala.actors.Actor._
-
-
-object Session
-{
- /* events */
-
- //{{{
- case class Statistics(props: Properties.T)
- case class Global_Options(options: Options)
- case object Caret_Focus
- case class Raw_Edits(doc_blobs: Document.Blobs, edits: List[Document.Edit_Text])
- case class Dialog_Result(id: Document_ID.Generic, serial: Long, result: String)
- case class Commands_Changed(
- assignment: Boolean, nodes: Set[Document.Node.Name], commands: Set[Command])
-
- sealed abstract class Phase
- case object Inactive extends Phase
- case object Startup extends Phase // transient
- case object Failed extends Phase
- case object Ready extends Phase
- case object Shutdown extends Phase // transient
- //}}}
-
-
- /* protocol handlers */
-
- type Prover = Isabelle_Process with Protocol
-
- abstract class Protocol_Handler
- {
- def stop(prover: Prover): Unit = {}
- val functions: Map[String, (Prover, Isabelle_Process.Protocol_Output) => Boolean]
- }
-
- class Protocol_Handlers(
- handlers: Map[String, Session.Protocol_Handler] = Map.empty,
- functions: Map[String, Isabelle_Process.Protocol_Output => Boolean] = Map.empty)
- {
- def get(name: String): Option[Protocol_Handler] = handlers.get(name)
-
- def add(prover: Prover, name: String): Protocol_Handlers =
- {
- val (handlers1, functions1) =
- handlers.get(name) match {
- case Some(old_handler) =>
- System.err.println("Redefining protocol handler: " + name)
- old_handler.stop(prover)
- (handlers - name, functions -- old_handler.functions.keys)
- case None => (handlers, functions)
- }
-
- val (handlers2, functions2) =
- try {
- val new_handler = Class.forName(name).newInstance.asInstanceOf[Protocol_Handler]
- val new_functions =
- for ((a, f) <- new_handler.functions.toList) yield
- (a, (msg: Isabelle_Process.Protocol_Output) => f(prover, msg))
-
- val dups = for ((a, _) <- new_functions if functions1.isDefinedAt(a)) yield a
- if (!dups.isEmpty) error("Duplicate protocol functions: " + commas_quote(dups))
-
- (handlers1 + (name -> new_handler), functions1 ++ new_functions)
- }
- catch {
- case exn: Throwable =>
- System.err.println("Failed to initialize protocol handler: " +
- name + "\n" + Exn.message(exn))
- (handlers1, functions1)
- }
-
- new Protocol_Handlers(handlers2, functions2)
- }
-
- def invoke(msg: Isabelle_Process.Protocol_Output): Boolean =
- msg.properties match {
- case Markup.Function(a) if functions.isDefinedAt(a) =>
- try { functions(a)(msg) }
- catch {
- case exn: Throwable =>
- System.err.println("Failed invocation of protocol function: " +
- quote(a) + "\n" + Exn.message(exn))
- false
- }
- case _ => false
- }
-
- def stop(prover: Prover): Protocol_Handlers =
- {
- for ((_, handler) <- handlers) handler.stop(prover)
- new Protocol_Handlers()
- }
- }
-}
-
-
-class Session(val thy_load: Thy_Load)
-{
- /* global flags */
-
- @volatile var timing: Boolean = false
- @volatile var verbose: Boolean = false
-
-
- /* tuning parameters */
-
- def output_delay: Time = Time.seconds(0.1) // prover output (markup, common messages)
- def message_delay: Time = Time.seconds(0.1) // prover input/output messages
- def prune_delay: Time = Time.seconds(60.0) // prune history -- delete old versions
- def prune_size: Int = 0 // size of retained history
- def syslog_limit: Int = 100
- def reparse_limit: Int = 0
-
-
- /* pervasive event buses */
-
- val statistics = new Event_Bus[Session.Statistics]
- val global_options = new Event_Bus[Session.Global_Options]
- val caret_focus = new Event_Bus[Session.Caret_Focus.type]
- val raw_edits = new Event_Bus[Session.Raw_Edits]
- val commands_changed = new Event_Bus[Session.Commands_Changed]
- val phase_changed = new Event_Bus[Session.Phase]
- val syslog_messages = new Event_Bus[Isabelle_Process.Output]
- val raw_output_messages = new Event_Bus[Isabelle_Process.Output]
- val all_messages = new Event_Bus[Isabelle_Process.Message] // potential bottle-neck
- val trace_events = new Event_Bus[Simplifier_Trace.Event.type]
-
-
- /** buffered command changes (delay_first discipline) **/
-
- //{{{
- private case object Stop
-
- private val (_, commands_changed_buffer) =
- Simple_Thread.actor("commands_changed_buffer", daemon = true)
- {
- var finished = false
- while (!finished) {
- receive {
- case Stop => finished = true; reply(())
- case changed: Session.Commands_Changed => commands_changed.event(changed)
- case bad => System.err.println("commands_changed_buffer: ignoring bad message " + bad)
- }
- }
- }
- //}}}
-
-
- /** pipelined change parsing **/
-
- //{{{
- private case class Text_Edits(
- previous: Future[Document.Version],
- doc_blobs: Document.Blobs,
- text_edits: List[Document.Edit_Text],
- version_result: Promise[Document.Version])
-
- private val (_, change_parser) = Simple_Thread.actor("change_parser", daemon = true)
- {
- var finished = false
- while (!finished) {
- receive {
- case Stop => finished = true; reply(())
-
- case Text_Edits(previous, doc_blobs, text_edits, version_result) =>
- val prev = previous.get_finished
- val (syntax_changed, doc_edits, version) =
- Timing.timeit("Thy_Load.text_edits", timing) {
- thy_load.text_edits(reparse_limit, prev, doc_blobs, text_edits)
- }
- version_result.fulfill(version)
- sender ! Change(doc_blobs, syntax_changed, doc_edits, prev, version)
-
- case bad => System.err.println("change_parser: ignoring bad message " + bad)
- }
- }
- }
- //}}}
-
-
-
- /** main protocol actor **/
-
- /* global state */
-
- private val syslog = Volatile(Queue.empty[XML.Elem])
- def current_syslog(): String = cat_lines(syslog().iterator.map(XML.content))
-
- @volatile private var _phase: Session.Phase = Session.Inactive
- private def phase_=(new_phase: Session.Phase)
- {
- _phase = new_phase
- phase_changed.event(new_phase)
- }
- def phase = _phase
- def is_ready: Boolean = phase == Session.Ready
-
- private val global_state = Volatile(Document.State.init)
- def current_state(): Document.State = global_state()
-
- def recent_syntax(): Outer_Syntax =
- {
- val version = current_state().recent_finished.version.get_finished
- if (version.is_init) thy_load.base_syntax
- else version.syntax
- }
-
- def snapshot(name: Document.Node.Name = Document.Node.Name.empty,
- pending_edits: List[Text.Edit] = Nil): Document.Snapshot =
- global_state().snapshot(name, pending_edits)
-
-
- /* protocol handlers */
-
- @volatile private var _protocol_handlers = new Session.Protocol_Handlers()
-
- def protocol_handler(name: String): Option[Session.Protocol_Handler] =
- _protocol_handlers.get(name)
-
-
- /* theory files */
-
- def header_edit(name: Document.Node.Name, header: Document.Node.Header): Document.Edit_Text =
- {
- val header1 =
- if (thy_load.loaded_theories(name.theory))
- header.error("Cannot update finished theory " + quote(name.theory))
- else header
- (name, Document.Node.Deps(header1))
- }
-
-
- /* actor messages */
-
- private case class Start(args: List[String])
- private case class Cancel_Exec(exec_id: Document_ID.Exec)
- private case class Change(
- doc_blobs: Document.Blobs,
- syntax_changed: Boolean,
- doc_edits: List[Document.Edit_Command],
- previous: Document.Version,
- version: Document.Version)
- private case class Protocol_Command(name: String, args: List[String])
- private case class Messages(msgs: List[Isabelle_Process.Message])
- private case class Update_Options(options: Options)
-
- private val (_, session_actor) = Simple_Thread.actor("session_actor", daemon = true)
- {
- val this_actor = self
-
- var prune_next = System.currentTimeMillis() + prune_delay.ms
-
-
- /* buffered prover messages */
-
- object receiver
- {
- private var buffer = new mutable.ListBuffer[Isabelle_Process.Message]
-
- private def flush(): Unit = synchronized {
- if (!buffer.isEmpty) {
- val msgs = buffer.toList
- this_actor ! Messages(msgs)
- buffer = new mutable.ListBuffer[Isabelle_Process.Message]
- }
- }
- def invoke(msg: Isabelle_Process.Message): Unit = synchronized {
- msg match {
- case _: Isabelle_Process.Input =>
- buffer += msg
- case output: Isabelle_Process.Protocol_Output if output.properties == Markup.Flush =>
- flush()
- case output: Isabelle_Process.Output =>
- buffer += msg
- if (output.is_syslog)
- syslog >> (queue =>
- {
- val queue1 = queue.enqueue(output.message)
- if (queue1.length > syslog_limit) queue1.dequeue._2 else queue1
- })
- }
- }
-
- private val timer = new Timer("session_actor.receiver", true)
- timer.schedule(new TimerTask { def run = flush }, message_delay.ms, message_delay.ms)
-
- def cancel() { timer.cancel() }
- }
-
- var prover: Option[Session.Prover] = None
-
-
- /* delayed command changes */
-
- object delay_commands_changed
- {
- private var changed_assignment: Boolean = false
- private var changed_nodes: Set[Document.Node.Name] = Set.empty
- private var changed_commands: Set[Command] = Set.empty
-
- private var flush_time: Option[Long] = None
-
- def flush_timeout: Long =
- flush_time match {
- case None => 5000L
- case Some(time) => (time - System.currentTimeMillis()) max 0
- }
-
- def flush()
- {
- if (changed_assignment || !changed_nodes.isEmpty || !changed_commands.isEmpty)
- commands_changed_buffer !
- Session.Commands_Changed(changed_assignment, changed_nodes, changed_commands)
- changed_assignment = false
- changed_nodes = Set.empty
- changed_commands = Set.empty
- flush_time = None
- }
-
- def invoke(assign: Boolean, commands: List[Command])
- {
- changed_assignment |= assign
- for (command <- commands) {
- changed_nodes += command.node_name
- changed_commands += command
- }
- val now = System.currentTimeMillis()
- flush_time match {
- case None => flush_time = Some(now + output_delay.ms)
- case Some(time) => if (now >= time) flush()
- }
- }
- }
-
-
- /* raw edits */
-
- def handle_raw_edits(doc_blobs: Document.Blobs, edits: List[Document.Edit_Text])
- //{{{
- {
- prover.get.discontinue_execution()
-
- val previous = global_state().history.tip.version
- val version = Future.promise[Document.Version]
- val change = global_state >>> (_.continue_history(previous, edits, version))
-
- raw_edits.event(Session.Raw_Edits(doc_blobs, edits))
- change_parser ! Text_Edits(previous, doc_blobs, edits, version)
- }
- //}}}
-
-
- /* resulting changes */
-
- def handle_change(change: Change)
- //{{{
- {
- val Change(doc_blobs, syntax_changed, doc_edits, previous, version) = change
-
- def id_command(command: Command)
- {
- for {
- digest <- command.blobs_digests
- if !global_state().defined_blob(digest)
- } {
- doc_blobs.get(digest) match {
- case Some(blob) =>
- global_state >> (_.define_blob(digest))
- prover.get.define_blob(blob)
- case None =>
- System.err.println("Missing blob for SHA1 digest " + digest)
- }
- }
-
- if (!global_state().defined_command(command.id)) {
- global_state >> (_.define_command(command))
- prover.get.define_command(command)
- }
- }
- doc_edits foreach {
- case (_, edit) =>
- edit foreach { case (c1, c2) => c1 foreach id_command; c2 foreach id_command }
- }
-
- val assignment = global_state().the_assignment(previous).check_finished
- global_state >> (_.define_version(version, assignment))
- prover.get.update(previous.id, version.id, doc_edits)
-
- if (syntax_changed) thy_load.syntax_changed()
- }
- //}}}
-
-
- /* prover output */
-
- def handle_output(output: Isabelle_Process.Output)
- //{{{
- {
- def bad_output()
- {
- if (verbose)
- System.err.println("Ignoring prover output: " + output.message.toString)
- }
-
- def accumulate(state_id: Document_ID.Generic, message: XML.Elem)
- {
- try {
- val st = global_state >>> (_.accumulate(state_id, message))
- delay_commands_changed.invoke(false, List(st.command))
- }
- catch {
- case _: Document.State.Fail => bad_output()
- }
- }
-
- output match {
- case msg: Isabelle_Process.Protocol_Output =>
- val handled = _protocol_handlers.invoke(msg)
- if (!handled) {
- msg.properties match {
- case Markup.Protocol_Handler(name) =>
- _protocol_handlers = _protocol_handlers.add(prover.get, name)
-
- case Protocol.Command_Timing(state_id, timing) =>
- val message = XML.elem(Markup.STATUS, List(XML.Elem(Markup.Timing(timing), Nil)))
- accumulate(state_id, prover.get.xml_cache.elem(message))
-
- case Markup.Assign_Update =>
- msg.text match {
- case Protocol.Assign_Update(id, update) =>
- try {
- val cmds = global_state >>> (_.assign(id, update))
- delay_commands_changed.invoke(true, cmds)
- }
- catch { case _: Document.State.Fail => bad_output() }
- case _ => bad_output()
- }
- // FIXME separate timeout event/message!?
- if (prover.isDefined && System.currentTimeMillis() > prune_next) {
- val old_versions = global_state >>> (_.prune_history(prune_size))
- if (!old_versions.isEmpty) prover.get.remove_versions(old_versions)
- prune_next = System.currentTimeMillis() + prune_delay.ms
- }
-
- case Markup.Removed_Versions =>
- msg.text match {
- case Protocol.Removed(removed) =>
- try {
- global_state >> (_.removed_versions(removed))
- }
- catch { case _: Document.State.Fail => bad_output() }
- case _ => bad_output()
- }
-
- case Markup.ML_Statistics(props) =>
- statistics.event(Session.Statistics(props))
-
- case Markup.Task_Statistics(props) =>
- // FIXME
-
- case _ => bad_output()
- }
- }
- case _ =>
- output.properties match {
- case Position.Id(state_id) =>
- accumulate(state_id, output.message)
-
- case _ if output.is_init =>
- phase = Session.Ready
-
- case Markup.Return_Code(rc) if output.is_exit =>
- if (rc == 0) phase = Session.Inactive
- else phase = Session.Failed
-
- case _ => raw_output_messages.event(output)
- }
- }
- }
- //}}}
-
-
- /* main loop */
-
- //{{{
- var finished = false
- while (!finished) {
- receiveWithin(delay_commands_changed.flush_timeout) {
- case TIMEOUT => delay_commands_changed.flush()
-
- case Start(args) if prover.isEmpty =>
- if (phase == Session.Inactive || phase == Session.Failed) {
- phase = Session.Startup
- prover = Some(new Isabelle_Process(receiver.invoke _, args) with Protocol)
- }
-
- case Stop =>
- if (phase == Session.Ready) {
- _protocol_handlers = _protocol_handlers.stop(prover.get)
- global_state >> (_ => Document.State.init) // FIXME event bus!?
- phase = Session.Shutdown
- prover.get.terminate
- prover = None
- phase = Session.Inactive
- }
- finished = true
- receiver.cancel()
- reply(())
-
- case Update_Options(options) if prover.isDefined =>
- if (is_ready) {
- prover.get.options(options)
- handle_raw_edits(Document.Blobs.empty, Nil)
- }
- global_options.event(Session.Global_Options(options))
- reply(())
-
- case Cancel_Exec(exec_id) if prover.isDefined =>
- prover.get.cancel_exec(exec_id)
-
- case Session.Raw_Edits(doc_blobs, edits) if prover.isDefined =>
- handle_raw_edits(doc_blobs, edits)
- reply(())
-
- case Session.Dialog_Result(id, serial, result) if prover.isDefined =>
- prover.get.dialog_result(serial, result)
- handle_output(new Isabelle_Process.Output(Protocol.Dialog_Result(id, serial, result)))
-
- case Protocol_Command(name, args) if prover.isDefined =>
- prover.get.protocol_command(name, args:_*)
-
- case Messages(msgs) =>
- msgs foreach {
- case input: Isabelle_Process.Input =>
- all_messages.event(input)
-
- case output: Isabelle_Process.Output =>
- if (output.is_stdout || output.is_stderr) raw_output_messages.event(output)
- else handle_output(output)
- if (output.is_syslog) syslog_messages.event(output)
- all_messages.event(output)
- }
-
- case change: Change
- if prover.isDefined && global_state().is_assigned(change.previous) =>
- handle_change(change)
-
- case bad if !bad.isInstanceOf[Change] =>
- System.err.println("session_actor: ignoring bad message " + bad)
- }
- }
- //}}}
- }
-
-
- /* actions */
-
- def start(args: List[String])
- {
- session_actor ! Start(args)
- }
-
- def stop()
- {
- commands_changed_buffer !? Stop
- change_parser !? Stop
- session_actor !? Stop
- }
-
- def protocol_command(name: String, args: String*)
- { session_actor ! Protocol_Command(name, args.toList) }
-
- def cancel_exec(exec_id: Document_ID.Exec) { session_actor ! Cancel_Exec(exec_id) }
-
- def update(doc_blobs: Document.Blobs, edits: List[Document.Edit_Text])
- { if (!edits.isEmpty) session_actor !? Session.Raw_Edits(doc_blobs, edits) }
-
- def update_options(options: Options)
- { session_actor !? Update_Options(options) }
-
- def dialog_result(id: Document_ID.Generic, serial: Long, result: String)
- { session_actor ! Session.Dialog_Result(id, serial, result) }
-}
--- a/src/Pure/Thy/term_style.ML Tue Mar 18 09:39:07 2014 -0700
+++ b/src/Pure/Thy/term_style.ML Tue Mar 18 21:02:33 2014 +0100
@@ -33,7 +33,7 @@
(* style parsing *)
fun parse_single ctxt =
- Parse.position Parse.xname -- Args.parse >> (fn (name, args) =>
+ Parse.position Parse.xname -- Parse.args >> (fn (name, args) =>
let
val (src, parse) = Args.check_src ctxt (get_data ctxt) (Args.src name args);
val (f, _) = Args.syntax (Scan.lift parse) src ctxt;
@@ -68,8 +68,8 @@
end);
fun sub_symbols (d :: s :: ss) =
- if Symbol.is_ascii_digit d andalso not (String.isPrefix ("\\<^") s)
- then d :: "\\<^sub>" :: sub_symbols (s :: ss)
+ if Symbol.is_ascii_digit d andalso not (String.isPrefix ("\<^") s)
+ then d :: "\<^sub>" :: sub_symbols (s :: ss)
else d :: s :: ss
| sub_symbols cs = cs;
@@ -84,10 +84,10 @@
| sub_term t = t;
val _ = Theory.setup
- (setup (Binding.name "lhs") (style_lhs_rhs fst) #>
- setup (Binding.name "rhs") (style_lhs_rhs snd) #>
- setup (Binding.name "prem") style_prem #>
- setup (Binding.name "concl") (Scan.succeed (K Logic.strip_imp_concl)) #>
- setup (Binding.name "sub") (Scan.succeed (K sub_term)));
+ (setup @{binding lhs} (style_lhs_rhs fst) #>
+ setup @{binding rhs} (style_lhs_rhs snd) #>
+ setup @{binding prem} style_prem #>
+ setup @{binding concl} (Scan.succeed (K Logic.strip_imp_concl)) #>
+ setup @{binding sub} (Scan.succeed (K sub_term)));
end;
--- a/src/Pure/Thy/thy_info.ML Tue Mar 18 09:39:07 2014 -0700
+++ b/src/Pure/Thy/thy_info.ML Tue Mar 18 21:02:33 2014 +0100
@@ -123,13 +123,13 @@
SOME theory => theory
| _ => error ("Theory loader: undefined entry for theory " ^ quote name));
-val get_imports = Thy_Load.imports_of o get_theory;
+val get_imports = Resources.imports_of o get_theory;
(*Proof General legacy*)
fun loaded_files name = NAMED_CRITICAL "Thy_Info" (fn () =>
(case get_deps name of
NONE => []
- | SOME {master = (thy_path, _), ...} => thy_path :: Thy_Load.loaded_files (get_theory name)));
+ | SOME {master = (thy_path, _), ...} => thy_path :: Resources.loaded_files (get_theory name)));
@@ -284,7 +284,7 @@
val text_pos = Position.put_id (Document_ID.print exec_id) (Path.position thy_path);
val (theory, present, weight) =
- Thy_Load.load_thy document last_timing update_time dir header text_pos text
+ Resources.load_thy document last_timing update_time dir header text_pos text
(if name = Context.PureN then [ML_Context.the_global_context ()] else parents);
fun commit () = update_thy deps theory;
in
@@ -295,18 +295,18 @@
(case lookup_deps name of
SOME NONE => (true, NONE, Position.none, get_imports name, [])
| NONE =>
- let val {master, text, theory_pos, imports, keywords} = Thy_Load.check_thy dir name
+ let val {master, text, theory_pos, imports, keywords} = Resources.check_thy dir name
in (false, SOME (make_deps master imports, text), theory_pos, imports, keywords) end
| SOME (SOME {master, ...}) =>
let
val {master = master', text = text', theory_pos = theory_pos', imports = imports',
- keywords = keywords'} = Thy_Load.check_thy dir name;
+ keywords = keywords'} = Resources.check_thy dir name;
val deps' = SOME (make_deps master' imports', text');
val current =
#2 master = #2 master' andalso
(case lookup_theory name of
NONE => false
- | SOME theory => Thy_Load.loaded_files_current theory);
+ | SOME theory => Resources.loaded_files_current theory);
in (current, deps', theory_pos', imports', keywords') end);
in
@@ -317,7 +317,7 @@
let
val path = Path.expand (Path.explode str);
val name = Path.implode (Path.base path);
- val node_name = File.full_path dir (Thy_Load.thy_path path);
+ val node_name = File.full_path dir (Resources.thy_path path);
fun check_entry (Task (node_name', _, _)) =
if node_name = node_name' then ()
else
@@ -384,7 +384,7 @@
val _ = use_theories {document = false, last_timing = K NONE, master_dir = master_dir} imports;
val _ = Thy_Header.define_keywords header;
val parents = map (get_theory o base_name o fst) imports;
- in Thy_Load.begin_theory master_dir header parents end;
+ in Resources.begin_theory master_dir header parents end;
(* register theory *)
@@ -392,8 +392,8 @@
fun register_thy theory =
let
val name = Context.theory_name theory;
- val {master, ...} = Thy_Load.check_thy (Thy_Load.master_directory theory) name;
- val imports = Thy_Load.imports_of theory;
+ val {master, ...} = Resources.check_thy (Resources.master_directory theory) name;
+ val imports = Resources.imports_of theory;
in
NAMED_CRITICAL "Thy_Info" (fn () =>
(kill_thy name;
--- a/src/Pure/Thy/thy_info.scala Tue Mar 18 09:39:07 2014 -0700
+++ b/src/Pure/Thy/thy_info.scala Tue Mar 18 21:02:33 2014 +0100
@@ -10,7 +10,7 @@
import java.util.concurrent.{Future => JFuture}
-class Thy_Info(thy_load: Thy_Load)
+class Thy_Info(resources: Resources)
{
/* messages */
@@ -33,9 +33,9 @@
{
def load_files(syntax: Outer_Syntax): List[String] =
{
- val string = thy_load.with_thy_text(name, _.toString)
- if (thy_load.body_files_test(syntax, string))
- thy_load.body_files(syntax, string)
+ val string = resources.with_thy_text(name, _.toString)
+ if (resources.body_files_test(syntax, string))
+ resources.body_files(syntax, string)
else Nil
}
}
@@ -71,7 +71,7 @@
val import_errors =
(for {
(theory, names) <- seen_names.iterator_list
- if !thy_load.loaded_theories(theory)
+ if !resources.loaded_theories(theory)
if names.length > 1
} yield
"Incoherent imports for theory " + quote(theory) + ":\n" +
@@ -82,10 +82,10 @@
header_errors ::: import_errors
}
- lazy val syntax: Outer_Syntax = thy_load.base_syntax.add_keywords(keywords)
+ lazy val syntax: Outer_Syntax = resources.base_syntax.add_keywords(keywords)
def loaded_theories: Set[String] =
- (thy_load.loaded_theories /: rev_deps) { case (loaded, dep) => loaded + dep.name.theory }
+ (resources.loaded_theories /: rev_deps) { case (loaded, dep) => loaded + dep.name.theory }
def load_files: List[Path] =
{
@@ -115,13 +115,13 @@
required_by(initiators) + Position.here(require_pos)
val required1 = required + thy
- if (required.seen_names.isDefinedAt(theory) || thy_load.loaded_theories(theory))
+ if (required.seen_names.isDefinedAt(theory) || resources.loaded_theories(theory))
required1
else {
try {
if (initiators.contains(name)) error(cycle_msg(initiators))
val header =
- try { thy_load.check_thy(name).cat_errors(message) }
+ try { resources.check_thy(name).cat_errors(message) }
catch { case ERROR(msg) => cat_error(msg, message) }
val imports = header.imports.map((_, Position.File(name.node)))
Dep(name, header) :: require_thys(name :: initiators, required1, imports)
--- a/src/Pure/Thy/thy_load.ML Tue Mar 18 09:39:07 2014 -0700
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,243 +0,0 @@
-(* Title: Pure/Thy/thy_load.ML
- Author: Makarius
-
-Management of theory sources and auxiliary files.
-*)
-
-signature THY_LOAD =
-sig
- val master_directory: theory -> Path.T
- val imports_of: theory -> (string * Position.T) list
- val thy_path: Path.T -> Path.T
- val check_thy: Path.T -> string ->
- {master: Path.T * SHA1.digest, text: string, theory_pos: Position.T,
- imports: (string * Position.T) list, keywords: Thy_Header.keywords}
- val parse_files: string -> (theory -> Token.file list) parser
- val provide: Path.T * SHA1.digest -> theory -> theory
- val provide_parse_files: string -> (theory -> Token.file list * theory) parser
- val load_file: theory -> Path.T -> (Path.T * SHA1.digest) * string
- val loaded_files: theory -> Path.T list
- val loaded_files_current: theory -> bool
- val begin_theory: Path.T -> Thy_Header.header -> theory list -> theory
- val load_thy: bool -> (Toplevel.transition -> Time.time option) -> int -> Path.T ->
- Thy_Header.header -> Position.T -> string -> theory list -> theory * (unit -> unit) * int
-end;
-
-structure Thy_Load: THY_LOAD =
-struct
-
-(* manage source files *)
-
-type files =
- {master_dir: Path.T, (*master directory of theory source*)
- imports: (string * Position.T) list, (*source specification of imports*)
- provided: (Path.T * SHA1.digest) list}; (*source path, digest*)
-
-fun make_files (master_dir, imports, provided): files =
- {master_dir = master_dir, imports = imports, provided = provided};
-
-structure Files = Theory_Data
-(
- type T = files;
- val empty = make_files (Path.current, [], []);
- fun extend _ = empty;
- fun merge _ = empty;
-);
-
-fun map_files f =
- Files.map (fn {master_dir, imports, provided} =>
- make_files (f (master_dir, imports, provided)));
-
-
-val master_directory = #master_dir o Files.get;
-val imports_of = #imports o Files.get;
-
-fun put_deps master_dir imports = map_files (fn _ => (master_dir, imports, []));
-
-
-(* theory files *)
-
-val thy_path = Path.ext "thy";
-
-fun check_file dir file = File.check_file (File.full_path dir file);
-
-fun check_thy dir thy_name =
- let
- val path = thy_path (Path.basic thy_name);
- val master_file = check_file dir path;
- val text = File.read master_file;
-
- val {name = (name, pos), imports, keywords} =
- Thy_Header.read (Path.position master_file) text;
- val _ = thy_name <> name andalso
- error ("Bad file name " ^ Path.print path ^ " for theory " ^ quote name ^ Position.here pos);
- in
- {master = (master_file, SHA1.digest text), text = text, theory_pos = pos,
- imports = imports, keywords = keywords}
- end;
-
-
-(* load files *)
-
-fun parse_files cmd =
- Scan.ahead Parse.not_eof -- Parse.path >> (fn (tok, name) => fn thy =>
- (case Token.get_files tok of
- [] =>
- let
- val master_dir = master_directory thy;
- val pos = Token.pos_of tok;
- val src_paths = Keyword.command_files cmd (Path.explode name);
- in map (Command.read_file master_dir pos) src_paths end
- | files => map Exn.release files));
-
-fun provide (src_path, id) =
- map_files (fn (master_dir, imports, provided) =>
- if AList.defined (op =) provided src_path then
- error ("Duplicate use of source file: " ^ Path.print src_path)
- else (master_dir, imports, (src_path, id) :: provided));
-
-fun provide_parse_files cmd =
- parse_files cmd >> (fn files => fn thy =>
- let
- val fs = files thy;
- val thy' = fold (fn {src_path, digest, ...} => provide (src_path, digest)) fs thy;
- in (fs, thy') end);
-
-fun load_file thy src_path =
- let
- val full_path = check_file (master_directory thy) src_path;
- val text = File.read full_path;
- val id = SHA1.digest text;
- in ((full_path, id), text) end;
-
-fun loaded_files_current thy =
- #provided (Files.get thy) |>
- forall (fn (src_path, id) =>
- (case try (load_file thy) src_path of
- NONE => false
- | SOME ((_, id'), _) => id = id'));
-
-(*Proof General legacy*)
-fun loaded_files thy =
- let val {master_dir, provided, ...} = Files.get thy
- in map (File.full_path master_dir o #1) provided end;
-
-
-(* load theory *)
-
-fun begin_theory master_dir {name, imports, keywords} parents =
- Theory.begin_theory name parents
- |> put_deps master_dir imports
- |> fold Thy_Header.declare_keyword keywords;
-
-fun excursion master_dir last_timing init elements =
- let
- fun prepare_span span =
- Thy_Syntax.span_content span
- |> Command.read init master_dir []
- |> (fn tr => Toplevel.put_timing (last_timing tr) tr);
-
- fun element_result span_elem (st, _) =
- let
- 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 (results, thy) end;
-
-fun load_thy document last_timing update_time master_dir header text_pos text parents =
- let
- val time = ! Toplevel.timing;
-
- val {name = (name, _), ...} = header;
- val _ = Thy_Header.define_keywords header;
-
- val lexs = Keyword.get_lexicons ();
- val toks = Thy_Syntax.parse_tokens lexs text_pos text;
- val spans = Thy_Syntax.parse_spans toks;
- val elements = Thy_Syntax.parse_elements spans;
-
- fun init () =
- begin_theory master_dir header parents
- |> Present.begin_theory update_time
- (fn () => HTML.html_mode (implode o map Thy_Syntax.present_span) spans);
-
- val _ = if time then writeln ("\n**** Starting theory " ^ quote name ^ " ****") else ();
- val (results, thy) =
- cond_timeit time "" (fn () => excursion master_dir last_timing init elements);
- val _ = if time then writeln ("**** Finished theory " ^ quote name ^ " ****\n") else ();
-
- fun present () =
- let
- val res = filter_out (Toplevel.is_ignored o #1) (maps Toplevel.join_results results);
- val ((minor, _), outer_syntax) = Outer_Syntax.get_syntax ();
- in
- if exists (Toplevel.is_skipped_proof o #2) res then
- warning ("Cannot present theory with skipped proofs: " ^ quote name)
- else
- let val tex_source =
- Thy_Output.present_thy minor Keyword.command_tags
- (Outer_Syntax.is_markup outer_syntax) res toks
- |> Buffer.content;
- in if document then Present.theory_output name tex_source else () end
- end;
-
- in (thy, present, size text) end;
-
-
-(* antiquotations *)
-
-local
-
-fun check_path strict ctxt dir (name, pos) =
- let
- val _ = Context_Position.report ctxt pos Markup.language_path;
-
- val path = Path.append dir (Path.explode name)
- handle ERROR msg => error (msg ^ Position.here pos);
-
- val _ = Context_Position.report ctxt pos (Markup.path (Path.smart_implode path));
- val _ =
- if can Path.expand path andalso File.exists path then ()
- else
- let
- val path' = perhaps (try Path.expand) path;
- val msg = "Bad file: " ^ Path.print path' ^ Position.here pos;
- in
- if strict then error msg
- else
- Context_Position.if_visible ctxt Output.report
- (Markup.markup (Markup.bad |> Markup.properties (Position.properties_of pos)) msg)
- end;
- in path end;
-
-fun file_antiq strict ctxt (name, pos) =
- let
- val dir = master_directory (Proof_Context.theory_of ctxt);
- val _ = check_path strict ctxt dir (name, pos);
- in
- space_explode "/" name
- |> map Thy_Output.verb_text
- |> space_implode (Thy_Output.verb_text "/" ^ "\\discretionary{}{}{}")
- end;
-
-in
-
-val _ = Theory.setup
- (Thy_Output.antiquotation (Binding.name "file") (Scan.lift (Parse.position Parse.path))
- (file_antiq true o #context) #>
- Thy_Output.antiquotation (Binding.name "file_unchecked") (Scan.lift (Parse.position Parse.path))
- (file_antiq false o #context) #>
- ML_Antiquotation.value (Binding.name "path")
- (Args.context -- Scan.lift (Parse.position Parse.path) >> (fn (ctxt, arg) =>
- let val path = check_path true ctxt Path.current arg
- in "Path.explode " ^ ML_Syntax.print_string (Path.implode path) end)));
-
-end;
-
-end;
--- a/src/Pure/Thy/thy_load.scala Tue Mar 18 09:39:07 2014 -0700
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,111 +0,0 @@
-/* Title: Pure/Thy/thy_load.scala
- Author: Makarius
-
-Primitives for loading theory files.
-*/
-
-package isabelle
-
-
-import scala.annotation.tailrec
-
-import java.io.{File => JFile}
-
-
-object Thy_Load
-{
- /* paths */
-
- def thy_path(path: Path): Path = path.ext("thy")
-
- def is_wellformed(str: String): Boolean =
- try { thy_path(Path.explode(str)); true }
- catch { case ERROR(_) => false }
-}
-
-
-class Thy_Load(val loaded_theories: Set[String] = Set.empty, val base_syntax: Outer_Syntax)
-{
- /* document node names */
-
- def node_name(raw_path: Path): Document.Node.Name =
- {
- val path = raw_path.expand
- val node = path.implode
- val theory = Thy_Header.thy_name(node).getOrElse("")
- val master_dir = if (theory == "") "" else path.dir.implode
- Document.Node.Name(node, master_dir, theory)
- }
-
-
- /* file-system operations */
-
- def append(dir: String, source_path: Path): String =
- (Path.explode(dir) + source_path).expand.implode
-
- def with_thy_text[A](name: Document.Node.Name, f: CharSequence => A): A =
- {
- val path = Path.explode(name.node)
- if (!path.is_file) error("No such file: " + path.toString)
-
- val text = File.read(path)
- Symbol.decode_strict(text)
- f(text)
- }
-
-
- /* theory files */
-
- def body_files_test(syntax: Outer_Syntax, text: String): Boolean =
- syntax.thy_load_commands.exists({ case (cmd, _) => text.containsSlice(cmd) })
-
- def body_files(syntax: Outer_Syntax, text: String): List[String] =
- {
- val spans = Thy_Syntax.parse_spans(syntax.scan(text))
- spans.iterator.map(Thy_Syntax.span_files(syntax, _)).flatten.toList
- }
-
- def import_name(master: Document.Node.Name, s: String): Document.Node.Name =
- {
- val theory = Thy_Header.base_name(s)
- if (loaded_theories(theory)) Document.Node.Name(theory + ".thy", "", theory)
- else {
- val path = Path.explode(s)
- val node = append(master.master_dir, Thy_Load.thy_path(path))
- val master_dir = append(master.master_dir, path.dir)
- Document.Node.Name(node, master_dir, theory)
- }
- }
-
- def check_thy_text(name: Document.Node.Name, text: CharSequence): Document.Node.Header =
- {
- try {
- val header = Thy_Header.read(text)
-
- val name1 = header.name
- if (name.theory != name1)
- error("Bad file name " + Thy_Load.thy_path(Path.basic(name.theory)) +
- " for theory " + quote(name1))
-
- val imports = header.imports.map(import_name(name, _))
- Document.Node.Header(imports, header.keywords, Nil)
- }
- catch { case exn: Throwable => Document.Node.bad_header(Exn.message(exn)) }
- }
-
- def check_thy(name: Document.Node.Name): Document.Node.Header =
- with_thy_text(name, check_thy_text(name, _))
-
-
- /* theory text edits */
-
- def text_edits(
- reparse_limit: Int,
- previous: Document.Version,
- doc_blobs: Document.Blobs,
- edits: List[Document.Edit_Text]): (Boolean, List[Document.Edit_Command], Document.Version) =
- Thy_Syntax.text_edits(this, reparse_limit, previous, doc_blobs, edits)
-
- def syntax_changed() { }
-}
-
--- a/src/Pure/Thy/thy_output.ML Tue Mar 18 09:39:07 2014 -0700
+++ b/src/Pure/Thy/thy_output.ML Tue Mar 18 21:02:33 2014 +0100
@@ -151,7 +151,7 @@
val antiq =
Parse.!!!
- (Parse.position Parse.liberal_name -- properties -- Args.parse --| Scan.ahead Parse.eof)
+ (Parse.position Parse.liberal_name -- properties -- Parse.args --| Scan.ahead Parse.eof)
>> (fn ((name, props), args) => (props, Args.src name args));
end;
@@ -437,23 +437,23 @@
(* options *)
val _ = Theory.setup
- (add_option (Binding.name "show_types") (Config.put show_types o boolean) #>
- add_option (Binding.name "show_sorts") (Config.put show_sorts o boolean) #>
- add_option (Binding.name "show_structs") (Config.put show_structs o boolean) #>
- add_option (Binding.name "show_question_marks") (Config.put show_question_marks o boolean) #>
- add_option (Binding.name "show_abbrevs") (Config.put show_abbrevs o boolean) #>
- add_option (Binding.name "names_long") (Config.put Name_Space.names_long o boolean) #>
- add_option (Binding.name "names_short") (Config.put Name_Space.names_short o boolean) #>
- add_option (Binding.name "names_unique") (Config.put Name_Space.names_unique o boolean) #>
- add_option (Binding.name "eta_contract") (Config.put Syntax_Trans.eta_contract o boolean) #>
- add_option (Binding.name "display") (Config.put display o boolean) #>
- add_option (Binding.name "break") (Config.put break o boolean) #>
- add_option (Binding.name "quotes") (Config.put quotes o boolean) #>
- add_option (Binding.name "mode") (add_wrapper o Print_Mode.with_modes o single) #>
- add_option (Binding.name "margin") (add_wrapper o setmp_CRITICAL Pretty.margin_default o integer) #>
- add_option (Binding.name "indent") (Config.put indent o integer) #>
- add_option (Binding.name "source") (Config.put source o boolean) #>
- add_option (Binding.name "goals_limit") (Config.put Goal_Display.goals_limit o integer));
+ (add_option @{binding show_types} (Config.put show_types o boolean) #>
+ add_option @{binding show_sorts} (Config.put show_sorts o boolean) #>
+ add_option @{binding show_structs} (Config.put show_structs o boolean) #>
+ add_option @{binding show_question_marks} (Config.put show_question_marks o boolean) #>
+ add_option @{binding show_abbrevs} (Config.put show_abbrevs o boolean) #>
+ add_option @{binding names_long} (Config.put Name_Space.names_long o boolean) #>
+ add_option @{binding names_short} (Config.put Name_Space.names_short o boolean) #>
+ add_option @{binding names_unique} (Config.put Name_Space.names_unique o boolean) #>
+ add_option @{binding eta_contract} (Config.put Syntax_Trans.eta_contract o boolean) #>
+ add_option @{binding display} (Config.put display o boolean) #>
+ add_option @{binding break} (Config.put break o boolean) #>
+ add_option @{binding quotes} (Config.put quotes o boolean) #>
+ add_option @{binding mode} (add_wrapper o Print_Mode.with_modes o single) #>
+ add_option @{binding margin} (add_wrapper o setmp_CRITICAL Pretty.margin_default o integer) #>
+ add_option @{binding indent} (Config.put indent o integer) #>
+ add_option @{binding source} (Config.put source o boolean) #>
+ add_option @{binding goals_limit} (Config.put Goal_Display.goals_limit o integer));
(* basic pretty printing *)
@@ -565,20 +565,20 @@
in
val _ = Theory.setup
- (basic_entities_style (Binding.name "thm") (Term_Style.parse -- Attrib.thms) pretty_thm_style #>
- basic_entity (Binding.name "prop") (Term_Style.parse -- Args.prop) pretty_term_style #>
- basic_entity (Binding.name "term") (Term_Style.parse -- Args.term) pretty_term_style #>
- basic_entity (Binding.name "term_type") (Term_Style.parse -- Args.term) pretty_term_typ #>
- basic_entity (Binding.name "typeof") (Term_Style.parse -- Args.term) pretty_term_typeof #>
- basic_entity (Binding.name "const") (Args.const {proper = true, strict = false}) pretty_const #>
- basic_entity (Binding.name "abbrev") (Scan.lift Args.name_inner_syntax) pretty_abbrev #>
- basic_entity (Binding.name "typ") Args.typ_abbrev Syntax.pretty_typ #>
- basic_entity (Binding.name "class") (Scan.lift Args.name_inner_syntax) pretty_class #>
- basic_entity (Binding.name "type") (Scan.lift Args.name) pretty_type #>
- basic_entity (Binding.name "text") (Scan.lift Args.name_source_position) pretty_text_report #>
- basic_entities (Binding.name "prf") Attrib.thms (pretty_prf false) #>
- basic_entities (Binding.name "full_prf") Attrib.thms (pretty_prf true) #>
- basic_entity (Binding.name "theory") (Scan.lift (Parse.position Args.name)) pretty_theory);
+ (basic_entities_style @{binding thm} (Term_Style.parse -- Attrib.thms) pretty_thm_style #>
+ basic_entity @{binding prop} (Term_Style.parse -- Args.prop) pretty_term_style #>
+ basic_entity @{binding term} (Term_Style.parse -- Args.term) pretty_term_style #>
+ basic_entity @{binding term_type} (Term_Style.parse -- Args.term) pretty_term_typ #>
+ basic_entity @{binding typeof} (Term_Style.parse -- Args.term) pretty_term_typeof #>
+ basic_entity @{binding const} (Args.const {proper = true, strict = false}) pretty_const #>
+ basic_entity @{binding abbrev} (Scan.lift Args.name_inner_syntax) pretty_abbrev #>
+ basic_entity @{binding typ} Args.typ_abbrev Syntax.pretty_typ #>
+ basic_entity @{binding class} (Scan.lift Args.name_inner_syntax) pretty_class #>
+ basic_entity @{binding type} (Scan.lift Args.name) pretty_type #>
+ basic_entity @{binding text} (Scan.lift Args.name_source_position) pretty_text_report #>
+ basic_entities @{binding prf} Attrib.thms (pretty_prf false) #>
+ basic_entities @{binding full_prf} Attrib.thms (pretty_prf true) #>
+ basic_entity @{binding theory} (Scan.lift (Parse.position Args.name)) pretty_theory);
end;
@@ -600,8 +600,8 @@
in
val _ = Theory.setup
- (goal_state (Binding.name "goals") true #>
- goal_state (Binding.name "subgoals") false);
+ (goal_state @{binding goals} true #>
+ goal_state @{binding subgoals} false);
end;
@@ -611,7 +611,7 @@
val _ = Keyword.define ("by", NONE); (*overlap with command category*)
val _ = Theory.setup
- (antiquotation (Binding.name "lemma")
+ (antiquotation @{binding lemma}
(Scan.lift (Scan.ahead Parse.not_eof) -- Args.prop --
Scan.lift (Parse.position (Args.$$$ "by") -- Method.parse -- Scan.option Method.parse))
(fn {source, context = ctxt, ...} => fn ((prop_token, prop), (((_, by_pos), m1), m2)) =>
@@ -654,18 +654,18 @@
in
val _ = Theory.setup
- (ml_text (Binding.name "ML") (ml_enclose "fn _ => (" ");") #>
- ml_text (Binding.name "ML_op") (ml_enclose "fn _ => (op " ");") #>
- ml_text (Binding.name "ML_type") (ml_enclose "val _ = NONE : (" ") option;") #>
- ml_text (Binding.name "ML_structure")
+ (ml_text @{binding ML} (ml_enclose "fn _ => (" ");") #>
+ ml_text @{binding ML_op} (ml_enclose "fn _ => (op " ");") #>
+ ml_text @{binding ML_type} (ml_enclose "val _ = NONE : (" ") option;") #>
+ ml_text @{binding ML_structure}
(ml_enclose "functor XXX() = struct structure XX = " " end;") #>
- ml_text (Binding.name "ML_functor") (* FIXME formal treatment of functor name (!?) *)
+ ml_text @{binding ML_functor} (* FIXME formal treatment of functor name (!?) *)
(fn source =>
ML_Lex.read Position.none ("ML_Env.check_functor " ^
ML_Syntax.print_string (#1 (Symbol_Pos.source_content source)))) #>
- ml_text (Binding.name "ML_text") (K []));
+ ml_text @{binding ML_text} (K []));
end;
@@ -673,7 +673,7 @@
(* URLs *)
val _ = Theory.setup
- (antiquotation (Binding.name "url") (Scan.lift (Parse.position Parse.name))
+ (antiquotation @{binding url} (Scan.lift (Parse.position Parse.name))
(fn {context = ctxt, ...} => fn (name, pos) =>
(Context_Position.reports ctxt [(pos, Markup.language_path), (pos, Markup.url name)];
enclose "\\url{" "}" name)));
--- a/src/Pure/Thy/thy_syntax.scala Tue Mar 18 09:39:07 2014 -0700
+++ b/src/Pure/Thy/thy_syntax.scala Tue Mar 18 21:02:33 2014 +0100
@@ -257,7 +257,7 @@
}
def resolve_files(
- thy_load: Thy_Load,
+ resources: Resources,
syntax: Outer_Syntax,
node_name: Document.Node.Name,
span: List[Token],
@@ -267,7 +267,7 @@
span_files(syntax, span).map(file_name =>
Exn.capture {
val name =
- Document.Node.Name(thy_load.append(node_name.master_dir, Path.explode(file_name)))
+ Document.Node.Name(resources.append(node_name.master_dir, Path.explode(file_name)))
val blob = doc_blobs.get(name).map(blob => ((blob.bytes.sha1_digest, blob.file)))
(name, blob)
})
@@ -289,7 +289,7 @@
}
private def reparse_spans(
- thy_load: Thy_Load,
+ resources: Resources,
syntax: Outer_Syntax,
doc_blobs: Document.Blobs,
name: Document.Node.Name,
@@ -299,7 +299,7 @@
val cmds0 = commands.iterator(first, last).toList
val blobs_spans0 =
parse_spans(syntax.scan(cmds0.iterator.map(_.source).mkString)).
- map(span => (resolve_files(thy_load, syntax, name, span, doc_blobs), span))
+ map(span => (resolve_files(resources, syntax, name, span, doc_blobs), span))
val (cmds1, blobs_spans1) = chop_common(cmds0, blobs_spans0)
@@ -324,7 +324,7 @@
// FIXME somewhat slow
private def recover_spans(
- thy_load: Thy_Load,
+ resources: Resources,
syntax: Outer_Syntax,
doc_blobs: Document.Blobs,
name: Document.Node.Name,
@@ -342,7 +342,7 @@
case Some(first_unparsed) =>
val first = next_invisible_command(cmds.reverse, first_unparsed)
val last = next_invisible_command(cmds, first_unparsed)
- recover(reparse_spans(thy_load, syntax, doc_blobs, name, cmds, first, last))
+ recover(reparse_spans(resources, syntax, doc_blobs, name, cmds, first, last))
case None => cmds
}
recover(commands)
@@ -352,7 +352,7 @@
/* consolidate unfinished spans */
private def consolidate_spans(
- thy_load: Thy_Load,
+ resources: Resources,
syntax: Outer_Syntax,
doc_blobs: Document.Blobs,
reparse_limit: Int,
@@ -374,7 +374,7 @@
last = it.next
i += last.length
}
- reparse_spans(thy_load, syntax, doc_blobs, name, commands, first_unfinished, last)
+ reparse_spans(resources, syntax, doc_blobs, name, commands, first_unfinished, last)
case None => commands
}
case None => commands
@@ -396,7 +396,7 @@
}
private def text_edit(
- thy_load: Thy_Load,
+ resources: Resources,
syntax: Outer_Syntax,
doc_blobs: Document.Blobs,
reparse_limit: Int,
@@ -413,7 +413,7 @@
val commands0 = node.commands
val commands1 = edit_text(text_edits, commands0)
val commands2 =
- recover_spans(thy_load, syntax, doc_blobs, name, node.perspective.visible, commands1)
+ recover_spans(resources, syntax, doc_blobs, name, node.perspective.visible, commands1)
node.update_commands(commands2)
}
@@ -426,13 +426,13 @@
if (node.same_perspective(perspective)) node
else
node.update_perspective(perspective).update_commands(
- consolidate_spans(thy_load, syntax, doc_blobs, reparse_limit,
+ consolidate_spans(resources, syntax, doc_blobs, reparse_limit,
name, visible, node.commands))
}
}
def text_edits(
- thy_load: Thy_Load,
+ resources: Resources,
reparse_limit: Int,
previous: Document.Version,
doc_blobs: Document.Blobs,
@@ -440,7 +440,7 @@
: (Boolean, List[Document.Edit_Command], Document.Version) =
{
val ((syntax, syntax_changed), reparse0, nodes0, doc_edits0) =
- header_edits(thy_load.base_syntax, previous, edits)
+ header_edits(resources.base_syntax, previous, edits)
if (edits.isEmpty)
(false, Nil, Document.Version.make(syntax, previous.nodes))
@@ -469,10 +469,10 @@
val node1 =
if (reparse_set(name) && !commands.isEmpty)
node.update_commands(
- reparse_spans(thy_load, syntax, doc_blobs,
+ reparse_spans(resources, syntax, doc_blobs,
name, commands, commands.head, commands.last))
else node
- val node2 = (node1 /: edits)(text_edit(thy_load, syntax, doc_blobs, reparse_limit, _, _))
+ val node2 = (node1 /: edits)(text_edit(resources, syntax, doc_blobs, reparse_limit, _, _))
if (!(node.same_perspective(node2.perspective)))
doc_edits += (name -> node2.perspective)
--- a/src/Pure/Tools/build.scala Tue Mar 18 09:39:07 2014 -0700
+++ b/src/Pure/Tools/build.scala Tue Mar 18 21:02:33 2014 +0100
@@ -419,8 +419,8 @@
val parent = deps(parent_name)
(parent.loaded_theories, parent.syntax)
}
- val thy_load = new Thy_Load(preloaded, parent_syntax)
- val thy_info = new Thy_Info(thy_load)
+ val resources = new Resources(preloaded, parent_syntax)
+ val thy_info = new Thy_Info(resources)
if (verbose || list_files) {
val groups =
@@ -432,7 +432,7 @@
val thy_deps =
thy_info.dependencies(
info.theories.map(_._2).flatten.
- map(thy => (thy_load.node_name(info.dir + Thy_Load.thy_path(thy)), info.pos)))
+ map(thy => (resources.node_name(info.dir + Resources.thy_path(thy)), info.pos)))
thy_deps.errors match {
case Nil =>
--- a/src/Pure/Tools/proof_general.ML Tue Mar 18 09:39:07 2014 -0700
+++ b/src/Pure/Tools/proof_general.ML Tue Mar 18 21:02:33 2014 +0100
@@ -337,7 +337,7 @@
Thy_Info.register_thy (Toplevel.end_theory Position.none (Isar.state ()))
handle ERROR msg =>
(warning (cat_lines ["Failed to register theory: " ^ quote name, msg]);
- tell_file_retracted (Thy_Load.thy_path (Path.basic name)))
+ tell_file_retracted (Resources.thy_path (Path.basic name)))
val _ = Isar.init ();
in () end;
--- a/src/Pure/build-jars Tue Mar 18 09:39:07 2014 -0700
+++ b/src/Pure/build-jars Tue Mar 18 21:02:33 2014 +0100
@@ -53,6 +53,8 @@
PIDE/markup_tree.scala
PIDE/protocol.scala
PIDE/query_operation.scala
+ PIDE/resources.scala
+ PIDE/session.scala
PIDE/text.scala
PIDE/xml.scala
PIDE/yxml.scala
@@ -66,14 +68,12 @@
System/isabelle_system.scala
System/options.scala
System/platform.scala
- System/session.scala
System/system_channel.scala
System/utf8.scala
Thy/html.scala
Thy/present.scala
Thy/thy_header.scala
Thy/thy_info.scala
- Thy/thy_load.scala
Thy/thy_syntax.scala
Tools/build.scala
Tools/doc.scala
--- a/src/Pure/pure_syn.ML Tue Mar 18 09:39:07 2014 -0700
+++ b/src/Pure/pure_syn.ML Tue Mar 18 21:02:33 2014 +0100
@@ -9,8 +9,7 @@
val _ =
Outer_Syntax.command
- (("theory", Keyword.tag_theory Keyword.thy_begin), Position.file "pure_syn.ML")
- "begin theory context"
+ (("theory", Keyword.tag_theory Keyword.thy_begin), @{here}) "begin theory"
(Thy_Header.args >> (fn header =>
Toplevel.print o
Toplevel.init_theory
@@ -18,12 +17,11 @@
val _ =
Outer_Syntax.command
- (("ML_file", Keyword.tag_ml Keyword.thy_load), Position.file "pure_syn.ML")
- "ML text from file"
- (Thy_Load.parse_files "ML_file" >> (fn files => Toplevel.generic_theory (fn gthy =>
+ (("ML_file", Keyword.tag_ml Keyword.thy_load), @{here}) "ML text from file"
+ (Resources.parse_files "ML_file" >> (fn files => Toplevel.generic_theory (fn gthy =>
let
val [{src_path, lines, digest, pos}] = files (Context.theory_of gthy);
- val provide = Thy_Load.provide (src_path, digest);
+ val provide = Resources.provide (src_path, digest);
val source = {delimited = true, text = cat_lines lines, pos = pos};
in
gthy
--- a/src/Pure/simplifier.ML Tue Mar 18 09:39:07 2014 -0700
+++ b/src/Pure/simplifier.ML Tue Mar 18 21:02:33 2014 +0100
@@ -144,7 +144,7 @@
val the_simproc = Name_Space.get o get_simprocs;
val _ = Theory.setup
- (ML_Antiquotation.value (Binding.name "simproc")
+ (ML_Antiquotation.value @{binding simproc}
(Args.context -- Scan.lift (Parse.position Args.name)
>> (fn (ctxt, name) =>
"Simplifier.the_simproc ML_context " ^ ML_Syntax.print_string (check_simproc ctxt name))));
@@ -315,13 +315,13 @@
(* setup attributes *)
val _ = Theory.setup
- (Attrib.setup (Binding.name simpN) (Attrib.add_del simp_add simp_del)
+ (Attrib.setup @{binding simp} (Attrib.add_del simp_add simp_del)
"declaration of Simplifier rewrite rule" #>
- Attrib.setup (Binding.name congN) (Attrib.add_del cong_add cong_del)
+ Attrib.setup @{binding cong} (Attrib.add_del cong_add cong_del)
"declaration of Simplifier congruence rule" #>
- Attrib.setup (Binding.name "simproc") simproc_att
+ Attrib.setup @{binding simproc} simproc_att
"declaration of simplification procedures" #>
- Attrib.setup (Binding.name "simplified") simplified "simplified rule");
+ Attrib.setup @{binding simplified} simplified "simplified rule");
@@ -362,12 +362,12 @@
(** setup **)
fun method_setup more_mods =
- Method.setup (Binding.name simpN)
+ Method.setup @{binding simp}
(simp_method more_mods (fn ctxt => fn tac => fn facts =>
HEADGOAL (Method.insert_tac facts THEN'
(CHANGED_PROP oo tac) ctxt)))
"simplification" #>
- Method.setup (Binding.name "simp_all")
+ Method.setup @{binding simp_all}
(simp_method more_mods (fn ctxt => fn tac => fn facts =>
ALLGOALS (Method.insert_tac facts) THEN
(CHANGED_PROP o PARALLEL_GOALS o ALLGOALS o tac) ctxt))
--- a/src/Sequents/Washing.thy Tue Mar 18 09:39:07 2014 -0700
+++ b/src/Sequents/Washing.thy Tue Mar 18 21:02:33 2014 +0100
@@ -32,10 +32,10 @@
(* "activate" definitions for use in proof *)
-ML {* bind_thms ("changeI", [@{thm context1}] RL ([@{thm change}] RLN (2,[@{thm cut}]))) *}
-ML {* bind_thms ("load1I", [@{thm context1}] RL ([@{thm load1}] RLN (2,[@{thm cut}]))) *}
-ML {* bind_thms ("washI", [@{thm context1}] RL ([@{thm wash}] RLN (2,[@{thm cut}]))) *}
-ML {* bind_thms ("dryI", [@{thm context1}] RL ([@{thm dry}] RLN (2,[@{thm cut}]))) *}
+ML {* ML_Thms.bind_thms ("changeI", [@{thm context1}] RL ([@{thm change}] RLN (2,[@{thm cut}]))) *}
+ML {* ML_Thms.bind_thms ("load1I", [@{thm context1}] RL ([@{thm load1}] RLN (2,[@{thm cut}]))) *}
+ML {* ML_Thms.bind_thms ("washI", [@{thm context1}] RL ([@{thm wash}] RLN (2,[@{thm cut}]))) *}
+ML {* ML_Thms.bind_thms ("dryI", [@{thm context1}] RL ([@{thm dry}] RLN (2,[@{thm cut}]))) *}
(* a load of dirty clothes and two dollars gives you clean clothes *)
--- a/src/Tools/Code/code_runtime.ML Tue Mar 18 09:39:07 2014 -0700
+++ b/src/Tools/Code/code_runtime.ML Tue Mar 18 21:02:33 2014 +0100
@@ -325,7 +325,7 @@
let
val preamble =
"(* Generated from " ^
- Path.implode (Thy_Load.thy_path (Path.basic (Context.theory_name thy))) ^
+ Path.implode (Resources.thy_path (Path.basic (Context.theory_name thy))) ^
"; DO NOT EDIT! *)";
val _ = File.write (Path.explode file_name) (preamble ^ "\n\n" ^ code);
in
@@ -354,7 +354,7 @@
(** Isar setup **)
val _ =
- Theory.setup (ML_Context.antiquotation @{binding code} Args.term (fn _ => ml_code_antiq));
+ Theory.setup (ML_Antiquotation.declaration @{binding code} Args.term (fn _ => ml_code_antiq));
local
--- a/src/Tools/Code/code_target.ML Tue Mar 18 09:39:07 2014 -0700
+++ b/src/Tools/Code/code_target.ML Tue Mar 18 21:02:33 2014 +0100
@@ -380,7 +380,8 @@
| assert_module_name module_name = module_name;
fun using_master_directory ctxt =
- Option.map (Path.append (File.pwd ()) o Path.append (Thy_Load.master_directory (Proof_Context.theory_of ctxt)));
+ Option.map (Path.append (File.pwd ()) o
+ Path.append (Resources.master_directory (Proof_Context.theory_of ctxt)));
in
@@ -646,7 +647,7 @@
Parse.enum1 "|" (Parse.group (fn () => "code symbol pragma")
(parse_symbol_pragma parse_const parse_tyco parse_class parse_classrel parse_inst parse_module));
-val code_expr_argsP = Scan.optional (@{keyword "("} |-- Args.parse --| @{keyword ")"}) [];
+val code_expr_argsP = Scan.optional (@{keyword "("} |-- Parse.args --| @{keyword ")"}) [];
fun code_expr_inP all_public raw_cs =
Scan.repeat (@{keyword "in"} |-- Parse.!!! (Parse.name
--- a/src/Tools/jEdit/etc/options Tue Mar 18 09:39:07 2014 -0700
+++ b/src/Tools/jEdit/etc/options Tue Mar 18 21:02:33 2014 +0100
@@ -45,9 +45,6 @@
public option jedit_completion_delay : real = 0.5
-- "delay for completion popup (seconds)"
-public option jedit_completion_dismiss_delay : real = 0.0
- -- "delay for dismissing obsolete completion popup (seconds)"
-
public option jedit_completion_immediate : bool = false
-- "insert unique completion immediately into buffer (if delay = 0)"
@@ -85,6 +82,7 @@
option keyword2_color : string = "009966FF"
option keyword3_color : string = "0099FFFF"
option quasi_keyword_color : string = "9966FFFF"
+option improper_color : string = "FF5050FF"
option operator_color : string = "323232FF"
option caret_invisible_color : string = "50000080"
option completion_color : string = "0000FFFF"
--- a/src/Tools/jEdit/lib/Tools/jedit Tue Mar 18 09:39:07 2014 -0700
+++ b/src/Tools/jEdit/lib/Tools/jedit Tue Mar 18 21:02:33 2014 +0100
@@ -27,7 +27,7 @@
"src/jedit_editor.scala"
"src/jedit_lib.scala"
"src/jedit_options.scala"
- "src/jedit_thy_load.scala"
+ "src/jedit_resources.scala"
"src/monitor_dockable.scala"
"src/output_dockable.scala"
"src/plugin.scala"
--- a/src/Tools/jEdit/src/completion_popup.scala Tue Mar 18 09:39:07 2014 -0700
+++ b/src/Tools/jEdit/src/completion_popup.scala Tue Mar 18 21:02:33 2014 +0100
@@ -112,7 +112,7 @@
completion_popup match {
case Some(completion) =>
completion.active_range match {
- case Some((range, _)) if completion.isDisplayable => Some(range)
+ case Some(range) if completion.isDisplayable => Some(range)
case _ => None
}
case None => None
@@ -236,21 +236,35 @@
val items = result.items.map(new Item(_))
val completion =
- new Completion_Popup(Some((range, invalidate _)), layered, loc2, font, items)
+ new Completion_Popup(Some(range), layered, loc2, font, items)
{
override def complete(item: Completion.Item) {
PIDE.completion_history.update(item)
insert(item)
}
override def propagate(evt: KeyEvent) {
- JEdit_Lib.propagate_key(view, evt)
+ if (view.getKeyEventInterceptor == inner_key_listener) {
+ try {
+ view.setKeyEventInterceptor(null)
+ JEdit_Lib.propagate_key(view, evt)
+ }
+ finally {
+ if (isDisplayable) view.setKeyEventInterceptor(inner_key_listener)
+ }
+ }
if (evt.getID == KeyEvent.KEY_TYPED) input(evt)
}
- override def refocus() { text_area.requestFocus }
+ override def shutdown(focus: Boolean) {
+ if (view.getKeyEventInterceptor == inner_key_listener)
+ view.setKeyEventInterceptor(null)
+ if (focus) text_area.requestFocus
+ invalidate()
+ }
}
completion_popup = Some(completion)
+ view.setKeyEventInterceptor(completion.inner_key_listener)
invalidate()
- completion.show_popup()
+ completion.show_popup(false)
}
}
@@ -448,10 +462,10 @@
override def propagate(evt: KeyEvent) {
if (!evt.isConsumed) text_field.processKeyEvent(evt)
}
- override def refocus() { text_field.requestFocus }
+ override def shutdown(focus: Boolean) { if (focus) text_field.requestFocus }
}
completion_popup = Some(completion)
- completion.show_popup()
+ completion.show_popup(true)
case None =>
}
@@ -506,7 +520,7 @@
class Completion_Popup private(
- val active_range: Option[(Text.Range, () => Unit)],
+ val active_range: Option[Text.Range],
layered: JLayeredPane,
location: Point,
font: Font,
@@ -524,7 +538,7 @@
def complete(item: Completion.Item) { }
def propagate(evt: KeyEvent) { }
- def refocus() { }
+ def shutdown(focus: Boolean) { }
/* list view */
@@ -568,7 +582,7 @@
/* event handling */
- private val inner_key_listener =
+ val inner_key_listener =
JEdit_Lib.key_listener(
key_pressed = (e: KeyEvent) =>
{
@@ -639,27 +653,16 @@
new Popup(layered, completion, screen.relative(layered, size), size)
}
- private def show_popup()
+ private def show_popup(focus: Boolean)
{
popup.show
- list_view.requestFocus
+ if (focus) list_view.requestFocus
}
- private val hide_popup_delay =
- Swing_Thread.delay_last(PIDE.options.seconds("jedit_completion_dismiss_delay")) {
- active_range match { case Some((_, invalidate)) => invalidate() case _ => }
- popup.hide
- }
-
private def hide_popup()
{
- if (list_view.peer.isFocusOwner) refocus()
-
- if (PIDE.options.seconds("jedit_completion_dismiss_delay").is_zero) {
- active_range match { case Some((_, invalidate)) => invalidate() case _ => }
- popup.hide
- }
- else hide_popup_delay.invoke()
+ shutdown(list_view.peer.isFocusOwner)
+ popup.hide
}
}
--- a/src/Tools/jEdit/src/document_model.scala Tue Mar 18 09:39:07 2014 -0700
+++ b/src/Tools/jEdit/src/document_model.scala Tue Mar 18 21:02:33 2014 +0100
@@ -70,7 +70,7 @@
if (is_theory) {
JEdit_Lib.buffer_lock(buffer) {
Exn.capture {
- PIDE.thy_load.check_thy_text(node_name, buffer.getSegment(0, buffer.getLength))
+ PIDE.resources.check_thy_text(node_name, buffer.getSegment(0, buffer.getLength))
} match {
case Exn.Res(header) => header
case Exn.Exn(exn) => Document.Node.bad_header(Exn.message(exn))
@@ -150,7 +150,7 @@
_blob match {
case Some(x) => x
case None =>
- val bytes = PIDE.thy_load.file_content(buffer)
+ val bytes = PIDE.resources.file_content(buffer)
val file = new Command.File(node_name.node, buffer.getSegment(0, buffer.getLength))
_blob = Some((bytes, file))
(bytes, file)
--- a/src/Tools/jEdit/src/find_dockable.scala Tue Mar 18 09:39:07 2014 -0700
+++ b/src/Tools/jEdit/src/find_dockable.scala Tue Mar 18 21:02:33 2014 +0100
@@ -131,7 +131,7 @@
private val context_entries =
new Context_Entry("", "current context") ::
- PIDE.thy_load.loaded_theories.toList.sorted.map(name => Context_Entry(name, name))
+ PIDE.resources.loaded_theories.toList.sorted.map(name => Context_Entry(name, name))
private val context = new ComboBox[Context_Entry](context_entries) {
tooltip = "Search in pre-loaded theory (default: context of current command)"
--- a/src/Tools/jEdit/src/isabelle_sidekick.scala Tue Mar 18 09:39:07 2014 -0700
+++ b/src/Tools/jEdit/src/isabelle_sidekick.scala Tue Mar 18 21:02:33 2014 +0100
@@ -133,7 +133,7 @@
class Isabelle_Sidekick_Default extends
- Isabelle_Sidekick_Structure("isabelle", PIDE.thy_load.theory_node_name)
+ Isabelle_Sidekick_Structure("isabelle", PIDE.resources.theory_node_name)
class Isabelle_Sidekick_Options extends
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/jedit_resources.scala Tue Mar 18 21:02:33 2014 +0100
@@ -0,0 +1,123 @@
+/* Title: Tools/jEdit/src/jedit_resources.scala
+ Author: Makarius
+
+Resources for theories and auxiliary files, based on jEdit buffer
+content and virtual file-systems.
+*/
+
+package isabelle.jedit
+
+
+import isabelle._
+
+import java.io.{File => JFile, IOException, ByteArrayOutputStream}
+import javax.swing.text.Segment
+
+import org.gjt.sp.jedit.io.{VFS, FileVFS, VFSFile, VFSManager}
+import org.gjt.sp.jedit.MiscUtilities
+import org.gjt.sp.jedit.{jEdit, View, Buffer}
+import org.gjt.sp.jedit.bufferio.BufferIORequest
+
+
+class JEdit_Resources(loaded_theories: Set[String] = Set.empty, base_syntax: Outer_Syntax)
+ extends Resources(loaded_theories, base_syntax)
+{
+ /* document node names */
+
+ def node_name(buffer: Buffer): Document.Node.Name =
+ {
+ val node = JEdit_Lib.buffer_name(buffer)
+ val theory = Thy_Header.thy_name(node).getOrElse("")
+ val master_dir = if (theory == "") "" else buffer.getDirectory
+ Document.Node.Name(node, master_dir, theory)
+ }
+
+ def theory_node_name(buffer: Buffer): Option[Document.Node.Name] =
+ {
+ val name = node_name(buffer)
+ if (name.is_theory) Some(name) else None
+ }
+
+
+ /* file-system operations */
+
+ override def append(dir: String, source_path: Path): String =
+ {
+ val path = source_path.expand
+ if (dir == "" || path.is_absolute) Isabelle_System.platform_path(path)
+ else {
+ val vfs = VFSManager.getVFSForPath(dir)
+ if (vfs.isInstanceOf[FileVFS])
+ MiscUtilities.resolveSymlinks(
+ vfs.constructPath(dir, Isabelle_System.platform_path(path)))
+ else vfs.constructPath(dir, Isabelle_System.standard_path(path))
+ }
+ }
+
+ override def with_thy_text[A](name: Document.Node.Name, f: CharSequence => A): A =
+ {
+ Swing_Thread.now {
+ JEdit_Lib.jedit_buffer(name.node) match {
+ case Some(buffer) =>
+ JEdit_Lib.buffer_lock(buffer) {
+ Some(f(buffer.getSegment(0, buffer.getLength)))
+ }
+ case None => None
+ }
+ } getOrElse {
+ val file = new JFile(name.node) // FIXME load URL via jEdit VFS (!?)
+ if (!file.exists || !file.isFile) error("No such file: " + quote(file.toString))
+ f(File.read(file))
+ }
+ }
+
+ def check_file(view: View, path: String): Boolean =
+ {
+ val vfs = VFSManager.getVFSForPath(path)
+ val session = vfs.createVFSSession(path, view)
+
+ try {
+ session != null && {
+ try {
+ val file = vfs._getFile(session, path, view)
+ file != null && file.isReadable && file.getType == VFSFile.FILE
+ }
+ catch { case _: IOException => false }
+ }
+ }
+ finally {
+ try { vfs._endVFSSession(session, view) }
+ catch { case _: IOException => }
+ }
+ }
+
+
+ /* file content */
+
+ def file_content(buffer: Buffer): Bytes =
+ {
+ val path = buffer.getPath
+ val vfs = VFSManager.getVFSForPath(path)
+ val content =
+ new BufferIORequest(null, buffer, null, vfs, path) {
+ def _run() { }
+ def apply(): Bytes =
+ {
+ val out =
+ new ByteArrayOutputStream(buffer.getLength + 1) {
+ def content(): Bytes = Bytes(this.buf, 0, this.count)
+ }
+ write(buffer, out)
+ out.content()
+ }
+ }
+ content()
+ }
+
+
+ /* theory text edits */
+
+ override def syntax_changed(): Unit =
+ Swing_Thread.later { jEdit.propertiesChanged() }
+}
+
--- a/src/Tools/jEdit/src/jedit_thy_load.scala Tue Mar 18 09:39:07 2014 -0700
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,121 +0,0 @@
-/* Title: Tools/jEdit/src/jedit_thy_load.scala
- Author: Makarius
-
-Primitives for loading theory files, based on jEdit buffer content.
-*/
-
-package isabelle.jedit
-
-
-import isabelle._
-
-import java.io.{File => JFile, IOException, ByteArrayOutputStream}
-import javax.swing.text.Segment
-
-import org.gjt.sp.jedit.io.{VFS, FileVFS, VFSFile, VFSManager}
-import org.gjt.sp.jedit.MiscUtilities
-import org.gjt.sp.jedit.{jEdit, View, Buffer}
-import org.gjt.sp.jedit.bufferio.BufferIORequest
-
-class JEdit_Thy_Load(loaded_theories: Set[String] = Set.empty, base_syntax: Outer_Syntax)
- extends Thy_Load(loaded_theories, base_syntax)
-{
- /* document node names */
-
- def node_name(buffer: Buffer): Document.Node.Name =
- {
- val node = JEdit_Lib.buffer_name(buffer)
- val theory = Thy_Header.thy_name(node).getOrElse("")
- val master_dir = if (theory == "") "" else buffer.getDirectory
- Document.Node.Name(node, master_dir, theory)
- }
-
- def theory_node_name(buffer: Buffer): Option[Document.Node.Name] =
- {
- val name = node_name(buffer)
- if (name.is_theory) Some(name) else None
- }
-
-
- /* file-system operations */
-
- override def append(dir: String, source_path: Path): String =
- {
- val path = source_path.expand
- if (dir == "" || path.is_absolute) Isabelle_System.platform_path(path)
- else {
- val vfs = VFSManager.getVFSForPath(dir)
- if (vfs.isInstanceOf[FileVFS])
- MiscUtilities.resolveSymlinks(
- vfs.constructPath(dir, Isabelle_System.platform_path(path)))
- else vfs.constructPath(dir, Isabelle_System.standard_path(path))
- }
- }
-
- override def with_thy_text[A](name: Document.Node.Name, f: CharSequence => A): A =
- {
- Swing_Thread.now {
- JEdit_Lib.jedit_buffer(name.node) match {
- case Some(buffer) =>
- JEdit_Lib.buffer_lock(buffer) {
- Some(f(buffer.getSegment(0, buffer.getLength)))
- }
- case None => None
- }
- } getOrElse {
- val file = new JFile(name.node) // FIXME load URL via jEdit VFS (!?)
- if (!file.exists || !file.isFile) error("No such file: " + quote(file.toString))
- f(File.read(file))
- }
- }
-
- def check_file(view: View, path: String): Boolean =
- {
- val vfs = VFSManager.getVFSForPath(path)
- val session = vfs.createVFSSession(path, view)
-
- try {
- session != null && {
- try {
- val file = vfs._getFile(session, path, view)
- file != null && file.isReadable && file.getType == VFSFile.FILE
- }
- catch { case _: IOException => false }
- }
- }
- finally {
- try { vfs._endVFSSession(session, view) }
- catch { case _: IOException => }
- }
- }
-
-
- /* file content */
-
- def file_content(buffer: Buffer): Bytes =
- {
- val path = buffer.getPath
- val vfs = VFSManager.getVFSForPath(path)
- val content =
- new BufferIORequest(null, buffer, null, vfs, path) {
- def _run() { }
- def apply(): Bytes =
- {
- val out =
- new ByteArrayOutputStream(buffer.getLength + 1) {
- def content(): Bytes = Bytes(this.buf, 0, this.count)
- }
- write(buffer, out)
- out.content()
- }
- }
- content()
- }
-
-
- /* theory text edits */
-
- override def syntax_changed(): Unit =
- Swing_Thread.later { jEdit.propertiesChanged() }
-}
-
--- a/src/Tools/jEdit/src/plugin.scala Tue Mar 18 09:39:07 2014 -0700
+++ b/src/Tools/jEdit/src/plugin.scala Tue Mar 18 21:02:33 2014 +0100
@@ -36,12 +36,12 @@
@volatile var startup_notified = false
@volatile var plugin: Plugin = null
- @volatile var session: Session = new Session(new JEdit_Thy_Load(Set.empty, Outer_Syntax.empty))
+ @volatile var session: Session = new Session(new JEdit_Resources(Set.empty, Outer_Syntax.empty))
def options_changed() { plugin.options_changed() }
- def thy_load(): JEdit_Thy_Load =
- session.thy_load.asInstanceOf[JEdit_Thy_Load]
+ def resources(): JEdit_Resources =
+ session.resources.asInstanceOf[JEdit_Resources]
lazy val editor = new JEdit_Editor
@@ -109,7 +109,7 @@
if buffer != null && !buffer.isLoading && !buffer.getBooleanProperty(Buffer.GZIPPED)
} {
JEdit_Lib.buffer_lock(buffer) {
- val node_name = thy_load.node_name(buffer)
+ val node_name = resources.node_name(buffer)
val model =
document_model(buffer) match {
case Some(model) if model.node_name == node_name => model
@@ -202,10 +202,10 @@
if model.is_theory
} yield (model.node_name, Position.none)
- val thy_info = new Thy_Info(PIDE.thy_load)
+ val thy_info = new Thy_Info(PIDE.resources)
// FIXME avoid I/O in Swing thread!?!
val files = thy_info.dependencies(thys).deps.map(_.name.node).
- filter(file => !loaded_buffer(file) && PIDE.thy_load.check_file(view, file))
+ filter(file => !loaded_buffer(file) && PIDE.resources.check_file(view, file))
if (!files.isEmpty) {
if (PIDE.options.bool("jedit_auto_load")) {
@@ -349,9 +349,9 @@
JEdit_Lib.jedit_text_areas.foreach(Completion_Popup.Text_Area.init _)
val content = Isabelle_Logic.session_content(false)
- val thy_load = new JEdit_Thy_Load(content.loaded_theories, content.syntax)
+ val resources = new JEdit_Resources(content.loaded_theories, content.syntax)
- PIDE.session = new Session(thy_load) {
+ PIDE.session = new Session(resources) {
override def output_delay = PIDE.options.seconds("editor_output_delay")
override def reparse_limit = PIDE.options.int("editor_reparse_limit")
}
--- a/src/Tools/jEdit/src/rendering.scala Tue Mar 18 09:39:07 2014 -0700
+++ b/src/Tools/jEdit/src/rendering.scala Tue Mar 18 21:02:33 2014 +0100
@@ -239,6 +239,7 @@
val keyword2_color = color_value("keyword2_color")
val keyword3_color = color_value("keyword3_color")
val quasi_keyword_color = color_value("quasi_keyword_color")
+ val improper_color = color_value("improper_color")
val operator_color = color_value("operator_color")
val caret_invisible_color = color_value("caret_invisible_color")
val completion_color = color_value("completion_color")
@@ -335,7 +336,7 @@
{
case (links, Text.Info(info_range, XML.Elem(Markup.Path(name), _)))
if Path.is_valid(name) =>
- val jedit_file = PIDE.thy_load.append(snapshot.node_name.master_dir, Path.explode(name))
+ val jedit_file = PIDE.resources.append(snapshot.node_name.master_dir, Path.explode(name))
val link = PIDE.editor.hyperlink_file(jedit_file)
Some(links :+ Text.Info(snapshot.convert(info_range), link))
@@ -469,7 +470,7 @@
Some(add(prev, r, (true, XML.Text(txt1 + txt2))))
case (prev, Text.Info(r, XML.Elem(Markup.Path(name), _)))
if Path.is_valid(name) =>
- val jedit_file = PIDE.thy_load.append(snapshot.node_name.master_dir, Path.explode(name))
+ val jedit_file = PIDE.resources.append(snapshot.node_name.master_dir, Path.explode(name))
val text = "path " + quote(name) + "\nfile " + quote(jedit_file)
Some(add(prev, r, (true, XML.Text(text))))
case (prev, Text.Info(r, XML.Elem(Markup.Url(name), _))) =>
@@ -654,6 +655,7 @@
Markup.KEYWORD2 -> keyword2_color,
Markup.KEYWORD3 -> keyword3_color,
Markup.QUASI_KEYWORD -> quasi_keyword_color,
+ Markup.IMPROPER -> improper_color,
Markup.OPERATOR -> operator_color,
Markup.STRING -> Color.BLACK,
Markup.ALTSTRING -> Color.BLACK,
--- a/src/Tools/jEdit/src/theories_dockable.scala Tue Mar 18 09:39:07 2014 -0700
+++ b/src/Tools/jEdit/src/theories_dockable.scala Tue Mar 18 21:02:33 2014 +0100
@@ -192,7 +192,7 @@
}).filter(_._1.is_theory)
val nodes_status1 =
(nodes_status /: iterator)({ case (status, (name, node)) =>
- if (PIDE.thy_load.loaded_theories(name.theory)) status
+ if (PIDE.resources.loaded_theories(name.theory)) status
else status + (name -> Protocol.node_status(snapshot.state, snapshot.version, node)) })
if (nodes_status != nodes_status1) {
--- a/src/Tools/jEdit/src/timing_dockable.scala Tue Mar 18 09:39:07 2014 -0700
+++ b/src/Tools/jEdit/src/timing_dockable.scala Tue Mar 18 21:02:33 2014 +0100
@@ -186,7 +186,7 @@
}
val nodes_timing1 =
(nodes_timing /: iterator)({ case (timing1, (name, node)) =>
- if (PIDE.thy_load.loaded_theories(name.theory)) timing1
+ if (PIDE.resources.loaded_theories(name.theory)) timing1
else {
val node_timing =
Protocol.node_timing(snapshot.state, snapshot.version, node, timing_threshold)