--- 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 ***
--- 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 @@
\<newline> code: 0x0023ce
\<open> code: 0x002039 group: punctuation font: IsabelleText abbrev: <<
\<close> code: 0x00203a group: punctuation font: IsabelleText abbrev: >>
+\<here> 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
--- 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
Binary file lib/fonts/IsabelleText.ttf has changed
--- 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
Binary file lib/fonts/IsabelleTextBold.ttf has changed
--- 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
--- 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,
--- 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 =
--- 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 =
--- 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 "\\<here>" else "");
in
if null props then ""
else (if s = "" then "" else " ") ^ Markup.markup (Markup.properties props Markup.position) s
--- 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))
--- 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
}
}
--- 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 []
--- 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) =>
--- 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 **)
--- 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
- }
-
- }
-
}
--- 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
}
--- 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 =
{
--- 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;
--- 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)
}
}
--- 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);
--- 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)
--- 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 _)
}
-
}
--- 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 *)
--- 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;
--- 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;
--- 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 *)
--- 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
--- 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 @@
<!DOCTYPE ACTIONS SYSTEM "actions.dtd">
<ACTIONS>
- <ACTION NAME="isabelle.theories-panel">
- <CODE>
- wm.addDockableWindow("isabelle-theories");
- </CODE>
- </ACTION>
- <ACTION NAME="isabelle.timing-panel">
- <CODE>
- wm.addDockableWindow("isabelle-timing");
- </CODE>
- </ACTION>
- <ACTION NAME="isabelle.syslog-panel">
- <CODE>
- wm.addDockableWindow("isabelle-syslog");
- </CODE>
- </ACTION>
- <ACTION NAME="isabelle.documentation-panel">
- <CODE>
- wm.addDockableWindow("isabelle-documentation");
- </CODE>
- </ACTION>
- <ACTION NAME="isabelle.find-panel">
- <CODE>
- wm.addDockableWindow("isabelle-find");
- </CODE>
- </ACTION>
- <ACTION NAME="isabelle.sledgehammer-panel">
- <CODE>
- wm.addDockableWindow("isabelle-sledgehammer");
- </CODE>
- </ACTION>
- <ACTION NAME="isabelle.output-panel">
- <CODE>
- wm.addDockableWindow("isabelle-output");
- </CODE>
- </ACTION>
- <ACTION NAME="isabelle.raw-output-panel">
- <CODE>
- wm.addDockableWindow("isabelle-raw-output");
- </CODE>
- </ACTION>
- <ACTION NAME="isabelle.simp-trace-panel">
- <CODE>
- wm.addDockableWindow("isabelle-simp-trace");
- </CODE>
- </ACTION>
- <ACTION NAME="isabelle.protocol-panel">
- <CODE>
- wm.addDockableWindow("isabelle-protocol");
- </CODE>
- </ACTION>
- <ACTION NAME="isabelle.monitor-panel">
- <CODE>
- wm.addDockableWindow("isabelle-monitor");
- </CODE>
- </ACTION>
- <ACTION NAME="isabelle.symbols-panel">
- <CODE>
- wm.addDockableWindow("isabelle-symbols");
- </CODE>
- </ACTION>
<ACTION NAME="isabelle.set-continuous-checking">
<CODE>
isabelle.jedit.Isabelle.set_continuous_checking();
--- 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) =>
--- 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 @@
<!DOCTYPE DOCKABLES SYSTEM "dockables.dtd">
<DOCKABLES>
- <DOCKABLE NAME="isabelle-theories" MOVABLE="TRUE">
- new isabelle.jedit.Theories_Dockable(view, position);
- </DOCKABLE>
- <DOCKABLE NAME="isabelle-timing" MOVABLE="TRUE">
- new isabelle.jedit.Timing_Dockable(view, position);
- </DOCKABLE>
- <DOCKABLE NAME="isabelle-syslog" MOVABLE="TRUE">
- new isabelle.jedit.Syslog_Dockable(view, position);
- </DOCKABLE>
<DOCKABLE NAME="isabelle-documentation" MOVABLE="TRUE">
new isabelle.jedit.Documentation_Dockable(view, position);
</DOCKABLE>
- <DOCKABLE NAME="isabelle-output" MOVABLE="TRUE">
- new isabelle.jedit.Output_Dockable(view, position);
- </DOCKABLE>
<DOCKABLE NAME="isabelle-find" MOVABLE="TRUE">
new isabelle.jedit.Find_Dockable(view, position);
</DOCKABLE>
- <DOCKABLE NAME="isabelle-sledgehammer" MOVABLE="TRUE">
- new isabelle.jedit.Sledgehammer_Dockable(view, position);
- </DOCKABLE>
<DOCKABLE NAME="isabelle-info" MOVABLE="TRUE">
new isabelle.jedit.Info_Dockable(view, position);
</DOCKABLE>
<DOCKABLE NAME="isabelle-graphview" MOVABLE="TRUE">
new isabelle.jedit.Graphview_Dockable(view, position);
</DOCKABLE>
- <DOCKABLE NAME="isabelle-raw-output" MOVABLE="TRUE">
- new isabelle.jedit.Raw_Output_Dockable(view, position);
+ <DOCKABLE NAME="isabelle-monitor" MOVABLE="TRUE">
+ new isabelle.jedit.Monitor_Dockable(view, position);
+ </DOCKABLE>
+ <DOCKABLE NAME="isabelle-output" MOVABLE="TRUE">
+ new isabelle.jedit.Output_Dockable(view, position);
</DOCKABLE>
<DOCKABLE NAME="isabelle-protocol" MOVABLE="TRUE">
new isabelle.jedit.Protocol_Dockable(view, position);
</DOCKABLE>
- <DOCKABLE NAME="isabelle-monitor" MOVABLE="TRUE">
- new isabelle.jedit.Monitor_Dockable(view, position);
+ <DOCKABLE NAME="isabelle-raw-output" MOVABLE="TRUE">
+ new isabelle.jedit.Raw_Output_Dockable(view, position);
+ </DOCKABLE>
+ <DOCKABLE NAME="isabelle-simplifier-trace" MOVABLE="TRUE">
+ new isabelle.jedit.Simplifier_Trace_Dockable(view, position);
+ </DOCKABLE>
+ <DOCKABLE NAME="isabelle-sledgehammer" MOVABLE="TRUE">
+ new isabelle.jedit.Sledgehammer_Dockable(view, position);
</DOCKABLE>
<DOCKABLE NAME="isabelle-symbols" MOVABLE="TRUE">
new isabelle.jedit.Symbols_Dockable(view, position);
</DOCKABLE>
- <DOCKABLE NAME="isabelle-simp-trace" MOVABLE="TRUE">
- new isabelle.jedit.Simplifier_Trace_Dockable(view, position);
+ <DOCKABLE NAME="isabelle-syslog" MOVABLE="TRUE">
+ new isabelle.jedit.Syslog_Dockable(view, position);
+ </DOCKABLE>
+ <DOCKABLE NAME="isabelle-theories" MOVABLE="TRUE">
+ new isabelle.jedit.Theories_Dockable(view, position);
+ </DOCKABLE>
+ <DOCKABLE NAME="isabelle-timing" MOVABLE="TRUE">
+ new isabelle.jedit.Timing_Dockable(view, position);
</DOCKABLE>
</DOCKABLES>
--- 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
}
--- 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
--- 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)
}
--- 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)))))
--- 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()
--- 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)