# HG changeset patch # User wenzelm # Date 1392753613 -3600 # Node ID 439d40b226d1a4ab707ae1f7d8e9026f3a275166 # Parent 4394bb0b522b5bfd8e6b142cff8682b7f4b38ea5# Parent 88c40aff747dee1fad7a099ca19fbe2472fdb425 merged diff -r 4394bb0b522b -r 439d40b226d1 NEWS --- a/NEWS Tue Feb 18 17:56:48 2014 +0100 +++ b/NEWS Tue Feb 18 21:00:13 2014 +0100 @@ -358,6 +358,13 @@ pass runtime Proof.context (and ensure that the simplified entity actually belongs to it). +* Subtle change of semantics of Thm.eq_thm: theory stamps are not +compared (according to Thm.thm_ord), but assumed to be covered by the +current background theory. Thus equivalent data produced in different +branches of the theory graph usually coincides (e.g. relevant for +theory merge). Note that the softer Thm.eq_thm_prop is often more +appropriate than Thm.eq_thm. + *** System *** diff -r 4394bb0b522b -r 439d40b226d1 etc/symbols --- a/etc/symbols Tue Feb 18 17:56:48 2014 +0100 +++ b/etc/symbols Tue Feb 18 21:00:13 2014 +0100 @@ -350,6 +350,7 @@ \ code: 0x0023ce \ code: 0x002039 group: punctuation font: IsabelleText abbrev: << \ code: 0x00203a group: punctuation font: IsabelleText abbrev: >> +\ code: 0x002302 font: IsabelleText \<^sub> code: 0x0021e9 group: control font: IsabelleText \<^sup> code: 0x0021e7 group: control font: IsabelleText \<^bold> code: 0x002759 group: control font: IsabelleText diff -r 4394bb0b522b -r 439d40b226d1 lib/fonts/IsabelleText.sfd --- a/lib/fonts/IsabelleText.sfd Tue Feb 18 17:56:48 2014 +0100 +++ b/lib/fonts/IsabelleText.sfd Tue Feb 18 21:00:13 2014 +0100 @@ -19,7 +19,7 @@ OS2_WeightWidthSlopeOnly: 0 OS2_UseTypoMetrics: 1 CreationTime: 1050361371 -ModificationTime: 1389823475 +ModificationTime: 1392668982 PfmFamily: 17 TTFWeight: 400 TTFWidth: 5 @@ -2240,9 +2240,9 @@ DisplaySize: -48 AntiAlias: 1 FitToEm: 1 -WinInfo: 9104 16 10 +WinInfo: 8912 16 10 TeXData: 1 0 0 631296 315648 210432 572416 -1048576 210432 783286 444596 497025 792723 393216 433062 380633 303038 157286 324010 404750 52429 2506097 1059062 262144 -BeginChars: 1114189 1095 +BeginChars: 1114189 1096 StartChar: u10000 Encoding: 65536 65536 0 @@ -55572,5 +55572,27 @@ 893 663 l 1,9,-1 EndSplineSet EndChar + +StartChar: house +Encoding: 8962 8962 1095 +Width: 1233 +Flags: W +LayerCount: 2 +Fore +SplineSet +146.5 0 m 9,0,-1 + 146.5 647 l 25,1,-1 + 616 1220 l 25,2,-1 + 1086.5 647 l 25,3,-1 + 1086.5 0 l 17,4,-1 + 146.5 0 l 9,0,-1 +268.5 122 m 17,5,-1 + 964.5 122 l 9,6,-1 + 964.5 591 l 25,7,-1 + 616 1018 l 25,8,-1 + 268.5 591 l 25,9,-1 + 268.5 122 l 17,5,-1 +EndSplineSet +EndChar EndChars EndSplineFont diff -r 4394bb0b522b -r 439d40b226d1 lib/fonts/IsabelleText.ttf Binary file lib/fonts/IsabelleText.ttf has changed diff -r 4394bb0b522b -r 439d40b226d1 lib/fonts/IsabelleTextBold.sfd --- a/lib/fonts/IsabelleTextBold.sfd Tue Feb 18 17:56:48 2014 +0100 +++ b/lib/fonts/IsabelleTextBold.sfd Tue Feb 18 21:00:13 2014 +0100 @@ -19,7 +19,7 @@ OS2_WeightWidthSlopeOnly: 0 OS2_UseTypoMetrics: 1 CreationTime: 1050374980 -ModificationTime: 1389823579 +ModificationTime: 1392669044 PfmFamily: 17 TTFWeight: 700 TTFWidth: 5 @@ -1674,8 +1674,8 @@ DisplaySize: -48 AntiAlias: 1 FitToEm: 1 -WinInfo: 9072 16 10 -BeginChars: 1114112 1084 +WinInfo: 8928 16 10 +BeginChars: 1114112 1085 StartChar: u10000 Encoding: 65536 65536 0 @@ -58502,5 +58502,27 @@ 1067 1072 l 1,9,-1 EndSplineSet EndChar + +StartChar: house +Encoding: 8962 8962 1084 +Width: 1233 +Flags: W +LayerCount: 2 +Fore +SplineSet +110 0 m 9,0,-1 + 110 682 l 25,1,-1 + 616 1220 l 25,2,-1 + 1123 682 l 25,3,-1 + 1123 0 l 17,4,-1 + 110 0 l 9,0,-1 +298 187 m 17,5,-1 + 935 187 l 9,6,-1 + 935 625 l 25,7,-1 + 616 959 l 25,8,-1 + 298 625 l 25,9,-1 + 298 187 l 17,5,-1 +EndSplineSet +EndChar EndChars EndSplineFont diff -r 4394bb0b522b -r 439d40b226d1 lib/fonts/IsabelleTextBold.ttf Binary file lib/fonts/IsabelleTextBold.ttf has changed diff -r 4394bb0b522b -r 439d40b226d1 src/Doc/IsarImplementation/Tactic.thy --- a/src/Doc/IsarImplementation/Tactic.thy Tue Feb 18 17:56:48 2014 +0100 +++ b/src/Doc/IsarImplementation/Tactic.thy Tue Feb 18 21:00:13 2014 +0100 @@ -920,9 +920,8 @@ "thm"} has fewer than @{text "n"} premises. \item @{ML Thm.eq_thm}~@{text "(thm\<^sub>1, thm\<^sub>2)"} reports whether @{text - "thm\<^sub>1"} and @{text "thm\<^sub>2"} are equal. Both theorems must have - compatible background theories. Both theorems must have the same - conclusions, the same set of hypotheses, and the same set of sort + "thm\<^sub>1"} and @{text "thm\<^sub>2"} are equal. Both theorems must have the + same conclusions, the same set of hypotheses, and the same set of sort hypotheses. Names of bound variables are ignored as usual. \item @{ML Thm.eq_thm_prop}~@{text "(thm\<^sub>1, thm\<^sub>2)"} reports whether diff -r 4394bb0b522b -r 439d40b226d1 src/HOL/Predicate_Compile.thy --- a/src/HOL/Predicate_Compile.thy Tue Feb 18 17:56:48 2014 +0100 +++ b/src/HOL/Predicate_Compile.thy Tue Feb 18 21:00:13 2014 +0100 @@ -81,6 +81,7 @@ Core_Data.PredData.map (Graph.new_node (@{const_name contains}, Core_Data.PredData { + pos = Position.thread_data (), intros = [(NONE, @{thm containsI})], elim = SOME @{thm containsE}, preprocessed = true, diff -r 4394bb0b522b -r 439d40b226d1 src/HOL/Tools/Predicate_Compile/core_data.ML --- a/src/HOL/Tools/Predicate_Compile/core_data.ML Tue Feb 18 17:56:48 2014 +0100 +++ b/src/HOL/Tools/Predicate_Compile/core_data.ML Tue Feb 18 21:00:13 2014 +0100 @@ -18,6 +18,7 @@ }; datatype pred_data = PredData of { + pos : Position.T, intros : (string option * thm) list, elim : thm option, preprocessed : bool, @@ -100,6 +101,7 @@ PredfunData {definition = definition, intro = intro, elim = elim, neg_intro = neg_intro} datatype pred_data = PredData of { + pos: Position.T, intros : (string option * thm) list, elim : thm option, preprocessed : bool, @@ -109,13 +111,17 @@ }; fun rep_pred_data (PredData data) = data; +val pos_of = #pos o rep_pred_data; -fun mk_pred_data (((intros, elim), preprocessed), (function_names, (predfun_data, needs_random))) = - PredData {intros = intros, elim = elim, preprocessed = preprocessed, +fun mk_pred_data + (pos, (((intros, elim), preprocessed), (function_names, (predfun_data, needs_random)))) = + PredData {pos = pos, intros = intros, elim = elim, preprocessed = preprocessed, function_names = function_names, predfun_data = predfun_data, needs_random = needs_random} -fun map_pred_data f (PredData {intros, elim, preprocessed, function_names, predfun_data, needs_random}) = - mk_pred_data (f (((intros, elim), preprocessed), (function_names, (predfun_data, needs_random)))) +fun map_pred_data f + (PredData {pos, intros, elim, preprocessed, function_names, predfun_data, needs_random}) = + mk_pred_data + (f (pos, (((intros, elim), preprocessed), (function_names, (predfun_data, needs_random))))) fun eq_option eq (NONE, NONE) = true | eq_option eq (SOME x, SOME y) = eq (x, y) @@ -130,7 +136,13 @@ type T = pred_data Graph.T; val empty = Graph.empty; val extend = I; - val merge = Graph.merge eq_pred_data; + val merge = + Graph.join (fn key => fn (x, y) => + if eq_pred_data (x, y) + then raise Graph.SAME + else + error ("Duplicate predicate declarations for " ^ quote key ^ + Position.here (pos_of x) ^ Position.here (pos_of y))); ); @@ -260,11 +272,13 @@ (case try (Inductive.the_inductive ctxt) name of SOME (info as (_, result)) => let + val thy = Proof_Context.theory_of ctxt + + val pos = Position.thread_data () fun is_intro_of intro = let val (const, _) = strip_comb (HOLogic.dest_Trueprop (concl_of intro)) in (fst (dest_Const const) = name) end; - val thy = Proof_Context.theory_of ctxt val intros = map (preprocess_intro thy) (filter is_intro_of (#intrs result)) val index = find_index (fn s => s = name) (#names (fst info)) val pre_elim = nth (#elims result) index @@ -273,13 +287,13 @@ val nparams = length (Inductive.params_of (#raw_induct result)) val elim = prove_casesrule ctxt (pred, (pre_elim, nparams)) elim_t in - mk_pred_data (((map (pair NONE) intros, SOME elim), true), no_compilation) + mk_pred_data (pos, (((map (pair NONE) intros, SOME elim), true), no_compilation)) end | NONE => error ("No such predicate: " ^ quote name)) fun add_predfun_data name mode data = let - val add = (apsnd o apsnd o apfst) (cons (mode, mk_predfun_data data)) + val add = (apsnd o apsnd o apsnd o apfst) (cons (mode, mk_predfun_data data)) in PredData.map (Graph.map_node name (map_pred_data add)) end fun is_inductive_predicate ctxt name = @@ -305,17 +319,21 @@ (case try (Graph.get_node gr) name of SOME _ => Graph.map_node name (map_pred_data - (apfst (apfst (apfst (fn intros => intros @ [(opt_case_name, thm)]))))) gr + (apsnd (apfst (apfst (apfst (fn intros => intros @ [(opt_case_name, thm)])))))) gr | NONE => Graph.new_node - (name, mk_pred_data ((([(opt_case_name, thm)], NONE), false), no_compilation)) gr) + (name, + mk_pred_data (Position.thread_data (), + (((([(opt_case_name, thm)], NONE), false), no_compilation)))) gr) in PredData.map cons_intro thy end fun set_elim thm = let val (name, _) = dest_Const (fst (strip_comb (HOLogic.dest_Trueprop (hd (prems_of thm))))) - in PredData.map (Graph.map_node name (map_pred_data (apfst (apfst (apsnd (K (SOME thm))))))) end + in + PredData.map (Graph.map_node name (map_pred_data (apsnd (apfst (apfst (apsnd (K (SOME thm)))))))) + end fun register_predicate (constname, intros, elim) thy = let @@ -324,7 +342,8 @@ if not (member (op =) (Graph.keys (PredData.get thy)) constname) then PredData.map (Graph.new_node (constname, - mk_pred_data (((named_intros, SOME elim), false), no_compilation))) thy + mk_pred_data (Position.thread_data (), + (((named_intros, SOME elim), false), no_compilation)))) thy else thy end @@ -345,14 +364,14 @@ fun defined_function_of compilation pred = let - val set = (apsnd o apfst) (cons (compilation, [])) + val set = (apsnd o apsnd o apfst) (cons (compilation, [])) in PredData.map (Graph.map_node pred (map_pred_data set)) end fun set_function_name compilation pred mode name = let - val set = (apsnd o apfst) + val set = (apsnd o apsnd o apfst) (AList.map_default (op =) (compilation, [(mode, name)]) (cons (mode, name))) in PredData.map (Graph.map_node pred (map_pred_data set)) @@ -360,7 +379,7 @@ fun set_needs_random name modes = let - val set = (apsnd o apsnd o apsnd) (K modes) + val set = (apsnd o apsnd o apsnd o apsnd) (K modes) in PredData.map (Graph.map_node name (map_pred_data set)) end @@ -389,7 +408,7 @@ end fun preprocess_intros name thy = - PredData.map (Graph.map_node name (map_pred_data (apfst (fn (rules, preprocessed) => + PredData.map (Graph.map_node name (map_pred_data (apsnd (apfst (fn (rules, preprocessed) => if preprocessed then (rules, preprocessed) else let @@ -401,7 +420,7 @@ val elim' = prove_casesrule ctxt (pred, (elim, 0)) elim_t in ((named_intros', SOME elim'), true) - end)))) + end))))) thy @@ -422,7 +441,7 @@ AList.lookup eq_mode (Symtab.lookup_list (Alt_Compilations_Data.get (Proof_Context.theory_of ctxt)) pred_name) mode -fun force_modes_and_compilations pred_name compilations = +fun force_modes_and_compilations pred_name compilations thy = let (* thm refl is a dummy thm *) val modes = map fst compilations @@ -435,11 +454,14 @@ map (rpair non_random_dummys) Predicate_Compile_Aux.non_random_compilations val alt_compilations = map (apsnd fst) compilations in + thy |> PredData.map (Graph.new_node (pred_name, - mk_pred_data ((([], SOME @{thm refl}), true), (dummy_function_names, ([], needs_random))))) - #> Alt_Compilations_Data.map (Symtab.insert (K false) (pred_name, alt_compilations)) + mk_pred_data + (Position.thread_data (), + ((([], SOME @{thm refl}), true), (dummy_function_names, ([], needs_random)))))) + |> Alt_Compilations_Data.map (Symtab.insert (K false) (pred_name, alt_compilations)) end fun functional_compilation fun_name mode compfuns T = diff -r 4394bb0b522b -r 439d40b226d1 src/Pure/General/path.scala --- a/src/Pure/General/path.scala Tue Feb 18 17:56:48 2014 +0100 +++ b/src/Pure/General/path.scala Tue Feb 18 21:00:13 2014 +0100 @@ -94,7 +94,7 @@ else (List(root_elem(es.head)), es.tail) val elems = raw_elems.filterNot(s => s.isEmpty || s == ".").map(explode_elem) - new Path(norm_elems(elems.reverse ++ roots)) + new Path(norm_elems(elems.reverse ::: roots)) } def is_ok(str: String): Boolean = diff -r 4394bb0b522b -r 439d40b226d1 src/Pure/General/position.ML --- a/src/Pure/General/position.ML Tue Feb 18 17:56:48 2014 +0100 +++ b/src/Pure/General/position.ML Tue Feb 18 21:00:13 2014 +0100 @@ -192,7 +192,7 @@ (SOME i, NONE) => "(line " ^ Markup.print_int i ^ ")" | (SOME i, SOME name) => "(line " ^ Markup.print_int i ^ " of " ^ quote name ^ ")" | (NONE, SOME name) => "(file " ^ quote name ^ ")" - | _ => ""); + | _ => if is_reported pos then "\\" else ""); in if null props then "" else (if s = "" then "" else " ") ^ Markup.markup (Markup.properties props Markup.position) s diff -r 4394bb0b522b -r 439d40b226d1 src/Pure/General/position.scala --- a/src/Pure/General/position.scala Tue Feb 18 17:56:48 2014 +0100 +++ b/src/Pure/General/position.scala Tue Feb 18 21:00:13 2014 +0100 @@ -50,7 +50,7 @@ object Range { - def apply(range: Text.Range): T = Offset(range.start) ++ Offset(range.stop) + def apply(range: Text.Range): T = Offset(range.start) ::: Offset(range.stop) def unapply(pos: T): Option[Text.Range] = (pos, pos) match { case (Offset(start), End_Offset(stop)) if start <= stop => Some(Text.Range(start, stop)) diff -r 4394bb0b522b -r 439d40b226d1 src/Pure/General/pretty.scala --- a/src/Pure/General/pretty.scala Tue Feb 18 17:56:48 2014 +0100 +++ b/src/Pure/General/pretty.scala Tue Feb 18 21:00:13 2014 +0100 @@ -45,12 +45,11 @@ object Block { def apply(i: Int, body: XML.Body): XML.Tree = - XML.Elem(Markup(Markup.BLOCK, Markup.Indent(i)), body) + XML.Elem(Markup.Block(i), body) def unapply(tree: XML.Tree): Option[(Int, XML.Body)] = tree match { - case XML.Elem(Markup(Markup.BLOCK, Markup.Indent(i)), body) => - Some((i, body)) + case XML.Elem(Markup.Block(i), body) => Some((i, body)) case _ => None } } @@ -58,12 +57,11 @@ object Break { def apply(w: Int): XML.Tree = - XML.Elem(Markup(Markup.BREAK, Markup.Width(w)), - List(XML.Text(spaces(w)))) + XML.Elem(Markup.Break(w), List(XML.Text(spaces(w)))) def unapply(tree: XML.Tree): Option[Int] = tree match { - case XML.Elem(Markup(Markup.BREAK, Markup.Width(w)), _) => Some(w) + case XML.Elem(Markup.Break(w), _) => Some(w) case _ => None } } diff -r 4394bb0b522b -r 439d40b226d1 src/Pure/ML/ml_lex.ML --- a/src/Pure/ML/ml_lex.ML Tue Feb 18 17:56:48 2014 +0100 +++ b/src/Pure/ML/ml_lex.ML Tue Feb 18 21:00:13 2014 +0100 @@ -300,7 +300,7 @@ fun read pos txt = let - val _ = Position.report pos Markup.ML_source; + val _ = Position.report pos Markup.language_ML; val syms = Symbol_Pos.explode (txt, pos); val termination = if null syms then [] diff -r 4394bb0b522b -r 439d40b226d1 src/Pure/PIDE/command.scala --- a/src/Pure/PIDE/command.scala Tue Feb 18 17:56:48 2014 +0100 +++ b/src/Pure/PIDE/command.scala Tue Feb 18 21:00:13 2014 +0100 @@ -108,19 +108,17 @@ if id == command.id || id == alt_id => command.chunks.get(file_name) match { case Some(chunk) => - val range = chunk.decode(raw_range) - if (chunk.range.contains(range)) { - val props = Position.purge(atts) - val info: Text.Markup = Text.Info(range, XML.Elem(Markup(name, props), args)) - state.add_markup(file_name, info) + chunk.decode(raw_range).try_restrict(chunk.range) match { + case Some(range) => + if (!range.is_singularity) { + val props = Position.purge(atts) + state.add_markup(file_name, + Text.Info(range, XML.Elem(Markup(name, props), args))) + } + else state + case None => bad(); state } - else { - bad() - state - } - case None => - bad() - state + case None => bad(); state } case XML.Elem(Markup(name, atts), args) @@ -130,9 +128,7 @@ val info: Text.Markup = Text.Info(range, XML.Elem(Markup(name, props), args)) state.add_markup("", info) - case _ => - // FIXME bad() - state + case _ => /* FIXME bad(); */ state } }) case XML.Elem(Markup(name, props), body) => diff -r 4394bb0b522b -r 439d40b226d1 src/Pure/PIDE/markup.ML --- a/src/Pure/PIDE/markup.ML Tue Feb 18 17:56:48 2014 +0100 +++ b/src/Pure/PIDE/markup.ML Tue Feb 18 21:00:13 2014 +0100 @@ -20,6 +20,14 @@ val name: string -> T -> T val kindN: string val instanceN: string + val languageN: string val language: string -> T + val language_sort: T + val language_type: T + val language_term: T + val language_prop: T + val language_ML: T + val language_document: T + val language_text: T val bindingN: string val binding: T val entityN: string val entity: string -> string -> T val get_entity_kind: T -> string option @@ -62,10 +70,6 @@ val inner_cartoucheN: string val inner_cartouche: T val inner_commentN: string val inner_comment: T val token_rangeN: string val token_range: T - val sortN: string val sort: T - val typN: string val typ: T - val termN: string val term: T - val propN: string val prop: T val sortingN: string val sorting: T val typingN: string val typing: T val ML_keyword1N: string val ML_keyword1: T @@ -81,8 +85,6 @@ val ML_openN: string val ML_structN: string val ML_typingN: string val ML_typing: T - val ML_sourceN: string val ML_source: T - val document_sourceN: string val document_source: T val antiquotedN: string val antiquoted: T val antiquoteN: string val antiquote: T val ML_antiquotationN: string @@ -163,6 +165,12 @@ val command_timing: Properties.entry val loading_theory: string -> Properties.T val dest_loading_theory: Properties.T -> string option + val simp_trace_logN: string + val simp_trace_stepN: string + val simp_trace_recurseN: string + val simp_trace_hintN: string + val simp_trace_ignoreN: string + val simp_trace_cancel: serial -> Properties.T val no_output: Output.output * Output.output val default_output: T -> Output.output * Output.output val add_mode: string -> (T -> Output.output * Output.output) -> unit @@ -220,9 +228,9 @@ fun properties more_props ((elem, props): T) = (elem, fold_rev Properties.put more_props props); -fun markup_elem elem = (elem, (elem, []): T); -fun markup_string elem prop = (elem, fn s => (elem, [(prop, s)]): T); -fun markup_int elem prop = (elem, fn i => (elem, [(prop, print_int i)]): T); +fun markup_elem name = (name, (name, []): T); +fun markup_string name prop = (name, fn s => (name, [(prop, s)]): T); +fun markup_int name prop = (name, fn i => (name, [(prop, print_int i)]): T); (* misc properties *) @@ -235,6 +243,20 @@ val instanceN = "instance"; +(* embedded languages *) + +val (languageN, language) = markup_string "language" nameN; + +val language_sort = language "sort"; +val language_type = language "type"; +val language_term = language "term"; +val language_prop = language "prop"; + +val language_ML = language "ML"; +val language_document = language "document"; +val language_text = language "text"; + + (* formal entities *) val (bindingN, binding) = markup_elem "binding"; @@ -317,11 +339,6 @@ val (token_rangeN, token_range) = markup_elem "token_range"; -val (sortN, sort) = markup_elem "sort"; -val (typN, typ) = markup_elem "typ"; -val (termN, term) = markup_elem "term"; -val (propN, prop) = markup_elem "prop"; - val (sortingN, sorting) = markup_elem "sorting"; val (typingN, typing) = markup_elem "typing"; @@ -344,10 +361,7 @@ val (ML_typingN, ML_typing) = markup_elem "ML_typing"; -(* embedded source text *) - -val (ML_sourceN, ML_source) = markup_elem "ML_source"; -val (document_sourceN, document_source) = markup_elem "document_source"; +(* antiquotations *) val (antiquotedN, antiquoted) = markup_elem "antiquoted"; val (antiquoteN, antiquote) = markup_elem "antiquote"; @@ -510,6 +524,16 @@ | dest_loading_theory _ = NONE; +(* simplifier trace *) + +val simp_trace_logN = "simp_trace_log"; +val simp_trace_stepN = "simp_trace_step"; +val simp_trace_recurseN = "simp_trace_recurse"; +val simp_trace_hintN = "simp_trace_hint"; +val simp_trace_ignoreN = "simp_trace_ignore"; + +fun simp_trace_cancel i = [(functionN, "simp_trace_cancel"), (serialN, print_int i)]; + (** print mode operations **) diff -r 4394bb0b522b -r 439d40b226d1 src/Pure/PIDE/markup.scala --- a/src/Pure/PIDE/markup.scala Tue Feb 18 17:56:48 2014 +0100 +++ b/src/Pure/PIDE/markup.scala Tue Feb 18 21:00:13 2014 +0100 @@ -27,6 +27,24 @@ val Empty = Markup("", Nil) val Broken = Markup("broken", Nil) + class Markup_String(val name: String, prop: String) + { + private val Prop = new Properties.String(prop) + + def apply(s: String): Markup = Markup(name, Prop(s)) + def unapply(markup: Markup): Option[String] = + if (markup.name == name) Prop.unapply(markup.properties) else None + } + + class Markup_Int(val name: String, prop: String) + { + private val Prop = new Properties.Int(prop) + + def apply(i: Int): Markup = Markup(name, Prop(i)) + def unapply(markup: Markup): Option[Int] = + if (markup.name == name) Prop.unapply(markup.properties) else None + } + /* formal entities */ @@ -39,9 +57,9 @@ { def unapply(markup: Markup): Option[(String, String)] = markup match { - case Markup(ENTITY, props @ Kind(kind)) => - props match { - case Name(name) => Some(kind, name) + case Markup(ENTITY, props) => + (props, props) match { + case (Kind(kind), Name(name)) => Some(kind, name) case _ => None } case _ => None @@ -67,38 +85,25 @@ val POSITION = "position" + /* embedded languages */ + + val LANGUAGE = "language" + val Language = new Markup_String(LANGUAGE, NAME) + + /* external resources */ val PATH = "path" - - object Path - { - def unapply(markup: Markup): Option[String] = - markup match { - case Markup(PATH, Name(name)) => Some(name) - case _ => None - } - } + val Path = new Markup_String(PATH, NAME) val URL = "url" - - object Url - { - def unapply(markup: Markup): Option[String] = - markup match { - case Markup(URL, Name(name)) => Some(name) - case _ => None - } - } + val Url = new Markup_String(URL, NAME) /* pretty printing */ - val Indent = new Properties.Int("indent") - val BLOCK = "block" - - val Width = new Properties.Int("width") - val BREAK = "break" + val Block = new Markup_Int("block", "indent") + val Break = new Markup_Int("break", "width") val ITEM = "item" val BULLET = "bullet" @@ -138,11 +143,6 @@ val TOKEN_RANGE = "token_range" - val SORT = "sort" - val TYP = "typ" - val TERM = "term" - val PROP = "prop" - val SORTING = "sorting" val TYPING = "typing" @@ -150,10 +150,7 @@ val METHOD = "method" - /* embedded source text */ - - val ML_SOURCE = "ML_source" - val DOCUMENT_SOURCE = "document_source" + /* antiquotations */ val ANTIQUOTED = "antiquoted" val ANTIQUOTE = "antiquote" @@ -392,82 +389,26 @@ } } + /* simplifier trace */ - val TEXT = "text" - val Text = new Properties.String(TEXT) - - val PARENT = "parent" - val Parent = new Properties.Long(PARENT) + val SIMP_TRACE = "simp_trace" - val SUCCESS = "success" - val Success = new Properties.Boolean(SUCCESS) + val SIMP_TRACE_LOG = "simp_trace_log" + val SIMP_TRACE_STEP = "simp_trace_step" + val SIMP_TRACE_RECURSE = "simp_trace_recurse" + val SIMP_TRACE_HINT = "simp_trace_hint" + val SIMP_TRACE_IGNORE = "simp_trace_ignore" - val MEMORY = "memory" - val Memory = new Properties.Boolean(MEMORY) - - val CANCEL_SIMP_TRACE = "simp_trace_cancel" - object Cancel_Simp_Trace + val SIMP_TRACE_CANCEL = "simp_trace_cancel" + object Simp_Trace_Cancel { def unapply(props: Properties.T): Option[Long] = props match { - case (FUNCTION, CANCEL_SIMP_TRACE) :: Serial(id) => Some(id) + case (FUNCTION, SIMP_TRACE_CANCEL) :: Serial(i) => Some(i) case _ => None } } - - val SIMP_TRACE = "simp_trace" - object Simp_Trace - { - def unapply(tree: XML.Tree): Option[(Long, Simplifier_Trace.Answer)] = - tree match { - case XML.Elem(Markup(SIMP_TRACE, props), _) => - (props, props) match { - case (Serial(serial), Name(name)) => - Simplifier_Trace.all_answers.find(_.name == name).map((serial, _)) - case _ => - None - } - case _ => - None - } - } - - /* trace items from the prover */ - - object Simp_Trace_Item - { - - def unapply(tree: XML.Tree): Option[(String, Data)] = - tree match { - case XML.Elem(Markup(RESULT, Serial(serial)), List( - XML.Elem(Markup(markup, props), content) - )) if markup.startsWith("simp_trace_") => - (props, props) match { - case (Text(text), Parent(parent)) => - Some((markup, Data(serial, markup, text, parent, props, content))) - case _ => - None - } - case _ => - None - } - - val LOG = "simp_trace_log" - val STEP = "simp_trace_step" - val RECURSE = "simp_trace_recurse" - val HINT = "simp_trace_hint" - val IGNORE = "simp_trace_ignore" - - case class Data(serial: Long, markup: String, text: String, - parent: Long, props: Properties.T, content: XML.Body) - { - def memory: Boolean = - Memory.unapply(props) getOrElse true - } - - } - } diff -r 4394bb0b522b -r 439d40b226d1 src/Pure/PIDE/protocol.scala --- a/src/Pure/PIDE/protocol.scala Tue Feb 18 17:56:48 2014 +0100 +++ b/src/Pure/PIDE/protocol.scala Tue Feb 18 21:00:13 2014 +0100 @@ -282,10 +282,12 @@ { def elem_positions(props: Properties.T, set: Set[Text.Range]): Set[Text.Range] = props match { - case Position.Reported(id, file_name, range) + case Position.Reported(id, file_name, raw_range) if (id == command_id || id == alt_id) && file_name == chunk.file_name => - val range1 = chunk.decode(range).restrict(chunk.range) - if (range1.is_singularity) set else set + range1 + chunk.decode(raw_range).try_restrict(chunk.range) match { + case Some(range) if !range.is_singularity => set + range + case _ => set + } case _ => set } diff -r 4394bb0b522b -r 439d40b226d1 src/Pure/PIDE/yxml.scala --- a/src/Pure/PIDE/yxml.scala Tue Feb 18 17:56:48 2014 +0100 +++ b/src/Pure/PIDE/yxml.scala Tue Feb 18 21:00:13 2014 +0100 @@ -33,7 +33,7 @@ def tree(t: XML.Tree): Unit = t match { case XML.Elem(Markup(name, atts), ts) => - s += X; s += Y; s++= name; atts.foreach(attrib); s += X + s += X; s += Y; s ++= name; atts.foreach(attrib); s += X ts.foreach(tree) s += X; s += Y; s += X case XML.Text(text) => s ++= text @@ -120,7 +120,7 @@ /* failsafe parsing */ private def markup_broken(source: CharSequence) = - XML.elem(Markup.Broken.name, List(XML.Text(source.toString))) + XML.Elem(Markup.Broken, List(XML.Text(source.toString))) def parse_body_failsafe(source: CharSequence): XML.Body = { diff -r 4394bb0b522b -r 439d40b226d1 src/Pure/Syntax/syntax_phases.ML --- a/src/Pure/Syntax/syntax_phases.ML Tue Feb 18 17:56:48 2014 +0100 +++ b/src/Pure/Syntax/syntax_phases.ML Tue Feb 18 21:00:13 2014 +0100 @@ -342,7 +342,7 @@ Markup.markup Markup.report (Context_Position.reported_text ctxt pos Markup.bad "")); fun parse_sort ctxt = - Syntax.parse_token ctxt Term_XML.Decode.sort Markup.sort + Syntax.parse_token ctxt Term_XML.Decode.sort Markup.language_sort (fn (syms, pos) => parse_tree ctxt "sort" (syms, pos) |> uncurry (report_result ctxt pos) @@ -351,7 +351,7 @@ handle ERROR msg => parse_failed ctxt pos msg "sort"); fun parse_typ ctxt = - Syntax.parse_token ctxt Term_XML.Decode.typ Markup.typ + Syntax.parse_token ctxt Term_XML.Decode.typ Markup.language_type (fn (syms, pos) => parse_tree ctxt "type" (syms, pos) |> uncurry (report_result ctxt pos) @@ -362,8 +362,8 @@ let val (markup, kind, root, constrain) = if is_prop - then (Markup.prop, "proposition", "prop", Type.constraint propT) - else (Markup.term, "term", Config.get ctxt Syntax.root, I); + then (Markup.language_prop, "prop", "prop", Type.constraint propT) + else (Markup.language_term, "term", Config.get ctxt Syntax.root, I); val decode = constrain o Term_XML.Decode.term; in Syntax.parse_token ctxt decode markup @@ -749,8 +749,8 @@ in -val unparse_sort = unparse_t sort_to_ast Printer.pretty_typ_ast Markup.sort; -val unparse_typ = unparse_t typ_to_ast Printer.pretty_typ_ast Markup.typ; +val unparse_sort = unparse_t sort_to_ast Printer.pretty_typ_ast Markup.language_sort; +val unparse_typ = unparse_t typ_to_ast Printer.pretty_typ_ast Markup.language_type; fun unparse_term ctxt = let @@ -760,7 +760,7 @@ in unparse_t (term_to_ast idents (is_some o Syntax.lookup_const syn)) (Printer.pretty_term_ast (not (Pure_Thy.old_appl_syntax thy))) - Markup.term ctxt + Markup.language_term ctxt end; end; diff -r 4394bb0b522b -r 439d40b226d1 src/Pure/System/isabelle_system.scala --- a/src/Pure/System/isabelle_system.scala Tue Feb 18 17:56:48 2014 +0100 +++ b/src/Pure/System/isabelle_system.scala Tue Feb 18 21:00:13 2014 +0100 @@ -267,7 +267,7 @@ def execute_env(cwd: JFile, env: Map[String, String], redirect: Boolean, args: String*): Process = { val cmdline = - if (Platform.is_windows) List(get_cygwin_root() + "\\bin\\env.exe") ++ args + if (Platform.is_windows) List(get_cygwin_root() + "\\bin\\env.exe") ::: args.toList else args val env1 = if (env == null) settings else settings ++ env raw_execute(cwd, env1, redirect, cmdline: _*) @@ -283,7 +283,7 @@ { private val params = List(standard_path(Path.explode("~~/lib/scripts/process")), "group", "-", "no_script") - private val proc = execute_env(cwd, env, redirect, (params ++ args):_*) + private val proc = execute_env(cwd, env, redirect, (params ::: args.toList):_*) // channels @@ -414,7 +414,7 @@ } match { case Some(dir) => val file = standard_path(dir + Path.basic(name)) - process_output(execute(true, (List(file) ++ args): _*)) + process_output(execute(true, (List(file) ::: args.toList): _*)) case None => ("Unknown Isabelle tool: " + name, 2) } } diff -r 4394bb0b522b -r 439d40b226d1 src/Pure/Thy/thy_output.ML --- a/src/Pure/Thy/thy_output.ML Tue Feb 18 17:56:48 2014 +0100 +++ b/src/Pure/Thy/thy_output.ML Tue Feb 18 21:00:13 2014 +0100 @@ -188,7 +188,7 @@ fun check_text (txt, pos) state = - (Position.report pos Markup.document_source; + (Position.report pos Markup.language_document; if Toplevel.is_skipped_proof state then () else ignore (eval_antiquote (#1 (Keyword.get_lexicons ())) state (txt, pos))); @@ -470,6 +470,9 @@ fun pretty_text ctxt = Pretty.chunks o map Pretty.str o map (tweak_line ctxt) o split_lines; +fun pretty_text_report ctxt (s, pos) = + (Context_Position.report ctxt pos Markup.language_text; pretty_text ctxt s); + fun pretty_term ctxt t = Syntax.pretty_term (Variable.auto_fixes t ctxt) t; fun pretty_thm ctxt = pretty_term ctxt o Thm.full_prop_of; @@ -574,7 +577,7 @@ 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) pretty_text #> + basic_entity (Binding.name "text") (Scan.lift (Parse.position Args.name)) 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); diff -r 4394bb0b522b -r 439d40b226d1 src/Pure/Tools/simplifier_trace.ML --- a/src/Pure/Tools/simplifier_trace.ML Tue Feb 18 17:56:48 2014 +0100 +++ b/src/Pure/Tools/simplifier_trace.ML Tue Feb 18 21:00:13 2014 +0100 @@ -13,7 +13,7 @@ structure Simplifier_Trace: SIMPLIFIER_TRACE = struct -(** background data **) +(** context data **) datatype mode = Disabled | Normal | Full @@ -23,7 +23,7 @@ | merge_modes Full _ = Full val empty_breakpoints = - (Item_Net.init (op =) single (* FIXME equality on terms? *), + (Item_Net.init (op aconv) single, Item_Net.init eq_rrule (single o Thm.full_prop_of o #thm)) fun merge_breakpoints ((term_bs1, thm_bs1), (term_bs2, thm_bs2)) = @@ -49,10 +49,11 @@ parent = 0, breakpoints = empty_breakpoints} val extend = I - fun merge ({max_depth = max_depth1, mode = mode1, interactive = interactive1, - memory = memory1, breakpoints = breakpoints1, ...}: T, - {max_depth = max_depth2, mode = mode2, interactive = interactive2, - memory = memory2, breakpoints = breakpoints2, ...}: T) = + fun merge + ({max_depth = max_depth1, mode = mode1, interactive = interactive1, + memory = memory1, breakpoints = breakpoints1, ...}: T, + {max_depth = max_depth2, mode = mode2, interactive = interactive2, + memory = memory2, breakpoints = breakpoints2, ...}: T) = {max_depth = Int.max (max_depth1, max_depth2), depth = 0, mode = merge_modes mode1 mode2, @@ -97,14 +98,17 @@ (term_matches, thm_matches) end + + (** config and attributes **) fun config raw_mode interactive max_depth memory = let - val mode = case raw_mode of - "normal" => Normal - | "full" => Full - | _ => error ("Simplifier_Trace.config: unknown mode " ^ raw_mode) + val mode = + (case raw_mode of + "normal" => Normal + | "full" => Full + | _ => error ("Simplifier_Trace.config: unknown mode " ^ raw_mode)) val update = Data.map (fn {depth, parent, breakpoints, ...} => {max_depth = max_depth, @@ -122,11 +126,15 @@ val thm_breakpoint = Thm.declaration_attribute add_thm_breakpoint + + (** tracing state **) val futures = Synchronized.var "Simplifier_Trace.futures" (Inttab.empty: string future Inttab.table) + + (** markup **) fun output_result (id, data) = @@ -138,14 +146,6 @@ val memoryN = "memory" val successN = "success" -val logN = "simp_trace_log" -val stepN = "simp_trace_step" -val recurseN = "simp_trace_recurse" -val hintN = "simp_trace_hint" -val ignoreN = "simp_trace_ignore" - -val cancelN = "simp_trace_cancel" - type payload = {props: Properties.T, pretty: Pretty.T} @@ -158,15 +158,17 @@ val {max_depth, depth, mode, interactive, memory, parent, ...} = Data.get (Context.Proof ctxt) val eligible = - case mode of + (case mode of Disabled => false | Normal => triggered - | Full => true + | Full => true) - val markup' = if markup = stepN andalso not interactive then logN else markup + val markup' = + if markup = Markup.simp_trace_stepN andalso not interactive + then Markup.simp_trace_logN + else markup in - if not eligible orelse depth > max_depth then - NONE + if not eligible orelse depth > max_depth then NONE else let val {props = more_props, pretty} = payload () @@ -181,15 +183,14 @@ end end + + (** tracing output **) fun send_request (result_id, content) = let fun break () = - (Output.protocol_message - [(Markup.functionN, cancelN), - (serialN, Markup.print_int result_id)] - ""; + (Output.protocol_message (Markup.simp_trace_cancel result_id) ""; Synchronized.change futures (Inttab.delete_safe result_id)) val promise = Future.promise break : string future in @@ -209,10 +210,8 @@ val term_triggered = not (null matching_terms) val text = - if unconditional then - "Apply rewrite rule?" - else - "Apply conditional rewrite rule?" + if unconditional then "Apply rewrite rule?" + else "Apply conditional rewrite rule?" fun payload () = let @@ -233,8 +232,7 @@ in if not (null matching_terms) then [Pretty.block (Pretty.fbreaks (Pretty.str "Matching terms:" :: items))] - else - [] + else [] end val pretty = @@ -269,14 +267,14 @@ in if not interactive then (output_result result; Future.value (SOME (put mode false))) - else - Future.map to_response (send_request result) + else Future.map to_response (send_request result) end in - case mk_generic_result stepN text (thm_triggered orelse term_triggered) payload ctxt of + (case mk_generic_result Markup.simp_trace_stepN text + (thm_triggered orelse term_triggered) payload ctxt of NONE => Future.value (SOME ctxt) - | SOME res => mk_promise res + | SOME res => mk_promise res) end fun recurse text term ctxt = @@ -298,11 +296,9 @@ breakpoints = breakpoints} (Context.Proof ctxt) val context' = - case mk_generic_result recurseN text true payload ctxt of - NONE => - put 0 - | SOME res => - (output_result res; put (#1 res)) + (case mk_generic_result Markup.simp_trace_recurseN text true payload ctxt of + NONE => put 0 + | SOME res => (output_result res; put (#1 res))) in Context.the_proof context' end fun indicate_failure ({term, ctxt, thm, rrule, ...}: data) ctxt' = @@ -336,24 +332,21 @@ let val result_id = #1 result - fun to_response "exit" = - false + fun to_response "exit" = false | to_response "redo" = (Option.app output_result - (mk_generic_result ignoreN "Ignore" true empty_payload ctxt'); + (mk_generic_result Markup.simp_trace_ignoreN "Ignore" true empty_payload ctxt'); true) - | to_response _ = - raise Fail "Simplifier_Trace.indicate_failure: invalid message" + | to_response _ = raise Fail "Simplifier_Trace.indicate_failure: invalid message" in if not interactive then (output_result result; Future.value false) - else - Future.map to_response (send_request result) + else Future.map to_response (send_request result) end in - case mk_generic_result hintN "Step failed" true payload ctxt' of + (case mk_generic_result Markup.simp_trace_hintN "Step failed" true payload ctxt' of NONE => Future.value false - | SOME res => mk_promise res + | SOME res => mk_promise res) end fun indicate_success thm ctxt = @@ -362,9 +355,12 @@ {props = [(successN, "true")], pretty = Syntax.pretty_term ctxt (Thm.prop_of thm)} in - Option.app output_result (mk_generic_result hintN "Successfully rewrote" true payload ctxt) + Option.app output_result + (mk_generic_result Markup.simp_trace_hintN "Successfully rewrote" true payload ctxt) end + + (** setup **) fun simp_apply args ctxt cont = @@ -377,21 +373,17 @@ thm = thm, rrule = rrule} in - case Future.join (step data) of - NONE => - NONE + (case Future.join (step data) of + NONE => NONE | SOME ctxt' => let val res = cont ctxt' in - case res of + (case res of NONE => if Future.join (indicate_failure data ctxt') then simp_apply args ctxt cont - else - NONE - | SOME (thm, _) => - (indicate_success thm ctxt'; - res) - end + else NONE + | SOME (thm, _) => (indicate_success thm ctxt'; res)) + end) end val _ = Session.protocol_handler "isabelle.Simplifier_Trace$Handler" @@ -402,7 +394,7 @@ trace_apply = simp_apply}) val _ = - Isabelle_Process.protocol_command "Document.simp_trace_reply" + Isabelle_Process.protocol_command "Simplifier_Trace.reply" (fn [s, r] => let val serial = Markup.parse_int s @@ -415,20 +407,19 @@ handle exn => if Exn.is_interrupt exn then () (*sic!*) else reraise exn end) + + (** attributes **) -val pat_parser = - Args.context -- Scan.lift Args.name_inner_syntax >> uncurry Proof_Context.read_term_schematic - -val mode_parser: string parser = +val mode_parser = Scan.optional (Args.$$$ "mode" |-- Args.$$$ "=" |-- (Args.$$$ "normal" || Args.$$$ "full")) "normal" -val interactive_parser: bool parser = +val interactive_parser = Scan.optional (Args.$$$ "interactive" >> K true) false -val memory_parser: bool parser = +val memory_parser = Scan.optional (Args.$$$ "no_memory" >> K false) true val depth_parser = @@ -440,7 +431,7 @@ val _ = Theory.setup (Attrib.setup @{binding break_term} - ((Scan.repeat1 pat_parser) >> term_breakpoint) + (Scan.repeat1 Args.term_pattern >> term_breakpoint) "declaration of a term breakpoint" #> Attrib.setup @{binding break_thm} (Scan.succeed thm_breakpoint) diff -r 4394bb0b522b -r 439d40b226d1 src/Pure/Tools/simplifier_trace.scala --- a/src/Pure/Tools/simplifier_trace.scala Tue Feb 18 17:56:48 2014 +0100 +++ b/src/Pure/Tools/simplifier_trace.scala Tue Feb 18 21:00:13 2014 +0100 @@ -6,6 +6,7 @@ package isabelle + import scala.actors.Actor._ import scala.annotation.tailrec import scala.collection.immutable.SortedMap @@ -13,8 +14,42 @@ object Simplifier_Trace { + /* trace items from the prover */ - import Markup.Simp_Trace_Item + val TEXT = "text" + val Text = new Properties.String(TEXT) + + val PARENT = "parent" + val Parent = new Properties.Long(PARENT) + + val SUCCESS = "success" + val Success = new Properties.Boolean(SUCCESS) + + val MEMORY = "memory" + val Memory = new Properties.Boolean(MEMORY) + + object Item + { + case class Data( + serial: Long, markup: String, text: String, + parent: Long, props: Properties.T, content: XML.Body) + { + def memory: Boolean = Memory.unapply(props) getOrElse true + } + + def unapply(tree: XML.Tree): Option[(String, Data)] = + tree match { + case XML.Elem(Markup(Markup.RESULT, Markup.Serial(serial)), + List(XML.Elem(Markup(markup, props), content))) + if markup.startsWith("simp_trace_") => // FIXME proper comparison of string constants + (props, props) match { + case (Text(text), Parent(parent)) => + Some((markup, Data(serial, markup, text, parent, props, content))) + case _ => None + } + case _ => None + } + } /* replies to the prover */ @@ -23,7 +58,6 @@ object Answer { - object step { val skip = Answer("skip", "Skip") @@ -44,10 +78,23 @@ val default = exit val all = List(redo, exit) } - } - val all_answers = Answer.step.all ++ Answer.hint_fail.all + val all_answers: List[Answer] = Answer.step.all ::: Answer.hint_fail.all + + object Active + { + def unapply(tree: XML.Tree): Option[(Long, Answer)] = + tree match { + case XML.Elem(Markup(Markup.SIMP_TRACE, props), _) => + (props, props) match { + case (Markup.Serial(serial), Markup.Name(name)) => + all_answers.find(_.name == name).map((serial, _)) + case _ => None + } + case _ => None + } + } /* GUI interaction */ @@ -64,7 +111,7 @@ private object Stop case class Reply(session: Session, serial: Long, answer: Answer) - case class Question(data: Simp_Trace_Item.Data, answers: List[Answer], default_answer: Answer) + case class Question(data: Item.Data, answers: List[Answer], default_answer: Answer) case class Context( last_serial: Long = 0L, @@ -83,13 +130,13 @@ } - case class Trace(entries: List[Simp_Trace_Item.Data]) + case class Trace(entries: List[Item.Data]) case class Index(text: String, content: XML.Body) object Index { - def of_data(data: Simp_Trace_Item.Data): Index = + def of_data(data: Item.Data): Index = Index(data.text, data.content) } @@ -128,7 +175,7 @@ def do_reply(session: Session, serial: Long, answer: Answer) { - session.protocol_command("Document.simp_trace_reply", Properties.Value.Long(serial), answer.name) + session.protocol_command("Simplifier_Trace.reply", Properties.Value.Long(serial), answer.name) } loop { @@ -140,14 +187,12 @@ for ((serial, result) <- results.entries if serial > new_context.last_serial) { result match { - case Simp_Trace_Item(markup, data) => - import Simp_Trace_Item._ - + case Item(markup, data) => memory_children += (data.parent -> (memory_children.getOrElse(data.parent, Set.empty) + serial)) markup match { - case STEP => + case Markup.SIMP_TRACE_STEP => val index = Index.of_data(data) memory.get(index) match { case Some(answer) if data.memory => @@ -156,11 +201,11 @@ new_context += Question(data, Answer.step.all, Answer.step.default) } - case HINT => + case Markup.SIMP_TRACE_HINT => data.props match { - case Markup.Success(false) => + case Success(false) => results.get(data.parent) match { - case Some(Simp_Trace_Item(STEP, _)) => + case Some(Item(Markup.SIMP_TRACE_STEP, _)) => new_context += Question(data, Answer.hint_fail.all, Answer.hint_fail.default) case _ => // unknown, better send a default reply @@ -169,7 +214,7 @@ case _ => } - case IGNORE => + case Markup.SIMP_TRACE_IGNORE => // At this point, we know that the parent of this 'IGNORE' entry is a 'STEP' // entry, and that that 'STEP' entry is about to be replayed. Hence, we need // to selectively purge the replies which have been memorized, going down from @@ -179,7 +224,7 @@ def purge(queue: Vector[Long]): Unit = queue match { case s +: rest => - for (Simp_Trace_Item(STEP, data) <- results.get(s)) + for (Item(Markup.SIMP_TRACE_STEP, data) <- results.get(s)) memory -= Index.of_data(data) val children = memory_children.getOrElse(s, Set.empty) memory_children -= s @@ -208,7 +253,7 @@ // current results. val items = - for { (_, Simp_Trace_Item(_, data)) <- results.entries } + for { (_, Item(_, data)) <- results.entries } yield data reply(Trace(items.toList)) @@ -232,7 +277,7 @@ case Reply(session, serial, answer) => find_question(serial) match { case Some((id, Question(data, _, _))) => - if (data.markup == Markup.Simp_Trace_Item.STEP && data.memory) + if (data.markup == Markup.SIMP_TRACE_STEP && data.memory) { val index = Index.of_data(data) memory += (index -> answer) @@ -256,10 +301,9 @@ class Handler extends Session.Protocol_Handler { - private def cancel( - prover: Session.Prover, msg: Isabelle_Process.Protocol_Output): Boolean = + private def cancel(prover: Session.Prover, msg: Isabelle_Process.Protocol_Output): Boolean = msg.properties match { - case Markup.Cancel_Simp_Trace(serial) => + case Markup.Simp_Trace_Cancel(serial) => manager ! Cancel(serial) true case _ => @@ -272,8 +316,6 @@ manager ! Stop } - val functions = Map( - Markup.CANCEL_SIMP_TRACE -> cancel _) + val functions = Map(Markup.SIMP_TRACE_CANCEL -> cancel _) } - } diff -r 4394bb0b522b -r 439d40b226d1 src/Pure/context.ML --- a/src/Pure/context.ML Tue Feb 18 17:56:48 2014 +0100 +++ b/src/Pure/context.ML Tue Feb 18 21:00:13 2014 +0100 @@ -43,7 +43,6 @@ val this_theory: theory -> string -> theory val eq_thy: theory * theory -> bool val subthy: theory * theory -> bool - val joinable: theory * theory -> bool val merge: theory * theory -> theory val finish_thy: theory -> theory val begin_thy: (theory -> pretty) -> string -> theory list -> theory @@ -246,8 +245,6 @@ fun subthy thys = eq_thy thys orelse proper_subthy thys; -fun joinable (thy1, thy2) = subthy (thy1, thy2) orelse subthy (thy2, thy1); - (* consistent ancestors *) diff -r 4394bb0b522b -r 439d40b226d1 src/Pure/defs.ML --- a/src/Pure/defs.ML Tue Feb 18 17:56:48 2014 +0100 +++ b/src/Pure/defs.ML Tue Feb 18 21:00:13 2014 +0100 @@ -11,7 +11,11 @@ val plain_args: typ list -> bool type T type spec = - {def: string option, description: string, lhs: typ list, rhs: (string * typ list) list} + {def: string option, + description: string, + pos: Position.T, + lhs: typ list, + rhs: (string * typ list) list} val all_specifications_of: T -> (string * spec list) list val specifications_of: T -> string -> spec list val dest: T -> @@ -53,11 +57,15 @@ (* datatype defs *) type spec = - {def: string option, description: string, lhs: args, rhs: (string * args) list}; + {def: string option, + description: string, + pos: Position.T, + lhs: args, + rhs: (string * args) list}; type def = - {specs: spec Inttab.table, (*source specifications*) - restricts: (args * string) list, (*global restrictions imposed by incomplete patterns*) + {specs: spec Inttab.table, (*source specifications*) + restricts: (args * string) list, (*global restrictions imposed by incomplete patterns*) reducts: (args * (string * args) list) list}; (*specifications as reduction system*) fun make_def (specs, restricts, reducts) = @@ -97,11 +105,12 @@ (* specifications *) -fun disjoint_specs c (i, {lhs = Ts, description = a, ...}: spec) = - Inttab.forall (fn (j, {lhs = Us, description = b, ...}: spec) => +fun disjoint_specs c (i, {description = a, pos = pos_a, lhs = Ts, ...}: spec) = + Inttab.forall (fn (j, {description = b, pos = pos_b, lhs = Us, ...}: spec) => i = j orelse disjoint_args (Ts, Us) orelse - error ("Clash of specifications " ^ quote a ^ " and " ^ quote b ^ - " for constant " ^ quote c)); + error ("Clash of specifications for constant " ^ quote c ^ ":\n" ^ + " " ^ quote a ^ Position.here pos_a ^ "\n" ^ + " " ^ quote b ^ Position.here pos_b)); fun join_specs c ({specs = specs1, restricts, reducts}, {specs = specs2, ...}: def) = let @@ -204,12 +213,13 @@ fun define ctxt unchecked def description (c, args) deps (Defs defs) = let + val pos = Position.thread_data (); val restr = if plain_args args orelse (case args of [Type (_, rec_args)] => plain_args rec_args | _ => false) then [] else [(args, description)]; val spec = - (serial (), {def = def, description = description, lhs = args, rhs = deps}); + (serial (), {def = def, description = description, pos = pos, lhs = args, rhs = deps}); val defs' = defs |> update_specs c spec; in Defs (defs' |> (if unchecked then I else dependencies ctxt (c, args) restr deps)) end; diff -r 4394bb0b522b -r 439d40b226d1 src/Pure/goal.ML --- a/src/Pure/goal.ML Tue Feb 18 17:56:48 2014 +0100 +++ b/src/Pure/goal.ML Tue Feb 18 21:00:13 2014 +0100 @@ -187,10 +187,10 @@ val skip = not immediate andalso not schematic andalso future andalso skip_proofs_enabled (); val pos = Position.thread_data (); - fun err msg = cat_error msg - ("The error(s) above occurred for the goal statement:\n" ^ - Syntax.string_of_term ctxt (Logic.list_implies (asms, Logic.mk_conjunction_list props)) ^ - (case Position.here pos of "" => "" | s => "\n" ^ s)); + fun err msg = + cat_error msg + ("The error(s) above occurred for the goal statement" ^ Position.here pos ^ ":\n" ^ + Syntax.string_of_term ctxt (Logic.list_implies (asms, Logic.mk_conjunction_list props))); fun cert_safe t = Thm.cterm_of thy (Envir.beta_norm (Term.no_dummy_patterns t)) handle TERM (msg, _) => err msg | TYPE (msg, _, _) => err msg; diff -r 4394bb0b522b -r 439d40b226d1 src/Pure/more_thm.ML --- a/src/Pure/more_thm.ML Tue Feb 18 17:56:48 2014 +0100 +++ b/src/Pure/more_thm.ML Tue Feb 18 21:00:13 2014 +0100 @@ -37,7 +37,6 @@ val thm_cache: (thm -> 'a) -> thm -> 'a val is_reflexive: thm -> bool val eq_thm: thm * thm -> bool - val eq_thm_thy: thm * thm -> bool val eq_thm_prop: thm * thm -> bool val eq_thm_strict: thm * thm -> bool val equiv_thm: thm * thm -> bool @@ -191,17 +190,17 @@ fun is_reflexive th = op aconv (Logic.dest_equals (Thm.prop_of th)) handle TERM _ => false; -fun eq_thm ths = - Context.joinable (pairself Thm.theory_of_thm ths) andalso - is_equal (thm_ord ths); +val eq_thm = is_equal o thm_ord; -val eq_thm_thy = Theory.eq_thy o pairself Thm.theory_of_thm; val eq_thm_prop = op aconv o pairself Thm.full_prop_of; fun eq_thm_strict ths = - eq_thm_thy ths andalso eq_thm ths andalso - let val (rep1, rep2) = pairself Thm.rep_thm ths - in #maxidx rep1 = #maxidx rep2 andalso #tags rep1 = #tags rep2 end; + eq_thm ths andalso + let val (rep1, rep2) = pairself Thm.rep_thm ths in + Theory.eq_thy (#thy rep1, #thy rep2) andalso + #maxidx rep1 = #maxidx rep2 andalso + #tags rep1 = #tags rep2 + end; (* pattern equivalence *) diff -r 4394bb0b522b -r 439d40b226d1 src/Tools/jEdit/src/Isabelle.props --- a/src/Tools/jEdit/src/Isabelle.props Tue Feb 18 17:56:48 2014 +0100 +++ b/src/Tools/jEdit/src/Isabelle.props Tue Feb 18 21:00:13 2014 +0100 @@ -27,48 +27,48 @@ options.isabelle-rendering.label=Rendering options.isabelle-rendering.code=new isabelle.jedit.Isabelle_Options2(); -#menu actions +#menu actions and dockables plugin.isabelle.jedit.Plugin.menu.label=Isabelle plugin.isabelle.jedit.Plugin.menu= \ - isabelle.documentation-panel \ - isabelle.find-panel \ - isabelle.monitor-panel \ - isabelle.output-panel \ - isabelle.protocol-panel \ - isabelle.raw-output-panel \ - isabelle.sledgehammer-panel \ - isabelle.simp-trace-panel \ - isabelle.symbols-panel \ - isabelle.syslog-panel \ - isabelle.theories-panel \ - isabelle.timing-panel -isabelle.documentation-panel.label=Documentation panel -isabelle.find-panel.label=Find panel -isabelle.monitor-panel.label=Monitor panel -isabelle.output-panel.label=Output panel -isabelle.protocol-panel.label=Protocol panel -isabelle.raw-output-panel.label=Raw Output panel -isabelle.simp-trace-panel.label=Simplifier trace panel -isabelle.sledgehammer-panel.label=Sledgehammer panel -isabelle.symbols-panel.label=Symbols panel -isabelle.syslog-panel.label=Syslog panel -isabelle.theories-panel.label=Theories panel -isabelle.timing-panel.label=Timing panel - -#dockables + isabelle-documentation \ + isabelle-find \ + isabelle-monitor \ + isabelle-output \ + isabelle-protocol \ + isabelle-raw-output \ + isabelle-simplifier-trace \ + isabelle-sledgehammer \ + isabelle-symbols \ + isabelle-syslog \ + isabelle-theories \ + isabelle-timing +isabelle-documentation.label=Documentation panel +isabelle-documentation.title=Documentation +isabelle-find.label=Find panel isabelle-find.title=Find +isabelle-graphview.label=Graphview panel isabelle-graphview.title=Graphview +isabelle-info.label=Info panel isabelle-info.title=Info +isabelle-monitor.label=Monitor panel isabelle-monitor.title=Monitor +isabelle-output.label=Output panel isabelle-output.title=Output -isabelle-simp-trace.title=Simplifier trace +isabelle-protocol.label=Protocol panel isabelle-protocol.title=Protocol +isabelle-raw-output.label=Raw Output panel isabelle-raw-output.title=Raw Output -isabelle-documentation.title=Documentation +isabelle-simplifier-trace.label=Simplifier Trace panel +isabelle-simplifier-trace.title=Simplifier Trace +isabelle-sledgehammer.label=Sledgehammer panel isabelle-sledgehammer.title=Sledgehammer +isabelle-symbols.label=Symbols panel isabelle-symbols.title=Symbols +isabelle-syslog.label=Syslog panel isabelle-syslog.title=Syslog +isabelle-theories.label=Theories panel isabelle-theories.title=Theories +isabelle-timing.label=Timing panel isabelle-timing.title=Timing #SideKick diff -r 4394bb0b522b -r 439d40b226d1 src/Tools/jEdit/src/actions.xml --- a/src/Tools/jEdit/src/actions.xml Tue Feb 18 17:56:48 2014 +0100 +++ b/src/Tools/jEdit/src/actions.xml Tue Feb 18 21:00:13 2014 +0100 @@ -2,66 +2,6 @@ - - - wm.addDockableWindow("isabelle-theories"); - - - - - wm.addDockableWindow("isabelle-timing"); - - - - - wm.addDockableWindow("isabelle-syslog"); - - - - - wm.addDockableWindow("isabelle-documentation"); - - - - - wm.addDockableWindow("isabelle-find"); - - - - - wm.addDockableWindow("isabelle-sledgehammer"); - - - - - wm.addDockableWindow("isabelle-output"); - - - - - wm.addDockableWindow("isabelle-raw-output"); - - - - - wm.addDockableWindow("isabelle-simp-trace"); - - - - - wm.addDockableWindow("isabelle-protocol"); - - - - - wm.addDockableWindow("isabelle-monitor"); - - - - - wm.addDockableWindow("isabelle-symbols"); - - isabelle.jedit.Isabelle.set_continuous_checking(); diff -r 4394bb0b522b -r 439d40b226d1 src/Tools/jEdit/src/active.scala --- a/src/Tools/jEdit/src/active.scala Tue Feb 18 17:56:48 2014 +0100 +++ b/src/Tools/jEdit/src/active.scala Tue Feb 18 21:00:13 2014 +0100 @@ -61,7 +61,7 @@ else text_area.setSelectedText(text) } - case Markup.Simp_Trace(serial, answer) => + case Simplifier_Trace.Active(serial, answer) => Simplifier_Trace.send_reply(PIDE.session, serial, answer) case Protocol.Dialog(id, serial, result) => diff -r 4394bb0b522b -r 439d40b226d1 src/Tools/jEdit/src/dockables.xml --- a/src/Tools/jEdit/src/dockables.xml Tue Feb 18 17:56:48 2014 +0100 +++ b/src/Tools/jEdit/src/dockables.xml Tue Feb 18 21:00:13 2014 +0100 @@ -2,46 +2,46 @@ - - new isabelle.jedit.Theories_Dockable(view, position); - - - new isabelle.jedit.Timing_Dockable(view, position); - - - new isabelle.jedit.Syslog_Dockable(view, position); - new isabelle.jedit.Documentation_Dockable(view, position); - - new isabelle.jedit.Output_Dockable(view, position); - new isabelle.jedit.Find_Dockable(view, position); - - new isabelle.jedit.Sledgehammer_Dockable(view, position); - new isabelle.jedit.Info_Dockable(view, position); new isabelle.jedit.Graphview_Dockable(view, position); - - new isabelle.jedit.Raw_Output_Dockable(view, position); + + new isabelle.jedit.Monitor_Dockable(view, position); + + + new isabelle.jedit.Output_Dockable(view, position); new isabelle.jedit.Protocol_Dockable(view, position); - - new isabelle.jedit.Monitor_Dockable(view, position); + + new isabelle.jedit.Raw_Output_Dockable(view, position); + + + new isabelle.jedit.Simplifier_Trace_Dockable(view, position); + + + new isabelle.jedit.Sledgehammer_Dockable(view, position); new isabelle.jedit.Symbols_Dockable(view, position); - - new isabelle.jedit.Simplifier_Trace_Dockable(view, position); + + new isabelle.jedit.Syslog_Dockable(view, position); + + + new isabelle.jedit.Theories_Dockable(view, position); + + + new isabelle.jedit.Timing_Dockable(view, position); diff -r 4394bb0b522b -r 439d40b226d1 src/Tools/jEdit/src/isabelle.scala --- a/src/Tools/jEdit/src/isabelle.scala Tue Feb 18 17:56:48 2014 +0100 +++ b/src/Tools/jEdit/src/isabelle.scala Tue Feb 18 21:00:13 2014 +0100 @@ -58,45 +58,75 @@ private def wm(view: View): DockableWindowManager = view.getDockableWindowManager - def docked_theories(view: View): Option[Theories_Dockable] = - wm(view).getDockableWindow("isabelle-theories") match { - case dockable: Theories_Dockable => Some(dockable) + def documentation_dockable(view: View): Option[Documentation_Dockable] = + wm(view).getDockableWindow("isabelle-documentation") match { + case dockable: Documentation_Dockable => Some(dockable) case _ => None } - def docked_timing(view: View): Option[Timing_Dockable] = - wm(view).getDockableWindow("isabelle-timing") match { - case dockable: Timing_Dockable => Some(dockable) + def find_dockable(view: View): Option[Find_Dockable] = + wm(view).getDockableWindow("isabelle-find") match { + case dockable: Find_Dockable => Some(dockable) case _ => None } - def docked_output(view: View): Option[Output_Dockable] = + def monitor_dockable(view: View): Option[Monitor_Dockable] = + wm(view).getDockableWindow("isabelle-monitor") match { + case dockable: Monitor_Dockable => Some(dockable) + case _ => None + } + + def output_dockable(view: View): Option[Output_Dockable] = wm(view).getDockableWindow("isabelle-output") match { case dockable: Output_Dockable => Some(dockable) case _ => None } - def docked_raw_output(view: View): Option[Raw_Output_Dockable] = + def protocol_dockable(view: View): Option[Protocol_Dockable] = + wm(view).getDockableWindow("isabelle-protocol") match { + case dockable: Protocol_Dockable => Some(dockable) + case _ => None + } + + def raw_output_dockable(view: View): Option[Raw_Output_Dockable] = wm(view).getDockableWindow("isabelle-raw-output") match { case dockable: Raw_Output_Dockable => Some(dockable) case _ => None } - def docked_simplifier_trace(view: View): Option[Simplifier_Trace_Dockable] = - wm(view).getDockableWindow("isabelle-simp-trace") match { + def simplifier_trace_dockable(view: View): Option[Simplifier_Trace_Dockable] = + wm(view).getDockableWindow("isabelle-simplifier-trace") match { case dockable: Simplifier_Trace_Dockable => Some(dockable) case _ => None } - def docked_protocol(view: View): Option[Protocol_Dockable] = - wm(view).getDockableWindow("isabelle-protocol") match { - case dockable: Protocol_Dockable => Some(dockable) + def sledgehammer_dockable(view: View): Option[Sledgehammer_Dockable] = + wm(view).getDockableWindow("isabelle-sledgehammer") match { + case dockable: Sledgehammer_Dockable => Some(dockable) + case _ => None + } + + def symbols_dockable(view: View): Option[Symbols_Dockable] = + wm(view).getDockableWindow("isabelle-symbols") match { + case dockable: Symbols_Dockable => Some(dockable) case _ => None } - def docked_monitor(view: View): Option[Monitor_Dockable] = - wm(view).getDockableWindow("isabelle-monitor") match { - case dockable: Monitor_Dockable => Some(dockable) + def syslog_dockable(view: View): Option[Syslog_Dockable] = + wm(view).getDockableWindow("isabelle-syslog") match { + case dockable: Syslog_Dockable => Some(dockable) + case _ => None + } + + def theories_dockable(view: View): Option[Theories_Dockable] = + wm(view).getDockableWindow("isabelle-theories") match { + case dockable: Theories_Dockable => Some(dockable) + case _ => None + } + + def timing_dockable(view: View): Option[Timing_Dockable] = + wm(view).getDockableWindow("isabelle-timing") match { + case dockable: Timing_Dockable => Some(dockable) case _ => None } diff -r 4394bb0b522b -r 439d40b226d1 src/Tools/jEdit/src/jEdit.props --- a/src/Tools/jEdit/src/jEdit.props Tue Feb 18 17:56:48 2014 +0100 +++ b/src/Tools/jEdit/src/jEdit.props Tue Feb 18 21:00:13 2014 +0100 @@ -188,8 +188,8 @@ isabelle-output.dock-position=bottom isabelle-output.height=174 isabelle-output.width=412 +isabelle-simplifier-trace.dock-position=bottom isabelle-sledgehammer.dock-position=bottom -isabelle-simp-trace.dock-position=bottom isabelle-symbols.dock-position=bottom isabelle-theories.dock-position=right isabelle.complete.label=Complete Isabelle text diff -r 4394bb0b522b -r 439d40b226d1 src/Tools/jEdit/src/jedit_lib.scala --- a/src/Tools/jEdit/src/jedit_lib.scala Tue Feb 18 17:56:48 2014 +0100 +++ b/src/Tools/jEdit/src/jedit_lib.scala Tue Feb 18 21:00:13 2014 +0100 @@ -222,9 +222,10 @@ try { val p = text_area.offsetToXY(range.start) val (q, r) = - if (stop >= end) (text_area.offsetToXY(end), char_width * (stop - end)) - else if (stop > 0 && buffer.getText(stop - 1, 1) == "\n") + if (try_get_text(buffer, Text.Range(stop - 1, stop)) == Some("\n")) (text_area.offsetToXY(stop - 1), char_width) + else if (stop >= end) + (text_area.offsetToXY(end), char_width * (stop - end)) else (text_area.offsetToXY(stop), 0) (p, q, r) } diff -r 4394bb0b522b -r 439d40b226d1 src/Tools/jEdit/src/rendering.scala --- a/src/Tools/jEdit/src/rendering.scala Tue Feb 18 17:56:48 2014 +0100 +++ b/src/Tools/jEdit/src/rendering.scala Tue Feb 18 21:00:13 2014 +0100 @@ -241,10 +241,10 @@ /* markup selectors */ private val highlight_include = - Set(Markup.SORT, Markup.TYP, Markup.TERM, Markup.PROP, Markup.ML_TYPING, Markup.TOKEN_RANGE, - Markup.ENTITY, Markup.PATH, Markup.URL, Markup.SORTING, Markup.TYPING, Markup.FREE, - Markup.SKOLEM, Markup.BOUND, Markup.VAR, Markup.TFREE, Markup.TVAR, Markup.ML_SOURCE, - Markup.DOCUMENT_SOURCE) + Set(Markup.LANGUAGE, Markup.ML_TYPING, Markup.TOKEN_RANGE, + Markup.ENTITY, Markup.PATH, Markup.URL, Markup.SORTING, + Markup.TYPING, Markup.FREE, Markup.SKOLEM, Markup.BOUND, + Markup.VAR, Markup.TFREE, Markup.TVAR) def highlight(range: Text.Range): Option[Text.Info[Color]] = { @@ -258,7 +258,21 @@ } - private val hyperlink_include = Set(Markup.ENTITY, Markup.PATH, Markup.URL) + private val hyperlink_include = Set(Markup.ENTITY, Markup.PATH, Markup.POSITION, Markup.URL) + + private def hyperlink_file(line: Int, name: String): Option[PIDE.editor.Hyperlink] = + if (Path.is_ok(name)) + Isabelle_System.source_file(Path.explode(name)).map(path => + PIDE.editor.hyperlink_file(Isabelle_System.platform_path(path), line)) + else None + + private def hyperlink_command(id: Document_ID.Generic, offset: Text.Offset) + : Option[PIDE.editor.Hyperlink] = + snapshot.state.find_command(snapshot.version, id) match { + case Some((node, command)) => + PIDE.editor.hyperlink_command(snapshot, command, offset) + case None => None + } def hyperlink(range: Text.Range): Option[Text.Info[PIDE.editor.Hyperlink]] = { @@ -281,26 +295,22 @@ case (Markup.KIND, Markup.ML_STRUCT) => true case _ => false }) => - props match { - case Position.Def_Line_File(line, name) if Path.is_ok(name) => - Isabelle_System.source_file(Path.explode(name)) match { - case Some(path) => - val jedit_file = Isabelle_System.platform_path(path) - val link = PIDE.editor.hyperlink_file(jedit_file, line) - Some(Text.Info(snapshot.convert(info_range), link) :: links) - case None => None - } + val opt_link = + props match { + case Position.Def_Line_File(line, name) => hyperlink_file(line, name) + case Position.Def_Id_Offset(id, offset) => hyperlink_command(id, offset) + case _ => None + } + opt_link.map(link => (Text.Info(snapshot.convert(info_range), link) :: links)) - case Position.Def_Id_Offset(id, offset) => - snapshot.state.find_command(snapshot.version, id) match { - case Some((node, command)) => - PIDE.editor.hyperlink_command(snapshot, command, offset) - .map(link => (Text.Info(snapshot.convert(info_range), link) :: links)) - case None => None - } - - case _ => None - } + case (links, Text.Info(info_range, XML.Elem(Markup(Markup.POSITION, props), _))) => + val opt_link = + props match { + case Position.Line_File(line, name) => hyperlink_file(line, name) + case Position.Id_Offset(id, offset) => hyperlink_command(id, offset) + case _ => None + } + opt_link.map(link => (Text.Info(snapshot.convert(info_range), link) :: links)) case _ => None }) match { case Text.Info(_, info :: _) :: _ => Some(info) case _ => None } @@ -365,23 +375,18 @@ private val tooltips: Map[String, String] = Map( - Markup.SORT -> "sort", - Markup.TYP -> "type", - Markup.TERM -> "term", - Markup.PROP -> "proposition", Markup.TOKEN_RANGE -> "inner syntax token", Markup.FREE -> "free variable", Markup.SKOLEM -> "skolem variable", Markup.BOUND -> "bound variable", Markup.VAR -> "schematic variable", Markup.TFREE -> "free type variable", - Markup.TVAR -> "schematic type variable", - Markup.ML_SOURCE -> "ML source", - Markup.DOCUMENT_SOURCE -> "document source") + Markup.TVAR -> "schematic type variable") private val tooltip_elements = - Set(Markup.TIMING, Markup.ENTITY, Markup.SORTING, Markup.TYPING, - Markup.ML_TYPING, Markup.PATH, Markup.URL) ++ tooltips.keys + Set(Markup.LANGUAGE, Markup.TIMING, Markup.ENTITY, Markup.SORTING, + Markup.TYPING, Markup.ML_TYPING, Markup.PATH, Markup.URL) ++ + tooltips.keys private def pretty_typing(kind: String, body: XML.Body): XML.Tree = Pretty.block(XML.Text(kind) :: Pretty.Break(1) :: body) @@ -424,6 +429,8 @@ Some(add(prev, r, (true, pretty_typing("::", body)))) case (prev, Text.Info(r, XML.Elem(Markup(Markup.ML_TYPING, _), body))) => Some(add(prev, r, (false, pretty_typing("ML:", body)))) + case (prev, Text.Info(r, XML.Elem(Markup.Language(name), _))) => + Some(add(prev, r, (true, XML.Text("language: " + name)))) case (prev, Text.Info(r, XML.Elem(Markup(name, _), _))) => if (tooltips.isDefinedAt(name)) Some(add(prev, r, (true, XML.Text(tooltips(name))))) diff -r 4394bb0b522b -r 439d40b226d1 src/Tools/jEdit/src/simplifier_trace_dockable.scala --- a/src/Tools/jEdit/src/simplifier_trace_dockable.scala Tue Feb 18 17:56:48 2014 +0100 +++ b/src/Tools/jEdit/src/simplifier_trace_dockable.scala Tue Feb 18 21:00:13 2014 +0100 @@ -10,7 +10,6 @@ import isabelle._ import scala.actors.Actor._ - import scala.swing.{Button, CheckBox, Orientation, Separator} import scala.swing.event.ButtonClicked @@ -19,6 +18,7 @@ import org.gjt.sp.jedit.View + class Simplifier_Trace_Dockable(view: View, position: String) extends Dockable(view, position) { Swing_Thread.require() diff -r 4394bb0b522b -r 439d40b226d1 src/Tools/jEdit/src/simplifier_trace_window.scala --- a/src/Tools/jEdit/src/simplifier_trace_window.scala Tue Feb 18 17:56:48 2014 +0100 +++ b/src/Tools/jEdit/src/simplifier_trace_window.scala Tue Feb 18 21:00:13 2014 +0100 @@ -10,12 +10,9 @@ import isabelle._ import scala.annotation.tailrec - import scala.collection.immutable.SortedMap - import scala.swing.{BorderPanel, CheckBox, Component, Dimension, Frame, Label, TextField} import scala.swing.event.{Key, KeyPressed} - import scala.util.matching.Regex import java.awt.BorderLayout @@ -25,17 +22,15 @@ import org.gjt.sp.jedit.View + private object Simplifier_Trace_Window { - - import Markup.Simp_Trace_Item - sealed trait Trace_Tree { var children: SortedMap[Long, Elem_Tree] = SortedMap.empty val serial: Long val parent: Option[Trace_Tree] - var hints: List[Simp_Trace_Item.Data] + var hints: List[Simplifier_Trace.Item.Data] def set_interesting(): Unit } @@ -43,17 +38,19 @@ { val parent = None val hints = Nil - def hints_=(xs: List[Simp_Trace_Item.Data]) = throw new IllegalStateException("Root_Tree.hints") + def hints_=(xs: List[Simplifier_Trace.Item.Data]) = + throw new IllegalStateException("Root_Tree.hints") def set_interesting() = () def format(regex: Option[Regex]): XML.Body = Pretty.separate(children.values.map(_.format(regex)._2)(collection.breakOut)) } - final class Elem_Tree(data: Simp_Trace_Item.Data, val parent: Option[Trace_Tree]) extends Trace_Tree + final class Elem_Tree(data: Simplifier_Trace.Item.Data, val parent: Option[Trace_Tree]) + extends Trace_Tree { val serial = data.serial - var hints = List.empty[Simp_Trace_Item.Data] + var hints = List.empty[Simplifier_Trace.Item.Data] var interesting: Boolean = false def set_interesting(): Unit = @@ -76,7 +73,7 @@ Some(XML.Elem(Markup(Markup.ITEM, Nil), List(res))) } - def format_hint(data: Simp_Trace_Item.Data): XML.Tree = + def format_hint(data: Simplifier_Trace.Item.Data): XML.Tree = Pretty.block(Pretty.separate( XML.Text(data.text) :: data.content @@ -111,19 +108,19 @@ } @tailrec - def walk_trace(rest: List[Simp_Trace_Item.Data], lookup: Map[Long, Trace_Tree]): Unit = + def walk_trace(rest: List[Simplifier_Trace.Item.Data], lookup: Map[Long, Trace_Tree]): Unit = rest match { case Nil => () case head :: tail => lookup.get(head.parent) match { case Some(parent) => - if (head.markup == Simp_Trace_Item.HINT) + if (head.markup == Markup.SIMP_TRACE_HINT) { parent.hints ::= head walk_trace(tail, lookup) } - else if (head.markup == Simp_Trace_Item.IGNORE) + else if (head.markup == Markup.SIMP_TRACE_IGNORE) { parent.parent match { case None => @@ -137,7 +134,7 @@ { val entry = new Elem_Tree(head, Some(parent)) parent.children += ((head.serial, entry)) - if (head.markup == Simp_Trace_Item.STEP || head.markup == Simp_Trace_Item.LOG) + if (head.markup == Markup.SIMP_TRACE_STEP || head.markup == Markup.SIMP_TRACE_LOG) entry.set_interesting() walk_trace(tail, lookup + (head.serial -> entry)) } @@ -149,11 +146,10 @@ } -class Simplifier_Trace_Window(view: View, snapshot: Document.Snapshot, trace: Simplifier_Trace.Trace) extends Frame + +class Simplifier_Trace_Window( + view: View, snapshot: Document.Snapshot, trace: Simplifier_Trace.Trace) extends Frame { - - import Simplifier_Trace_Window._ - Swing_Thread.require() val area = new Pretty_Text_Area(view) @@ -165,11 +161,11 @@ private val tree = trace.entries.headOption match { case Some(first) => - val tree = new Root_Tree(first.parent) - walk_trace(trace.entries, Map(first.parent -> tree)) + val tree = new Simplifier_Trace_Window.Root_Tree(first.parent) + Simplifier_Trace_Window.walk_trace(trace.entries, Map(first.parent -> tree)) tree case None => - new Root_Tree(0) + new Simplifier_Trace_Window.Root_Tree(0) } do_update(None)