# HG changeset patch # User wenzelm # Date 1395172953 -3600 # Node ID 3250d70c8d0bf646452ac0fa8101d31cb26551ab # Parent 32b7eafc5a52490c8e831eeb06052a4c14372788# Parent c7c85cdb725dbfeac6048aeef520d3b0d8bf74f6 merged; diff -r 32b7eafc5a52 -r 3250d70c8d0b NEWS --- 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. diff -r 32b7eafc5a52 -r 3250d70c8d0b src/CCL/CCL.thy --- 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 diff -r 32b7eafc5a52 -r 3250d70c8d0b src/CCL/Term.thy --- 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 diff -r 32b7eafc5a52 -r 3250d70c8d0b src/CCL/Type.thy --- 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 diff -r 32b7eafc5a52 -r 3250d70c8d0b src/Doc/Codegen/Setup.thy --- 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" diff -r 32b7eafc5a52 -r 3250d70c8d0b src/Doc/IsarImplementation/ML.thy --- 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} diff -r 32b7eafc5a52 -r 3250d70c8d0b src/Doc/Tutorial/ToyList/ToyList_Test.thy --- 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; diff -r 32b7eafc5a52 -r 3250d70c8d0b src/Doc/antiquote_setup.ML --- 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 *) diff -r 32b7eafc5a52 -r 3250d70c8d0b src/FOLP/IFOLP.thy --- 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 diff -r 32b7eafc5a52 -r 3250d70c8d0b src/HOL/Bali/AxSem.thy --- 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] diff -r 32b7eafc5a52 -r 3250d70c8d0b src/HOL/Bali/Eval.thy --- 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!] diff -r 32b7eafc5a52 -r 3250d70c8d0b src/HOL/Bali/Evaln.thy --- 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\Norm s\In1l (Callee l e)\\n\ (v,s') = False" diff -r 32b7eafc5a52 -r 3250d70c8d0b src/HOL/Bali/Example.thy --- 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 diff -r 32b7eafc5a52 -r 3250d70c8d0b src/HOL/Bali/Term.thy --- 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 \ bool" where "is_stmt t = (\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] diff -r 32b7eafc5a52 -r 3250d70c8d0b src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy --- 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 \ nat" +fun degree :: "poly \ nat" where "degree (CN c 0 p) = 1 + degree p" | "degree p = 0" -fun head:: "poly \ poly" +fun head :: "poly \ poly" where "head (CN c 0 p) = head p" | "head p = p" (* More general notions of degree and head *) -fun degreen:: "poly \ nat \ nat" +fun degreen :: "poly \ nat \ nat" where "degreen (CN c n p) = (\m. if n = m then 1 + degreen p n else 0)" | "degreen p = (\m. 0)" -fun headn:: "poly \ nat \ poly" +fun headn :: "poly \ nat \ poly" where "headn (CN c n p) = (\m. if n \ m then headn p m else CN c n p)" | "headn p = (\m. p)" -fun coefficients:: "poly \ poly list" +fun coefficients :: "poly \ poly list" where "coefficients (CN c 0 p) = c # coefficients p" | "coefficients p = [p]" -fun isconstant:: "poly \ bool" +fun isconstant :: "poly \ bool" where "isconstant (CN c 0 p) = False" | "isconstant p = True" -fun behead:: "poly \ poly" +fun behead :: "poly \ 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 \ Num" +fun headconst :: "poly \ Num" where "headconst (CN c n p) = headconst p" | "headconst (C n) = n" @@ -679,11 +679,11 @@ shows "isnpolyh p n0 \ isnpolyh q n1 \ p *\<^sub>p q = 0\<^sub>p \ p = 0\<^sub>p \ 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 \ isnpolyh q n1 \ m \ min n0 n1 \ degreen (p *\<^sub>p q) m = (if p = 0\<^sub>p \ 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 \ 0\<^sub>p" + assumes "isnpoly p" + and "p \ 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 \ 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: "\p. isnpolyh p n \ isnpolyh (f p) n" - and np: "isnpolyh p n" + assumes "\p. isnpolyh p n \ 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) \ 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 \ degree p = 0 \ 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' \ 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': "\c \ set (coefficients p). wf_bs bs c \ wf_bs (x#bs) p" +lemma wf_bs_coefficients': "\c \ set (coefficients p). wf_bs bs c \ wf_bs (x # bs) p" by (induct p rule: coefficients.induct) (auto simp add: wf_bs_def) lemma coefficients_Nil[simp]: "coefficients p \ []" @@ -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) \ wf_bs (x#bs) p" +lemma wf_bs_decrpoly: "wf_bs bs (decrpoly p) \ wf_bs (x # bs) p" unfolding wf_bs_def by (induct p rule: decrpoly.induct) auto lemma length_le_list_ex: "length xs \ n \ \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 \ p\ 0\<^sub>p \ 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 \ degree (polyneg p) = degree p" by (induct p arbitrary: n rule: degree.induct) auto -lemma polyneg_head: "isnpolyh p n \ head(polyneg p) = polyneg (head p)" +lemma polyneg_head: "isnpolyh p n \ 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 \ 0\<^sub>p" - shows "polydivide_aux a n p k s = (k',r) \ k' \ k \ (degree r = 0 \ degree r < degree p) \ + and ndp: "degree p = n" + and pnz: "p \ 0\<^sub>p" + shows "polydivide_aux a n p k s = (k', r) \ k' \ k \ (degree r = 0 \ degree r < degree p) \ (\nr. isnpolyh r nr) \ (\q n1. isnpolyh q n1 \ (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 \ s -\<^sub>p ?p' = 0\<^sub>p" by simp + have "degree (s -\<^sub>p ?p') < degree s \ 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:"\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 \ \ isconstant p" lemma isnonconstant_pnormal_iff: - assumes nc: "isnonconstant p" + assumes "isnonconstant p" shows "pnormal (polypoly bs p) \ Ipoly bs (head p) \ 0" proof let ?p = "polypoly bs p" assume H: "pnormal ?p" have csz: "coefficients p \ []" - 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) \ 0" by (simp add: polypoly_def) @@ -1993,7 +1994,7 @@ assume h: "\head p\\<^sub>p\<^bsup>bs\<^esup> \ 0" let ?p = "polypoly bs p" have csz: "coefficients p \ []" - using nc by (cases p) auto + using assms by (cases p) auto then have pz: "?p \ []" 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) \ Ipoly bs (head p) \ 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 "\head p\\<^sub>p\<^bsup>bs\<^esup> \ 0" unfolding nonconstant_def by blast next let ?p = "polypoly bs p" assume h: "\head p\\<^sub>p\<^bsup>bs\<^esup> \ 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) \ \head p\\<^sub>p\<^bsup>bs\<^esup> \ 0" proof let ?p = "polypoly bs p" assume H: "degree p = Polynomial_List.degree ?p" - from isnonconstant_coefficients_length[OF inc] have pz: "?p \ []" + from isnonconstant_coefficients_length[OF assms] have pz: "?p \ []" 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 "\head p\\<^sub>p\<^bsup>bs\<^esup> \ 0" + with isnonconstant_pnormal_iff[OF assms] show "\head p\\<^sub>p\<^bsup>bs\<^esup> \ 0" by blast next let ?p = "polypoly bs p" assume H: "\head p\\<^sub>p\<^bsup>bs\<^esup> \ 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 \ nat \ poly \ 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)" diff -r 32b7eafc5a52 -r 3250d70c8d0b src/HOL/SMT_Examples/boogie.ML --- 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; diff -r 32b7eafc5a52 -r 3250d70c8d0b src/HOL/SPARK/Tools/spark_commands.ML --- 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 diff -r 32b7eafc5a52 -r 3250d70c8d0b src/HOL/Tools/SMT/smt_config.ML --- 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 diff -r 32b7eafc5a52 -r 3250d70c8d0b src/HOL/Tools/SMT2/smt2_config.ML --- 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 diff -r 32b7eafc5a52 -r 3250d70c8d0b src/HOL/Tools/recdef.ML --- 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 = diff -r 32b7eafc5a52 -r 3250d70c8d0b src/HOL/UNITY/Comp/Alloc.thy --- 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!] diff -r 32b7eafc5a52 -r 3250d70c8d0b src/Pure/Isar/args.ML --- 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 **) diff -r 32b7eafc5a52 -r 3250d70c8d0b src/Pure/Isar/class.ML --- 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; diff -r 32b7eafc5a52 -r 3250d70c8d0b src/Pure/Isar/code.ML --- 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); diff -r 32b7eafc5a52 -r 3250d70c8d0b src/Pure/Isar/context_rules.ML --- 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; diff -r 32b7eafc5a52 -r 3250d70c8d0b src/Pure/Isar/isar_cmd.ML --- 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")); diff -r 32b7eafc5a52 -r 3250d70c8d0b src/Pure/Isar/locale.ML --- 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"); diff -r 32b7eafc5a52 -r 3250d70c8d0b src/Pure/Isar/method.ML --- 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"); diff -r 32b7eafc5a52 -r 3250d70c8d0b src/Pure/Isar/outer_syntax.ML --- 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; diff -r 32b7eafc5a52 -r 3250d70c8d0b src/Pure/Isar/parse.ML --- 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; diff -r 32b7eafc5a52 -r 3250d70c8d0b src/Pure/Isar/parse.scala --- 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 => diff -r 32b7eafc5a52 -r 3250d70c8d0b src/Pure/Isar/parse_spec.ML --- 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 []; diff -r 32b7eafc5a52 -r 3250d70c8d0b src/Pure/Isar/proof_context.ML --- 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 diff -r 32b7eafc5a52 -r 3250d70c8d0b src/Pure/Isar/token.ML --- 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; diff -r 32b7eafc5a52 -r 3250d70c8d0b src/Pure/ML/ml_antiquotation.ML --- 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; diff -r 32b7eafc5a52 -r 3250d70c8d0b src/Pure/ML/ml_antiquotations.ML --- /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; + diff -r 32b7eafc5a52 -r 3250d70c8d0b src/Pure/ML/ml_context.ML --- 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; diff -r 32b7eafc5a52 -r 3250d70c8d0b src/Pure/ML/ml_env.ML --- 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, diff -r 32b7eafc5a52 -r 3250d70c8d0b src/Pure/ML/ml_thms.ML --- 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; diff -r 32b7eafc5a52 -r 3250d70c8d0b src/Pure/PIDE/document.ML --- 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 diff -r 32b7eafc5a52 -r 3250d70c8d0b src/Pure/PIDE/markup.ML --- 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"; diff -r 32b7eafc5a52 -r 3250d70c8d0b src/Pure/PIDE/markup.scala --- 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" diff -r 32b7eafc5a52 -r 3250d70c8d0b src/Pure/PIDE/resources.ML --- /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; diff -r 32b7eafc5a52 -r 3250d70c8d0b src/Pure/PIDE/resources.scala --- /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() { } +} + diff -r 32b7eafc5a52 -r 3250d70c8d0b src/Pure/PIDE/session.ML --- /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; diff -r 32b7eafc5a52 -r 3250d70c8d0b src/Pure/PIDE/session.scala --- /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) } +} diff -r 32b7eafc5a52 -r 3250d70c8d0b src/Pure/Proof/extraction.ML --- 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"); diff -r 32b7eafc5a52 -r 3250d70c8d0b src/Pure/Proof/proof_syntax.ML --- 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>\\_./ _)", [0, 3], 3)), - (Lexicon.mark_const "Appt", [proofT, aT] ---> proofT, Mixfix ("(1_ \\/ _)", [4, 5], 4)), - (Lexicon.mark_const "AppP", [proofT, proofT] ---> proofT, Mixfix ("(1_ \\/ _)", [4, 5], 4))] + [("_Lam", [paramsT, proofT] ---> proofT, Mixfix ("(1\<^bold>\_./ _)", [0, 3], 3)), + (Lexicon.mark_const "Appt", [proofT, aT] ---> proofT, Mixfix ("(1_ \/ _)", [4, 5], 4)), + (Lexicon.mark_const "AppP", [proofT, proofT] ---> proofT, Mixfix ("(1_ \/ _)", [4, 5], 4))] |> Sign.add_trrules (map Syntax.Parse_Print_Rule [(Ast.mk_appl (Ast.Constant "_Lam") [Ast.mk_appl (Ast.Constant "_Lam0") diff -r 32b7eafc5a52 -r 3250d70c8d0b src/Pure/Pure.thy --- 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" diff -r 32b7eafc5a52 -r 3250d70c8d0b src/Pure/ROOT --- 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" diff -r 32b7eafc5a52 -r 3250d70c8d0b src/Pure/ROOT.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"; diff -r 32b7eafc5a52 -r 3250d70c8d0b src/Pure/System/session.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; diff -r 32b7eafc5a52 -r 3250d70c8d0b src/Pure/System/session.scala --- 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) } -} diff -r 32b7eafc5a52 -r 3250d70c8d0b src/Pure/Thy/term_style.ML --- 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; diff -r 32b7eafc5a52 -r 3250d70c8d0b src/Pure/Thy/thy_info.ML --- 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; diff -r 32b7eafc5a52 -r 3250d70c8d0b src/Pure/Thy/thy_info.scala --- 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) diff -r 32b7eafc5a52 -r 3250d70c8d0b src/Pure/Thy/thy_load.ML --- 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; diff -r 32b7eafc5a52 -r 3250d70c8d0b src/Pure/Thy/thy_load.scala --- 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() { } -} - diff -r 32b7eafc5a52 -r 3250d70c8d0b src/Pure/Thy/thy_output.ML --- 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))); diff -r 32b7eafc5a52 -r 3250d70c8d0b src/Pure/Thy/thy_syntax.scala --- 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) diff -r 32b7eafc5a52 -r 3250d70c8d0b src/Pure/Tools/build.scala --- 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 => diff -r 32b7eafc5a52 -r 3250d70c8d0b src/Pure/Tools/proof_general.ML --- 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; diff -r 32b7eafc5a52 -r 3250d70c8d0b src/Pure/build-jars --- 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 diff -r 32b7eafc5a52 -r 3250d70c8d0b src/Pure/pure_syn.ML --- 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 diff -r 32b7eafc5a52 -r 3250d70c8d0b src/Pure/simplifier.ML --- 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)) diff -r 32b7eafc5a52 -r 3250d70c8d0b src/Sequents/Washing.thy --- 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 *) diff -r 32b7eafc5a52 -r 3250d70c8d0b src/Tools/Code/code_runtime.ML --- 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 diff -r 32b7eafc5a52 -r 3250d70c8d0b src/Tools/Code/code_target.ML --- 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 diff -r 32b7eafc5a52 -r 3250d70c8d0b src/Tools/jEdit/etc/options --- 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" diff -r 32b7eafc5a52 -r 3250d70c8d0b src/Tools/jEdit/lib/Tools/jedit --- 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" diff -r 32b7eafc5a52 -r 3250d70c8d0b src/Tools/jEdit/src/completion_popup.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 } } diff -r 32b7eafc5a52 -r 3250d70c8d0b src/Tools/jEdit/src/document_model.scala --- 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) diff -r 32b7eafc5a52 -r 3250d70c8d0b src/Tools/jEdit/src/find_dockable.scala --- 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)" diff -r 32b7eafc5a52 -r 3250d70c8d0b src/Tools/jEdit/src/isabelle_sidekick.scala --- 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 diff -r 32b7eafc5a52 -r 3250d70c8d0b src/Tools/jEdit/src/jedit_resources.scala --- /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() } +} + diff -r 32b7eafc5a52 -r 3250d70c8d0b src/Tools/jEdit/src/jedit_thy_load.scala --- 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() } -} - diff -r 32b7eafc5a52 -r 3250d70c8d0b src/Tools/jEdit/src/plugin.scala --- 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") } diff -r 32b7eafc5a52 -r 3250d70c8d0b src/Tools/jEdit/src/rendering.scala --- 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, diff -r 32b7eafc5a52 -r 3250d70c8d0b src/Tools/jEdit/src/theories_dockable.scala --- 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) { diff -r 32b7eafc5a52 -r 3250d70c8d0b src/Tools/jEdit/src/timing_dockable.scala --- 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)