Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
--- a/src/Doc/antiquote_setup.ML Sun Nov 25 18:50:13 2012 +0100
+++ b/src/Doc/antiquote_setup.ML Sun Nov 25 19:49:24 2012 +0100
@@ -210,7 +210,7 @@
entity_antiqs no_check "isatt" "executable" #>
entity_antiqs (K check_tool) "isatool" "tool" #>
entity_antiqs (thy_check ML_Context.intern_antiq ML_Context.defined_antiq)
- "" Isabelle_Markup.ML_antiquotationN;
+ "" Markup.ML_antiquotationN;
end;
--- a/src/HOL/Tools/Nitpick/nitpick.ML Sun Nov 25 18:50:13 2012 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick.ML Sun Nov 25 19:49:24 2012 +0100
@@ -245,7 +245,7 @@
if mode = Auto_Try then
Unsynchronized.change state_ref o Proof.goal_message o K
o Pretty.chunks o cons (Pretty.str "") o single
- o Pretty.mark Isabelle_Markup.intensify
+ o Pretty.mark Markup.intensify
else
print o Pretty.string_of
val pprint_a = pprint Output.urgent_message
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Sun Nov 25 18:50:13 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Sun Nov 25 19:49:24 2012 +0100
@@ -137,7 +137,7 @@
|> outcome_code = someN
? Proof.goal_message (fn () =>
[Pretty.str "",
- Pretty.mark Isabelle_Markup.intensify (Pretty.str (message ()))]
+ Pretty.mark Markup.intensify (Pretty.str (message ()))]
|> Pretty.chunks))
end
else if blocking then
--- a/src/HOL/Tools/try0.ML Sun Nov 25 18:50:13 2012 +0100
+++ b/src/HOL/Tools/try0.ML Sun Nov 25 19:49:24 2012 +0100
@@ -146,7 +146,7 @@
(true, (s, st |> (if mode = Auto_Try then
Proof.goal_message
(fn () => Pretty.chunks [Pretty.str "",
- Pretty.markup Isabelle_Markup.intensify
+ Pretty.markup Markup.intensify
[Pretty.str message]])
else
tap (fn _ => Output.urgent_message message))))
--- a/src/Pure/General/antiquote.ML Sun Nov 25 18:50:13 2012 +0100
+++ b/src/Pure/General/antiquote.ML Sun Nov 25 19:49:24 2012 +0100
@@ -41,9 +41,9 @@
fun reports_of text =
maps
(fn Text x => text x
- | Antiq (_, (pos, _)) => [((pos, Isabelle_Markup.antiq), "")]
- | Open pos => [((pos, Isabelle_Markup.antiq), "")]
- | Close pos => [((pos, Isabelle_Markup.antiq), "")]);
+ | Antiq (_, (pos, _)) => [((pos, Markup.antiq), "")]
+ | Open pos => [((pos, Markup.antiq), "")]
+ | Close pos => [((pos, Markup.antiq), "")]);
(* check_nesting *)
--- a/src/Pure/General/binding.ML Sun Nov 25 18:50:13 2012 +0100
+++ b/src/Pure/General/binding.ML Sun Nov 25 19:49:24 2012 +0100
@@ -124,7 +124,7 @@
fun pretty (Binding {prefix, qualifier, name, pos, ...}) =
if name = "" then Pretty.str "\"\""
else
- Pretty.markup (Position.markup pos Isabelle_Markup.binding)
+ Pretty.markup (Position.markup pos Markup.binding)
[Pretty.str (Long_Name.implode (map #1 (prefix @ qualifier) @ [name]))]
|> Pretty.quote;
--- a/src/Pure/General/graph_display.ML Sun Nov 25 18:50:13 2012 +0100
+++ b/src/Pure/General/graph_display.ML Sun Nov 25 19:49:24 2012 +0100
@@ -58,7 +58,7 @@
fun display_graph graph =
if print_mode_active graphview_reportN then
(Output.report
- (YXML.string_of (XML.Elem ((Isabelle_Markup.graphviewN, []), encode_graphview graph)));
+ (YXML.string_of (XML.Elem ((Markup.graphviewN, []), encode_graphview graph)));
writeln "(see graphview)")
else
let
--- a/src/Pure/General/name_space.ML Sun Nov 25 18:50:13 2012 +0100
+++ b/src/Pure/General/name_space.ML Sun Nov 25 19:49:24 2012 +0100
@@ -88,7 +88,7 @@
id: serial};
fun entry_markup def kind (name, {pos, id, ...}: entry) =
- Markup.properties (Position.entity_properties_of def id pos) (Isabelle_Markup.entity kind name);
+ Markup.properties (Position.entity_properties_of def id pos) (Markup.entity kind name);
fun print_entry_ref kind (name, entry) =
quote (Markup.markup (entry_markup false kind (name, entry)) name);
@@ -133,7 +133,7 @@
fun markup (Name_Space {kind, entries, ...}) name =
(case Symtab.lookup entries name of
- NONE => Isabelle_Markup.intensify
+ NONE => Markup.intensify
| SOME (_, entry) => entry_markup false kind (name, entry));
fun is_concealed space name = #concealed (the_entry space name);
--- a/src/Pure/General/path.ML Sun Nov 25 18:50:13 2012 +0100
+++ b/src/Pure/General/path.ML Sun Nov 25 19:49:24 2012 +0100
@@ -155,7 +155,7 @@
fun pretty path =
let val s = implode_path path
- in Pretty.mark (Isabelle_Markup.path s) (Pretty.str (quote s)) end;
+ in Pretty.mark (Markup.path s) (Pretty.str (quote s)) end;
val print = Pretty.str_of o pretty;
--- a/src/Pure/General/position.ML Sun Nov 25 18:50:13 2012 +0100
+++ b/src/Pure/General/position.ML Sun Nov 25 19:49:24 2012 +0100
@@ -62,7 +62,7 @@
fun norm_props (props: Properties.T) =
maps (fn a => the_list (find_first (fn (b, _) => a = b) props))
- Isabelle_Markup.position_properties';
+ Markup.position_properties';
fun make {line = i, offset = j, end_offset = k, props} = Pos ((i, j, k), norm_props props);
fun dest (Pos ((i, j, k), props)) = {line = i, offset = j, end_offset = k, props = props};
@@ -77,7 +77,7 @@
fun offset_of (Pos ((_, j, _), _)) = if valid j then SOME j else NONE;
fun end_offset_of (Pos ((_, _, k), _)) = if valid k then SOME k else NONE;
-fun file_of (Pos (_, props)) = Properties.get props Isabelle_Markup.fileN;
+fun file_of (Pos (_, props)) = Properties.get props Markup.fileN;
(* advance *)
@@ -109,7 +109,7 @@
fun file_name "" = []
- | file_name name = [(Isabelle_Markup.fileN, name)];
+ | file_name name = [(Markup.fileN, name)];
fun file_only name = Pos ((0, 0, 0), file_name name);
fun file name = Pos ((1, 1, 0), file_name name);
@@ -117,11 +117,11 @@
fun line_file i name = Pos ((i, 1, 0), file_name name);
fun line i = line_file i "";
-fun id id = Pos ((0, 1, 0), [(Isabelle_Markup.idN, id)]);
-fun id_only id = Pos ((0, 0, 0), [(Isabelle_Markup.idN, id)]);
+fun id id = Pos ((0, 1, 0), [(Markup.idN, id)]);
+fun id_only id = Pos ((0, 0, 0), [(Markup.idN, id)]);
-fun get_id (Pos (_, props)) = Properties.get props Isabelle_Markup.idN;
-fun put_id id (Pos (count, props)) = Pos (count, Properties.put (Isabelle_Markup.idN, id) props);
+fun get_id (Pos (_, props)) = Properties.get props Markup.idN;
+fun put_id id (Pos (count, props)) = Pos (count, Properties.put (Markup.idN, id) props);
(* markup properties *)
@@ -133,26 +133,24 @@
NONE => 0
| SOME s => the_default 0 (Int.fromString s));
in
- make {line = get Isabelle_Markup.lineN, offset = get Isabelle_Markup.offsetN,
- end_offset = get Isabelle_Markup.end_offsetN, props = props}
+ make {line = get Markup.lineN, offset = get Markup.offsetN,
+ end_offset = get Markup.end_offsetN, props = props}
end;
fun value k i = if valid i then [(k, string_of_int i)] else [];
fun properties_of (Pos ((i, j, k), props)) =
- value Isabelle_Markup.lineN i @
- value Isabelle_Markup.offsetN j @
- value Isabelle_Markup.end_offsetN k @ props;
+ value Markup.lineN i @ value Markup.offsetN j @ value Markup.end_offsetN k @ props;
val def_properties_of = properties_of #> (map (fn (x, y) => ("def_" ^ x, y)));
fun entity_properties_of def id pos =
- if def then (Isabelle_Markup.defN, string_of_int id) :: properties_of pos
- else (Isabelle_Markup.refN, string_of_int id) :: def_properties_of pos;
+ if def then (Markup.defN, string_of_int id) :: properties_of pos
+ else (Markup.refN, string_of_int id) :: def_properties_of pos;
fun default_properties default props =
- if exists (member (op =) Isabelle_Markup.position_properties o #1) props then props
+ if exists (member (op =) Markup.position_properties o #1) props then props
else properties_of default @ props;
val markup = Markup.properties o properties_of;
@@ -194,9 +192,7 @@
| _ => "");
in
if null props then ""
- else
- (if s = "" then "" else " ") ^
- Markup.markup (Markup.properties props Isabelle_Markup.position) s
+ else (if s = "" then "" else " ") ^ Markup.markup (Markup.properties props Markup.position) s
end;
val here_list = space_implode " " o map here;
--- a/src/Pure/General/position.scala Sun Nov 25 18:50:13 2012 +0100
+++ b/src/Pure/General/position.scala Sun Nov 25 19:49:24 2012 +0100
@@ -14,17 +14,17 @@
{
type T = Properties.T
- val Line = new Properties.Int(Isabelle_Markup.LINE)
- val Offset = new Properties.Int(Isabelle_Markup.OFFSET)
- val End_Offset = new Properties.Int(Isabelle_Markup.END_OFFSET)
- val File = new Properties.String(Isabelle_Markup.FILE)
- val Id = new Properties.Long(Isabelle_Markup.ID)
+ val Line = new Properties.Int(Markup.LINE)
+ val Offset = new Properties.Int(Markup.OFFSET)
+ val End_Offset = new Properties.Int(Markup.END_OFFSET)
+ val File = new Properties.String(Markup.FILE)
+ val Id = new Properties.Long(Markup.ID)
- val Def_Line = new Properties.Int(Isabelle_Markup.DEF_LINE)
- val Def_Offset = new Properties.Int(Isabelle_Markup.DEF_OFFSET)
- val Def_End_Offset = new Properties.Int(Isabelle_Markup.DEF_END_OFFSET)
- val Def_File = new Properties.String(Isabelle_Markup.DEF_FILE)
- val Def_Id = new Properties.Long(Isabelle_Markup.DEF_ID)
+ val Def_Line = new Properties.Int(Markup.DEF_LINE)
+ val Def_Offset = new Properties.Int(Markup.DEF_OFFSET)
+ val Def_End_Offset = new Properties.Int(Markup.DEF_END_OFFSET)
+ val Def_File = new Properties.String(Markup.DEF_FILE)
+ val Def_Id = new Properties.Long(Markup.DEF_ID)
object Line_File
{
@@ -84,7 +84,7 @@
}
}
- def purge(props: T): T = props.filterNot(p => Isabelle_Markup.POSITION_PROPERTIES(p._1))
+ def purge(props: T): T = props.filterNot(p => Markup.POSITION_PROPERTIES(p._1))
/* here: inlined formal markup */
--- a/src/Pure/General/pretty.ML Sun Nov 25 18:50:13 2012 +0100
+++ b/src/Pure/General/pretty.ML Sun Nov 25 19:49:24 2012 +0100
@@ -156,11 +156,11 @@
fun mark_str (m, s) = mark m (str s);
fun marks_str (ms, s) = fold_rev mark ms (str s);
-fun command name = mark_str (Isabelle_Markup.keyword1, name);
-fun keyword name = mark_str (Isabelle_Markup.keyword2, name);
+fun command name = mark_str (Markup.keyword1, name);
+fun keyword name = mark_str (Markup.keyword2, name);
val text = breaks o map str o Symbol.explode_words;
-val paragraph = markup Isabelle_Markup.paragraph;
+val paragraph = markup Markup.paragraph;
val para = paragraph o text;
fun markup_chunks m prts = markup m (fbreaks prts);
@@ -304,11 +304,11 @@
fun out (Block ((bg, en), [], _, _)) = Buffer.add bg #> Buffer.add en
| out (Block ((bg, en), prts, indent, _)) =
Buffer.add bg #>
- Buffer.markup (Isabelle_Markup.block indent) (fold out prts) #>
+ Buffer.markup (Markup.block indent) (fold out prts) #>
Buffer.add en
| out (String (s, _)) = Buffer.add s
| out (Break (false, wd)) =
- Buffer.markup (Isabelle_Markup.break wd) (Buffer.add (output_spaces wd))
+ Buffer.markup (Markup.break wd) (Buffer.add (output_spaces wd))
| out (Break (true, _)) = Buffer.add (Output.output "\n");
in out prt Buffer.empty end;
--- a/src/Pure/General/pretty.scala Sun Nov 25 18:50:13 2012 +0100
+++ b/src/Pure/General/pretty.scala Sun Nov 25 19:49:24 2012 +0100
@@ -34,11 +34,11 @@
object Block
{
def apply(i: Int, body: XML.Body): XML.Tree =
- XML.Elem(Markup(Isabelle_Markup.BLOCK, Isabelle_Markup.Indent(i)), body)
+ XML.Elem(Markup(Markup.BLOCK, Markup.Indent(i)), body)
def unapply(tree: XML.Tree): Option[(Int, XML.Body)] =
tree match {
- case XML.Elem(Markup(Isabelle_Markup.BLOCK, Isabelle_Markup.Indent(i)), body) =>
+ case XML.Elem(Markup(Markup.BLOCK, Markup.Indent(i)), body) =>
Some((i, body))
case _ => None
}
@@ -47,19 +47,19 @@
object Break
{
def apply(w: Int): XML.Tree =
- XML.Elem(Markup(Isabelle_Markup.BREAK, Isabelle_Markup.Width(w)),
+ XML.Elem(Markup(Markup.BREAK, Markup.Width(w)),
List(XML.Text(spaces(w))))
def unapply(tree: XML.Tree): Option[Int] =
tree match {
- case XML.Elem(Markup(Isabelle_Markup.BREAK, Isabelle_Markup.Width(w)), _) => Some(w)
+ case XML.Elem(Markup(Markup.BREAK, Markup.Width(w)), _) => Some(w)
case _ => None
}
}
val FBreak = XML.Text("\n")
- val Separator = List(XML.elem(Isabelle_Markup.SEPARATOR, List(XML.Text(space))), FBreak)
+ val Separator = List(XML.elem(Markup.SEPARATOR, List(XML.Text(space))), FBreak)
def separate(ts: List[XML.Tree]): XML.Body = Library.separate(Separator, ts.map(List(_))).flatten
--- a/src/Pure/General/symbol_pos.ML Sun Nov 25 18:50:13 2012 +0100
+++ b/src/Pure/General/symbol_pos.ML Sun Nov 25 19:49:24 2012 +0100
@@ -71,7 +71,7 @@
fun err (syms, msg) = fn () =>
text () ^ get_pos syms ^
- Markup.markup Isabelle_Markup.no_report (" at " ^ Symbol.beginning 10 (map symbol syms)) ^
+ Markup.markup Markup.no_report (" at " ^ Symbol.beginning 10 (map symbol syms)) ^
(case msg of NONE => "" | SOME m => "\n" ^ m ());
in Scan.!! err scan end;
--- a/src/Pure/Isar/obtain.ML Sun Nov 25 18:50:13 2012 +0100
+++ b/src/Pure/Isar/obtain.ML Sun Nov 25 19:49:24 2012 +0100
@@ -299,7 +299,7 @@
val goal = Var (("guess", 0), propT);
fun print_result ctxt' (k, [(s, [_, th])]) =
- Proof_Display.print_results Isabelle_Markup.state int ctxt' (k, [(s, [th])]);
+ Proof_Display.print_results Markup.state int ctxt' (k, [(s, [th])]);
val before_qed = SOME (Method.primitive_text (Goal.conclude #> Raw_Simplifier.norm_hhf #>
(fn th => Goal.protect (Conjunction.intr (Drule.mk_term (Thm.cprop_of th)) th))));
fun after_qed [[_, res]] =
--- a/src/Pure/Isar/outer_syntax.ML Sun Nov 25 18:50:13 2012 +0100
+++ b/src/Pure/Isar/outer_syntax.ML Sun Nov 25 19:49:24 2012 +0100
@@ -60,7 +60,7 @@
fun command_markup def (name, Command {pos, id, ...}) =
Markup.properties (Position.entity_properties_of def id pos)
- (Isabelle_Markup.entity Isabelle_Markup.commandN name);
+ (Markup.entity Markup.commandN name);
(* parse command *)
--- a/src/Pure/Isar/proof.ML Sun Nov 25 18:50:13 2012 +0100
+++ b/src/Pure/Isar/proof.ML Sun Nov 25 19:49:24 2012 +0100
@@ -536,7 +536,7 @@
fun status_markup state =
(case try goal state of
- SOME {goal, ...} => Isabelle_Markup.proof_state (Thm.nprems_of goal)
+ SOME {goal, ...} => Markup.proof_state (Thm.nprems_of goal)
| NONE => Markup.empty);
fun method_error kind pos state =
@@ -1031,7 +1031,7 @@
fun skipped_proof state =
Context_Position.if_visible (context_of state) Output.report
- (Markup.markup Isabelle_Markup.bad "Skipped proof");
+ (Markup.markup Markup.bad "Skipped proof");
in
@@ -1051,7 +1051,7 @@
local
fun gen_have prep_att prepp before_qed after_qed stmt int =
- local_goal (Proof_Display.print_results Isabelle_Markup.state int)
+ local_goal (Proof_Display.print_results Markup.state int)
prep_att prepp "have" before_qed after_qed stmt;
fun gen_show prep_att prepp before_qed after_qed stmt int state =
@@ -1065,12 +1065,11 @@
fun print_results ctxt res =
if ! testing then ()
- else Proof_Display.print_results Isabelle_Markup.state int ctxt res;
+ else Proof_Display.print_results Markup.state int ctxt res;
fun print_rule ctxt th =
if ! testing then rule := SOME th
else if int then
- writeln
- (Markup.markup Isabelle_Markup.state (Proof_Display.string_of_rule ctxt "Successful" th))
+ writeln (Markup.markup Markup.state (Proof_Display.string_of_rule ctxt "Successful" th))
else ();
val test_proof =
try (local_skip_proof true)
--- a/src/Pure/Isar/proof_context.ML Sun Nov 25 18:50:13 2012 +0100
+++ b/src/Pure/Isar/proof_context.ML Sun Nov 25 19:49:24 2012 +0100
@@ -444,7 +444,7 @@
val (c, pos) = token_content text;
in
if Lexicon.is_tid c then
- (Context_Position.report ctxt pos Isabelle_Markup.tfree;
+ (Context_Position.report ctxt pos Markup.tfree;
TFree (c, default_sort ctxt (c, ~1)))
else
let
@@ -476,8 +476,7 @@
(case (Variable.lookup_fixed ctxt c, Variable.is_const ctxt c) of
(SOME x, false) =>
(Context_Position.report ctxt pos
- (Markup.name x
- (if can Name.dest_skolem x then Isabelle_Markup.skolem else Isabelle_Markup.free));
+ (Markup.name x (if can Name.dest_skolem x then Markup.skolem else Markup.free));
Free (x, infer_type ctxt (x, ty)))
| _ => prep_const_proper ctxt strict (c, pos))
end;
@@ -650,8 +649,7 @@
fun add_report S pos reports =
if Position.is_reported pos andalso not (AList.defined (op =) reports pos) then
- (pos, Position.reported_text pos Isabelle_Markup.sorting (Syntax.string_of_sort ctxt S))
- :: reports
+ (pos, Position.reported_text pos Markup.sorting (Syntax.string_of_sort ctxt S)) :: reports
else reports;
fun get_sort_reports xi raw_S =
--- a/src/Pure/Isar/runtime.ML Sun Nov 25 18:50:13 2012 +0100
+++ b/src/Pure/Isar/runtime.ML Sun Nov 25 19:49:24 2012 +0100
@@ -65,7 +65,7 @@
fun exn_msgs (context, (i, exn)) =
(case exn of
EXCURSION_FAIL (exn, loc) =>
- map (apsnd (fn msg => msg ^ Markup.markup Isabelle_Markup.no_report ("\n" ^ loc)))
+ map (apsnd (fn msg => msg ^ Markup.markup Markup.no_report ("\n" ^ loc)))
(sorted_msgs context exn)
| _ =>
let
--- a/src/Pure/Isar/token.ML Sun Nov 25 18:50:13 2012 +0100
+++ b/src/Pure/Isar/token.ML Sun Nov 25 19:49:24 2012 +0100
@@ -204,9 +204,7 @@
fun source_of (Token ((source, (pos, _)), (_, x), _)) =
if YXML.detect x then x
- else
- YXML.string_of
- (XML.Elem (Isabelle_Markup.token (Position.properties_of pos), [XML.Text source]));
+ else YXML.string_of (XML.Elem (Markup.token (Position.properties_of pos), [XML.Text source]));
fun source_position_of (Token ((source, (pos, _)), _, _)) = (source, pos);
--- a/src/Pure/Isar/toplevel.ML Sun Nov 25 18:50:13 2012 +0100
+++ b/src/Pure/Isar/toplevel.ML Sun Nov 25 19:49:24 2012 +0100
@@ -211,7 +211,7 @@
| SOME (Proof (prf, _)) =>
Proof.pretty_state (Proof_Node.position prf) (Proof_Node.current prf)
| SOME (SkipProof (d, _)) => [Pretty.str ("skipped proof: depth " ^ string_of_int d)])
- |> Pretty.markup_chunks Isabelle_Markup.state |> Pretty.writeln;
+ |> Pretty.markup_chunks Markup.state |> Pretty.writeln;
fun pretty_abstract state = Pretty.str ("<Isar " ^ str_of_state state ^ ">");
--- a/src/Pure/ML/ml_compiler_polyml.ML Sun Nov 25 18:50:13 2012 +0100
+++ b/src/Pure/ML/ml_compiler_polyml.ML Sun Nov 25 19:49:24 2012 +0100
@@ -15,7 +15,7 @@
endLine = _, endPosition = end_offset} = loc;
val props =
(case YXML.parse text of
- XML.Elem ((e, atts), _) => if e = Isabelle_Markup.positionN then atts else []
+ XML.Elem ((e, atts), _) => if e = Markup.positionN then atts else []
| XML.Text s => Position.file_name s);
in
Position.make {line = line, offset = offset, end_offset = end_offset, props = props}
@@ -41,20 +41,19 @@
fun reported_entity kind loc decl =
reported_text (position_of loc)
- (Isabelle_Markup.entityN,
- (Markup.kindN, kind) :: Position.def_properties_of (position_of decl)) "";
+ (Markup.entityN, (Markup.kindN, kind) :: Position.def_properties_of (position_of decl)) "";
fun reported loc (PolyML.PTtype types) =
cons
(PolyML.NameSpace.displayTypeExpression (types, depth, space)
|> pretty_ml |> Pretty.from_ML |> Pretty.string_of
- |> reported_text (position_of loc) Isabelle_Markup.ML_typing)
+ |> reported_text (position_of loc) Markup.ML_typing)
| reported loc (PolyML.PTdeclaredAt decl) =
- cons (reported_entity Isabelle_Markup.ML_defN loc decl)
+ cons (reported_entity Markup.ML_defN loc decl)
| reported loc (PolyML.PTopenedAt decl) =
- cons (reported_entity Isabelle_Markup.ML_openN loc decl)
+ cons (reported_entity Markup.ML_openN loc decl)
| reported loc (PolyML.PTstructureAt decl) =
- cons (reported_entity Isabelle_Markup.ML_structN loc decl)
+ cons (reported_entity Markup.ML_structN loc decl)
| reported _ (PolyML.PTnextSibling tree) = reported_tree (tree ())
| reported _ (PolyML.PTfirstChild tree) = reported_tree (tree ())
| reported _ _ = I
@@ -73,9 +72,9 @@
(* input *)
val location_props =
- op ^ (YXML.output_markup (Isabelle_Markup.position |> Markup.properties
- (filter (member (op =)
- [Isabelle_Markup.idN, Isabelle_Markup.fileN] o #1) (Position.properties_of pos))));
+ op ^
+ (YXML.output_markup (Markup.position |> Markup.properties
+ (filter (member (op =) [Markup.idN, Markup.fileN] o #1) (Position.properties_of pos))));
val input_buffer =
Unsynchronized.ref (toks |> map
--- a/src/Pure/ML/ml_context.ML Sun Nov 25 18:50:13 2012 +0100
+++ b/src/Pure/ML/ml_context.ML Sun Nov 25 19:49:24 2012 +0100
@@ -103,7 +103,7 @@
structure Antiq_Parsers = Theory_Data
(
type T = (Position.T -> antiq context_parser) Name_Space.table;
- val empty : T = Name_Space.empty_table Isabelle_Markup.ML_antiquotationN;
+ val empty : T = Name_Space.empty_table Markup.ML_antiquotationN;
val extend = I;
fun merge data : T = Name_Space.merge_tables data;
);
@@ -119,7 +119,7 @@
val thy = Proof_Context.theory_of ctxt;
val ((xname, _), pos) = Args.dest_src src;
val (_, scan) = Name_Space.check (Context.Proof ctxt) (Antiq_Parsers.get thy) (xname, pos);
- in Args.context_syntax Isabelle_Markup.ML_antiquotationN (scan pos) src ctxt end;
+ in Args.context_syntax Markup.ML_antiquotationN (scan pos) src ctxt end;
(* parsing and evaluation *)
--- a/src/Pure/ML/ml_lex.ML Sun Nov 25 18:50:13 2012 +0100
+++ b/src/Pure/ML/ml_lex.ML Sun Nov 25 19:49:24 2012 +0100
@@ -104,23 +104,23 @@
local
val token_kind_markup =
- fn Keyword => (Isabelle_Markup.ML_keyword, "")
+ fn Keyword => (Markup.ML_keyword, "")
| Ident => (Markup.empty, "")
| LongIdent => (Markup.empty, "")
- | TypeVar => (Isabelle_Markup.ML_tvar, "")
- | Word => (Isabelle_Markup.ML_numeral, "")
- | Int => (Isabelle_Markup.ML_numeral, "")
- | Real => (Isabelle_Markup.ML_numeral, "")
- | Char => (Isabelle_Markup.ML_char, "")
- | String => (Isabelle_Markup.ML_string, "")
+ | TypeVar => (Markup.ML_tvar, "")
+ | Word => (Markup.ML_numeral, "")
+ | Int => (Markup.ML_numeral, "")
+ | Real => (Markup.ML_numeral, "")
+ | Char => (Markup.ML_char, "")
+ | String => (Markup.ML_string, "")
| Space => (Markup.empty, "")
- | Comment => (Isabelle_Markup.ML_comment, "")
- | Error msg => (Isabelle_Markup.bad, msg)
+ | Comment => (Markup.ML_comment, "")
+ | Error msg => (Markup.bad, msg)
| EOF => (Markup.empty, "");
fun token_markup kind x =
if kind = Keyword andalso exists_string (not o Symbol.is_ascii_letter) x
- then (Isabelle_Markup.ML_delimiter, "")
+ then (Markup.ML_delimiter, "")
else token_kind_markup kind;
in
@@ -289,7 +289,7 @@
fun read pos txt =
let
- val _ = Position.report pos Isabelle_Markup.ML_source;
+ val _ = Position.report pos Markup.ML_source;
val syms = Symbol_Pos.explode (txt, pos);
val termination =
if null syms then []
--- a/src/Pure/PIDE/command.ML Sun Nov 25 18:50:13 2012 +0100
+++ b/src/Pure/PIDE/command.ML Sun Nov 25 19:49:24 2012 +0100
@@ -75,7 +75,7 @@
handle exn => ML_Compiler.exn_messages exn)) ();
fun timing tr t =
- if Timing.is_relevant t then Toplevel.status tr (Isabelle_Markup.timing t) else ();
+ if Timing.is_relevant t then Toplevel.status tr (Markup.timing t) else ();
fun proof_status tr st =
(case try Toplevel.proof_of st of
@@ -99,20 +99,20 @@
val is_proof = Keyword.is_proof (Toplevel.name_of tr);
val _ = Multithreading.interrupted ();
- val _ = Toplevel.status tr Isabelle_Markup.running;
+ val _ = Toplevel.status tr Markup.running;
val start = Timing.start ();
val (errs1, result) = run (is_init orelse is_proof) (Toplevel.set_print false tr) st;
val errs2 = (case result of NONE => [] | SOME st' => check_cmts tr cmts st');
val errs = errs1 @ errs2;
val _ = timing tr (Timing.result start);
- val _ = Toplevel.status tr Isabelle_Markup.finished;
+ val _ = Toplevel.status tr Markup.finished;
val _ = List.app (Toplevel.error_msg tr) errs;
in
(case result of
NONE =>
let
val _ = if null errs then Exn.interrupt () else ();
- val _ = Toplevel.status tr Isabelle_Markup.failed;
+ val _ = Toplevel.status tr Markup.failed;
in ((st, malformed'), no_print) end
| SOME st' =>
let
--- a/src/Pure/PIDE/command.scala Sun Nov 25 18:50:13 2012 +0100
+++ b/src/Pure/PIDE/command.scala Sun Nov 25 19:49:24 2012 +0100
@@ -34,7 +34,7 @@
def + (alt_id: Document.ID, message: XML.Elem): Command.State =
message match {
- case XML.Elem(Markup(Isabelle_Markup.STATUS, _), msgs) =>
+ case XML.Elem(Markup(Markup.STATUS, _), msgs) =>
(this /: msgs)((state, msg) =>
msg match {
case elem @ XML.Elem(markup, Nil) =>
@@ -43,7 +43,7 @@
case _ => System.err.println("Ignored status message: " + msg); state
})
- case XML.Elem(Markup(Isabelle_Markup.REPORT, _), msgs) =>
+ case XML.Elem(Markup(Markup.REPORT, _), msgs) =>
(this /: msgs)((state, msg) =>
msg match {
case XML.Elem(Markup(name, atts @ Position.Id_Range(id, raw_range)), args)
@@ -54,7 +54,7 @@
val info: Text.Markup = Text.Info(range, XML.Elem(Markup(name, props), args))
state.add_markup(info)
case XML.Elem(Markup(name, atts), args)
- if !atts.exists({ case (a, _) => Isabelle_Markup.POSITION_PROPERTIES(a) }) =>
+ if !atts.exists({ case (a, _) => Markup.POSITION_PROPERTIES(a) }) =>
val range = command.proper_range
val props = Position.purge(atts)
val info: Text.Markup = Text.Info(range, XML.Elem(Markup(name, props), args))
@@ -65,9 +65,9 @@
})
case XML.Elem(Markup(name, atts), body) =>
atts match {
- case Isabelle_Markup.Serial(i) =>
+ case Markup.Serial(i) =>
val props = Position.purge(atts)
- val message1 = XML.Elem(Markup(Isabelle_Markup.message(name), props), body)
+ val message1 = XML.Elem(Markup(Markup.message(name), props), body)
val message2 = XML.Elem(Markup(name, props), body)
val st0 = copy(results = results + (i -> message1))
--- a/src/Pure/PIDE/document.ML Sun Nov 25 18:50:13 2012 +0100
+++ b/src/Pure/PIDE/document.ML Sun Nov 25 19:49:24 2012 +0100
@@ -272,7 +272,7 @@
(#1 (Outer_Syntax.get_syntax ())) (Position.id id_string) text) ());
val _ =
Position.setmp_thread_data (Position.id_only id_string)
- (fn () => Output.status (Markup.markup_only Isabelle_Markup.accepted)) ();
+ (fn () => Output.status (Markup.markup_only Markup.accepted)) ();
val commands' =
Inttab.update_new (id, (name, span)) commands
handle Inttab.DUP dup => err_dup "command" dup;
--- a/src/Pure/PIDE/isabelle_markup.ML Sun Nov 25 18:50:13 2012 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,336 +0,0 @@
-(* Title: Pure/PIDE/isabelle_markup.ML
- Author: Makarius
-
-Isabelle markup elements.
-*)
-
-signature ISABELLE_MARKUP =
-sig
- val bindingN: string val binding: Markup.T
- val entityN: string val entity: string -> string -> Markup.T
- val get_entity_kind: Markup.T -> string option
- val defN: string
- val refN: string
- val lineN: string
- val offsetN: string
- val end_offsetN: string
- val fileN: string
- val idN: string
- val position_properties': string list
- val position_properties: string list
- val positionN: string val position: Markup.T
- val pathN: string val path: string -> Markup.T
- val indentN: string
- val blockN: string val block: int -> Markup.T
- val widthN: string
- val breakN: string val break: int -> Markup.T
- val fbreakN: string val fbreak: Markup.T
- val hiddenN: string val hidden: Markup.T
- val theoryN: string
- val classN: string
- val type_nameN: string
- val constantN: string
- val fixedN: string val fixed: string -> Markup.T
- val dynamic_factN: string val dynamic_fact: string -> Markup.T
- val tfreeN: string val tfree: Markup.T
- val tvarN: string val tvar: Markup.T
- val freeN: string val free: Markup.T
- val skolemN: string val skolem: Markup.T
- val boundN: string val bound: Markup.T
- val varN: string val var: Markup.T
- val numeralN: string val numeral: Markup.T
- val literalN: string val literal: Markup.T
- val delimiterN: string val delimiter: Markup.T
- val inner_stringN: string val inner_string: Markup.T
- val inner_commentN: string val inner_comment: Markup.T
- val token_rangeN: string val token_range: Markup.T
- val sortN: string val sort: Markup.T
- val typN: string val typ: Markup.T
- val termN: string val term: Markup.T
- val propN: string val prop: Markup.T
- val sortingN: string val sorting: Markup.T
- val typingN: string val typing: Markup.T
- val ML_keywordN: string val ML_keyword: Markup.T
- val ML_delimiterN: string val ML_delimiter: Markup.T
- val ML_tvarN: string val ML_tvar: Markup.T
- val ML_numeralN: string val ML_numeral: Markup.T
- val ML_charN: string val ML_char: Markup.T
- val ML_stringN: string val ML_string: Markup.T
- val ML_commentN: string val ML_comment: Markup.T
- val ML_defN: string
- val ML_openN: string
- val ML_structN: string
- val ML_typingN: string val ML_typing: Markup.T
- val ML_sourceN: string val ML_source: Markup.T
- val doc_sourceN: string val doc_source: Markup.T
- val antiqN: string val antiq: Markup.T
- val ML_antiquotationN: string
- val document_antiquotationN: string
- val document_antiquotation_optionN: string
- val paragraphN: string val paragraph: Markup.T
- val keywordN: string val keyword: Markup.T
- val operatorN: string val operator: Markup.T
- val commandN: string val command: Markup.T
- val stringN: string val string: Markup.T
- val altstringN: string val altstring: Markup.T
- val verbatimN: string val verbatim: Markup.T
- val commentN: string val comment: Markup.T
- val controlN: string val control: Markup.T
- val tokenN: string val token: Properties.T -> Markup.T
- val keyword1N: string val keyword1: Markup.T
- val keyword2N: string val keyword2: Markup.T
- val elapsedN: string
- val cpuN: string
- val gcN: string
- val timingN: string val timing: Timing.timing -> Markup.T
- val subgoalsN: string
- val proof_stateN: string val proof_state: int -> Markup.T
- val stateN: string val state: Markup.T
- val subgoalN: string val subgoal: Markup.T
- val sendbackN: string val sendback: Markup.T
- val intensifyN: string val intensify: Markup.T
- val taskN: string
- val acceptedN: string val accepted: Markup.T
- val forkedN: string val forked: Markup.T
- val joinedN: string val joined: Markup.T
- val runningN: string val running: Markup.T
- val finishedN: string val finished: Markup.T
- val failedN: string val failed: Markup.T
- val serialN: string
- val initN: string
- val statusN: string
- val writelnN: string
- val tracingN: string
- val warningN: string
- val errorN: string
- val protocolN: string
- val legacyN: string val legacy: Markup.T
- val promptN: string val prompt: Markup.T
- val reportN: string val report: Markup.T
- val no_reportN: string val no_report: Markup.T
- val badN: string val bad: Markup.T
- val graphviewN: string
- val functionN: string
- val assign_execs: Properties.T
- val removed_versions: Properties.T
- val invoke_scala: string -> string -> Properties.T
- val cancel_scala: string -> Properties.T
-end;
-
-structure Isabelle_Markup: ISABELLE_MARKUP =
-struct
-
-(** markup elements **)
-
-fun markup_elem elem = (elem, (elem, []): Markup.T);
-fun markup_string elem prop = (elem, fn s => (elem, [(prop, s)]): Markup.T);
-fun markup_int elem prop = (elem, fn i => (elem, [(prop, Markup.print_int i)]): Markup.T);
-
-
-(* formal entities *)
-
-val (bindingN, binding) = markup_elem "binding";
-
-val entityN = "entity";
-fun entity kind name = (entityN, [(Markup.nameN, name), (Markup.kindN, kind)]);
-
-fun get_entity_kind (name, props) =
- if name = entityN then AList.lookup (op =) props Markup.kindN
- else NONE;
-
-val defN = "def";
-val refN = "ref";
-
-
-(* position *)
-
-val lineN = "line";
-val offsetN = "offset";
-val end_offsetN = "end_offset";
-val fileN = "file";
-val idN = "id";
-
-val position_properties' = [fileN, idN];
-val position_properties = [lineN, offsetN, end_offsetN] @ position_properties';
-
-val (positionN, position) = markup_elem "position";
-
-
-(* path *)
-
-val (pathN, path) = markup_string "path" Markup.nameN;
-
-
-(* pretty printing *)
-
-val indentN = "indent";
-val (blockN, block) = markup_int "block" indentN;
-
-val widthN = "width";
-val (breakN, break) = markup_int "break" widthN;
-
-val (fbreakN, fbreak) = markup_elem "fbreak";
-
-
-(* hidden text *)
-
-val (hiddenN, hidden) = markup_elem "hidden";
-
-
-(* logical entities *)
-
-val theoryN = "theory";
-val classN = "class";
-val type_nameN = "type_name";
-val constantN = "constant";
-
-val (fixedN, fixed) = markup_string "fixed" Markup.nameN;
-val (dynamic_factN, dynamic_fact) = markup_string "dynamic_fact" Markup.nameN;
-
-
-(* inner syntax *)
-
-val (tfreeN, tfree) = markup_elem "tfree";
-val (tvarN, tvar) = markup_elem "tvar";
-val (freeN, free) = markup_elem "free";
-val (skolemN, skolem) = markup_elem "skolem";
-val (boundN, bound) = markup_elem "bound";
-val (varN, var) = markup_elem "var";
-val (numeralN, numeral) = markup_elem "numeral";
-val (literalN, literal) = markup_elem "literal";
-val (delimiterN, delimiter) = markup_elem "delimiter";
-val (inner_stringN, inner_string) = markup_elem "inner_string";
-val (inner_commentN, inner_comment) = markup_elem "inner_comment";
-
-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";
-
-
-(* ML syntax *)
-
-val (ML_keywordN, ML_keyword) = markup_elem "ML_keyword";
-val (ML_delimiterN, ML_delimiter) = markup_elem "ML_delimiter";
-val (ML_tvarN, ML_tvar) = markup_elem "ML_tvar";
-val (ML_numeralN, ML_numeral) = markup_elem "ML_numeral";
-val (ML_charN, ML_char) = markup_elem "ML_char";
-val (ML_stringN, ML_string) = markup_elem "ML_string";
-val (ML_commentN, ML_comment) = markup_elem "ML_comment";
-
-val ML_defN = "ML_def";
-val ML_openN = "ML_open";
-val ML_structN = "ML_struct";
-val (ML_typingN, ML_typing) = markup_elem "ML_typing";
-
-
-(* embedded source text *)
-
-val (ML_sourceN, ML_source) = markup_elem "ML_source";
-val (doc_sourceN, doc_source) = markup_elem "doc_source";
-
-val (antiqN, antiq) = markup_elem "antiq";
-val ML_antiquotationN = "ML_antiquotation";
-val document_antiquotationN = "document_antiquotation";
-val document_antiquotation_optionN = "document_antiquotation_option";
-
-
-(* text structure *)
-
-val (paragraphN, paragraph) = markup_elem "paragraph";
-
-
-(* outer syntax *)
-
-val (keywordN, keyword) = markup_elem "keyword";
-val (operatorN, operator) = markup_elem "operator";
-val (commandN, command) = markup_elem "command";
-val (stringN, string) = markup_elem "string";
-val (altstringN, altstring) = markup_elem "altstring";
-val (verbatimN, verbatim) = markup_elem "verbatim";
-val (commentN, comment) = markup_elem "comment";
-val (controlN, control) = markup_elem "control";
-
-val tokenN = "token";
-fun token props = (tokenN, props);
-
-val (keyword1N, keyword1) = markup_elem "keyword1";
-val (keyword2N, keyword2) = markup_elem "keyword2";
-
-
-(* timing *)
-
-val timingN = "timing";
-val elapsedN = "elapsed";
-val cpuN = "cpu";
-val gcN = "gc";
-
-fun timing {elapsed, cpu, gc} =
- (timingN,
- [(elapsedN, Time.toString elapsed),
- (cpuN, Time.toString cpu),
- (gcN, Time.toString gc)]);
-
-
-(* toplevel *)
-
-val subgoalsN = "subgoals";
-val (proof_stateN, proof_state) = markup_int "proof_state" subgoalsN;
-
-val (stateN, state) = markup_elem "state";
-val (subgoalN, subgoal) = markup_elem "subgoal";
-val (sendbackN, sendback) = markup_elem "sendback";
-val (intensifyN, intensify) = markup_elem "intensify";
-
-
-(* command status *)
-
-val taskN = "task";
-
-val (acceptedN, accepted) = markup_elem "accepted";
-val (forkedN, forked) = markup_elem "forked";
-val (joinedN, joined) = markup_elem "joined";
-val (runningN, running) = markup_elem "running";
-val (finishedN, finished) = markup_elem "finished";
-val (failedN, failed) = markup_elem "failed";
-
-
-(* messages *)
-
-val serialN = "serial";
-
-val initN = "init";
-val statusN = "status";
-val writelnN = "writeln";
-val tracingN = "tracing";
-val warningN = "warning";
-val errorN = "error";
-val protocolN = "protocol";
-
-val (legacyN, legacy) = markup_elem "legacy";
-val (promptN, prompt) = markup_elem "prompt";
-
-val (reportN, report) = markup_elem "report";
-val (no_reportN, no_report) = markup_elem "no_report";
-
-val (badN, bad) = markup_elem "bad";
-
-val graphviewN = "graphview";
-
-
-(* protocol message functions *)
-
-val functionN = "function"
-
-val assign_execs = [(functionN, "assign_execs")];
-val removed_versions = [(functionN, "removed_versions")];
-
-fun invoke_scala name id = [(functionN, "invoke_scala"), (Markup.nameN, name), (idN, id)];
-fun cancel_scala id = [(functionN, "cancel_scala"), (idN, id)];
-
-end;
--- a/src/Pure/PIDE/isabelle_markup.scala Sun Nov 25 18:50:13 2012 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,291 +0,0 @@
-/* Title: Pure/PIDE/isabelle_markup.scala
- Author: Makarius
-
-Isabelle markup elements.
-*/
-
-package isabelle
-
-
-object Isabelle_Markup
-{
- /* formal entities */
-
- val BINDING = "binding"
- val ENTITY = "entity"
- val DEF = "def"
- val REF = "ref"
-
- object Entity
- {
- def unapply(markup: Markup): Option[(String, String)] =
- markup match {
- case Markup(ENTITY, props @ Markup.Kind(kind)) =>
- props match {
- case Markup.Name(name) => Some(kind, name)
- case _ => None
- }
- case _ => None
- }
- }
-
-
- /* position */
-
- val LINE = "line"
- val OFFSET = "offset"
- val END_OFFSET = "end_offset"
- val FILE = "file"
- val ID = "id"
-
- val DEF_LINE = "def_line"
- val DEF_OFFSET = "def_offset"
- val DEF_END_OFFSET = "def_end_offset"
- val DEF_FILE = "def_file"
- val DEF_ID = "def_id"
-
- val POSITION_PROPERTIES = Set(LINE, OFFSET, END_OFFSET, FILE, ID)
- val POSITION = "position"
-
-
- /* path */
-
- val PATH = "path"
-
- object Path
- {
- def unapply(markup: Markup): Option[String] =
- markup match {
- case Markup(PATH, Markup.Name(name)) => Some(name)
- case _ => None
- }
- }
-
-
- /* pretty printing */
-
- val Indent = new Properties.Int("indent")
- val BLOCK = "block"
- val Width = new Properties.Int("width")
- val BREAK = "break"
-
- val SEPARATOR = "separator"
-
-
- /* hidden text */
-
- val HIDDEN = "hidden"
-
-
- /* logical entities */
-
- val CLASS = "class"
- val TYPE_NAME = "type_name"
- val FIXED = "fixed"
- val CONSTANT = "constant"
-
- val DYNAMIC_FACT = "dynamic_fact"
-
-
- /* inner syntax */
-
- val TFREE = "tfree"
- val TVAR = "tvar"
- val FREE = "free"
- val SKOLEM = "skolem"
- val BOUND = "bound"
- val VAR = "var"
- val NUMERAL = "numeral"
- val LITERAL = "literal"
- val DELIMITER = "delimiter"
- val INNER_STRING = "inner_string"
- val INNER_COMMENT = "inner_comment"
-
- val TOKEN_RANGE = "token_range"
-
- val SORT = "sort"
- val TYP = "typ"
- val TERM = "term"
- val PROP = "prop"
-
- val SORTING = "sorting"
- val TYPING = "typing"
-
- val ATTRIBUTE = "attribute"
- val METHOD = "method"
-
-
- /* embedded source text */
-
- val ML_SOURCE = "ML_source"
- val DOCUMENT_SOURCE = "document_source"
-
- val ANTIQ = "antiq"
- val ML_ANTIQUOTATION = "ML_antiquotation"
- val DOCUMENT_ANTIQUOTATION = "document_antiquotation"
- val DOCUMENT_ANTIQUOTATION_OPTION = "document_antiquotation_option"
-
-
- /* text structure */
-
- val PARAGRAPH = "paragraph"
-
-
- /* ML syntax */
-
- val ML_KEYWORD = "ML_keyword"
- val ML_DELIMITER = "ML_delimiter"
- val ML_TVAR = "ML_tvar"
- val ML_NUMERAL = "ML_numeral"
- val ML_CHAR = "ML_char"
- val ML_STRING = "ML_string"
- val ML_COMMENT = "ML_comment"
-
- val ML_DEF = "ML_def"
- val ML_OPEN = "ML_open"
- val ML_STRUCT = "ML_struct"
- val ML_TYPING = "ML_typing"
-
-
- /* outer syntax */
-
- val KEYWORD = "keyword"
- val OPERATOR = "operator"
- val COMMAND = "command"
- val STRING = "string"
- val ALTSTRING = "altstring"
- val VERBATIM = "verbatim"
- val COMMENT = "comment"
- val CONTROL = "control"
-
- val KEYWORD1 = "keyword1"
- val KEYWORD2 = "keyword2"
-
-
- /* timing */
-
- val TIMING = "timing"
- val ELAPSED = "elapsed"
- val CPU = "cpu"
- val GC = "gc"
-
- object Timing
- {
- def apply(timing: isabelle.Timing): Markup =
- Markup(TIMING, List(
- (ELAPSED, Properties.Value.Double(timing.elapsed.seconds)),
- (CPU, Properties.Value.Double(timing.cpu.seconds)),
- (GC, Properties.Value.Double(timing.gc.seconds))))
- def unapply(markup: Markup): Option[isabelle.Timing] =
- markup match {
- case Markup(TIMING, List(
- (ELAPSED, Properties.Value.Double(elapsed)),
- (CPU, Properties.Value.Double(cpu)),
- (GC, Properties.Value.Double(gc)))) =>
- Some(new isabelle.Timing(Time.seconds(elapsed), Time.seconds(cpu), Time.seconds(gc)))
- case _ => None
- }
- }
-
-
- /* toplevel */
-
- val SUBGOALS = "subgoals"
- val PROOF_STATE = "proof_state"
-
- val STATE = "state"
- val SUBGOAL = "subgoal"
- val SENDBACK = "sendback"
- val INTENSIFY = "intensify"
-
-
- /* command status */
-
- val TASK = "task"
-
- val ACCEPTED = "accepted"
- val FORKED = "forked"
- val JOINED = "joined"
- val RUNNING = "running"
- val FINISHED = "finished"
- val FAILED = "failed"
-
-
- /* interactive documents */
-
- val VERSION = "version"
- val ASSIGN = "assign"
-
-
- /* prover process */
-
- val PROVER_COMMAND = "prover_command"
- val PROVER_ARG = "prover_arg"
-
-
- /* messages */
-
- val Serial = new Properties.Long("serial")
-
- val MESSAGE = "message"
-
- val INIT = "init"
- val STATUS = "status"
- val REPORT = "report"
- val WRITELN = "writeln"
- val TRACING = "tracing"
- val WARNING = "warning"
- val ERROR = "error"
- val PROTOCOL = "protocol"
- val SYSTEM = "system"
- val STDOUT = "stdout"
- val STDERR = "stderr"
- val EXIT = "exit"
-
- val WRITELN_MESSAGE = "writeln_message"
- val TRACING_MESSAGE = "tracing_message"
- val WARNING_MESSAGE = "warning_message"
- val ERROR_MESSAGE = "error_message"
-
- val message: String => String =
- Map(WRITELN -> WRITELN_MESSAGE, TRACING -> TRACING_MESSAGE,
- WARNING -> WARNING_MESSAGE, ERROR -> ERROR_MESSAGE)
- .withDefault((name: String) => name + "_message")
-
- val Return_Code = new Properties.Int("return_code")
-
- val LEGACY = "legacy"
-
- val NO_REPORT = "no_report"
-
- val BAD = "bad"
-
- val GRAPHVIEW = "graphview"
-
-
- /* protocol message functions */
-
- val FUNCTION = "function"
- val Function = new Properties.String(FUNCTION)
-
- val Assign_Execs: Properties.T = List((FUNCTION, "assign_execs"))
- val Removed_Versions: Properties.T = List((FUNCTION, "removed_versions"))
-
- object Invoke_Scala
- {
- def unapply(props: Properties.T): Option[(String, String)] =
- props match {
- case List((FUNCTION, "invoke_scala"), (Markup.NAME, name), (ID, id)) => Some((name, id))
- case _ => None
- }
- }
- object Cancel_Scala
- {
- def unapply(props: Properties.T): Option[String] =
- props match {
- case List((FUNCTION, "cancel_scala"), (ID, id)) => Some(id)
- case _ => None
- }
- }
-}
-
--- a/src/Pure/PIDE/markup.ML Sun Nov 25 18:50:13 2012 +0100
+++ b/src/Pure/PIDE/markup.ML Sun Nov 25 19:49:24 2012 +0100
@@ -1,7 +1,7 @@
(* Title: Pure/PIDE/markup.ML
Author: Makarius
-Generic markup elements.
+Isabelle-specific implementation of quasi-abstract markup elements.
*)
signature MARKUP =
@@ -15,6 +15,115 @@
val nameN: string
val name: string -> T -> T
val kindN: string
+ val bindingN: string val binding: T
+ val entityN: string val entity: string -> string -> T
+ val get_entity_kind: T -> string option
+ val defN: string
+ val refN: string
+ val lineN: string
+ val offsetN: string
+ val end_offsetN: string
+ val fileN: string
+ val idN: string
+ val position_properties': string list
+ val position_properties: string list
+ val positionN: string val position: T
+ val pathN: string val path: string -> T
+ val indentN: string
+ val blockN: string val block: int -> T
+ val widthN: string
+ val breakN: string val break: int -> T
+ val fbreakN: string val fbreak: T
+ val hiddenN: string val hidden: T
+ val theoryN: string
+ val classN: string
+ val type_nameN: string
+ val constantN: string
+ val fixedN: string val fixed: string -> T
+ val dynamic_factN: string val dynamic_fact: string -> T
+ val tfreeN: string val tfree: T
+ val tvarN: string val tvar: T
+ val freeN: string val free: T
+ val skolemN: string val skolem: T
+ val boundN: string val bound: T
+ val varN: string val var: T
+ val numeralN: string val numeral: T
+ val literalN: string val literal: T
+ val delimiterN: string val delimiter: T
+ val inner_stringN: string val inner_string: 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_keywordN: string val ML_keyword: T
+ val ML_delimiterN: string val ML_delimiter: T
+ val ML_tvarN: string val ML_tvar: T
+ val ML_numeralN: string val ML_numeral: T
+ val ML_charN: string val ML_char: T
+ val ML_stringN: string val ML_string: T
+ val ML_commentN: string val ML_comment: T
+ val ML_defN: string
+ 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 doc_sourceN: string val doc_source: T
+ val antiqN: string val antiq: T
+ val ML_antiquotationN: string
+ val document_antiquotationN: string
+ val document_antiquotation_optionN: string
+ val paragraphN: string val paragraph: T
+ val keywordN: string val keyword: T
+ val operatorN: string val operator: T
+ val commandN: string val command: T
+ val stringN: string val string: T
+ val altstringN: string val altstring: T
+ val verbatimN: string val verbatim: T
+ val commentN: string val comment: T
+ val controlN: string val control: T
+ val tokenN: string val token: Properties.T -> T
+ val keyword1N: string val keyword1: T
+ val keyword2N: string val keyword2: T
+ val elapsedN: string
+ val cpuN: string
+ val gcN: string
+ val timingN: string val timing: Timing.timing -> T
+ val subgoalsN: string
+ val proof_stateN: string val proof_state: int -> T
+ val stateN: string val state: T
+ val subgoalN: string val subgoal: T
+ val sendbackN: string val sendback: T
+ val intensifyN: string val intensify: T
+ val taskN: string
+ val acceptedN: string val accepted: T
+ val forkedN: string val forked: T
+ val joinedN: string val joined: T
+ val runningN: string val running: T
+ val finishedN: string val finished: T
+ val failedN: string val failed: T
+ val serialN: string
+ val initN: string
+ val statusN: string
+ val writelnN: string
+ val tracingN: string
+ val warningN: string
+ val errorN: string
+ val protocolN: string
+ val legacyN: string val legacy: T
+ val promptN: string val prompt: T
+ val reportN: string val report: T
+ val no_reportN: string val no_report: T
+ val badN: string val bad: T
+ val graphviewN: string
+ val functionN: string
+ val assign_execs: Properties.T
+ val removed_versions: Properties.T
+ val invoke_scala: string -> string -> Properties.T
+ val cancel_scala: string -> 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
@@ -54,6 +163,10 @@
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);
+
(* misc properties *)
@@ -63,6 +176,213 @@
val kindN = "kind";
+(* formal entities *)
+
+val (bindingN, binding) = markup_elem "binding";
+
+val entityN = "entity";
+fun entity kind name = (entityN, [(nameN, name), (kindN, kind)]);
+
+fun get_entity_kind (name, props) =
+ if name = entityN then AList.lookup (op =) props kindN
+ else NONE;
+
+val defN = "def";
+val refN = "ref";
+
+
+(* position *)
+
+val lineN = "line";
+val offsetN = "offset";
+val end_offsetN = "end_offset";
+val fileN = "file";
+val idN = "id";
+
+val position_properties' = [fileN, idN];
+val position_properties = [lineN, offsetN, end_offsetN] @ position_properties';
+
+val (positionN, position) = markup_elem "position";
+
+
+(* path *)
+
+val (pathN, path) = markup_string "path" nameN;
+
+
+(* pretty printing *)
+
+val indentN = "indent";
+val (blockN, block) = markup_int "block" indentN;
+
+val widthN = "width";
+val (breakN, break) = markup_int "break" widthN;
+
+val (fbreakN, fbreak) = markup_elem "fbreak";
+
+
+(* hidden text *)
+
+val (hiddenN, hidden) = markup_elem "hidden";
+
+
+(* logical entities *)
+
+val theoryN = "theory";
+val classN = "class";
+val type_nameN = "type_name";
+val constantN = "constant";
+
+val (fixedN, fixed) = markup_string "fixed" nameN;
+val (dynamic_factN, dynamic_fact) = markup_string "dynamic_fact" nameN;
+
+
+(* inner syntax *)
+
+val (tfreeN, tfree) = markup_elem "tfree";
+val (tvarN, tvar) = markup_elem "tvar";
+val (freeN, free) = markup_elem "free";
+val (skolemN, skolem) = markup_elem "skolem";
+val (boundN, bound) = markup_elem "bound";
+val (varN, var) = markup_elem "var";
+val (numeralN, numeral) = markup_elem "numeral";
+val (literalN, literal) = markup_elem "literal";
+val (delimiterN, delimiter) = markup_elem "delimiter";
+val (inner_stringN, inner_string) = markup_elem "inner_string";
+val (inner_commentN, inner_comment) = markup_elem "inner_comment";
+
+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";
+
+
+(* ML syntax *)
+
+val (ML_keywordN, ML_keyword) = markup_elem "ML_keyword";
+val (ML_delimiterN, ML_delimiter) = markup_elem "ML_delimiter";
+val (ML_tvarN, ML_tvar) = markup_elem "ML_tvar";
+val (ML_numeralN, ML_numeral) = markup_elem "ML_numeral";
+val (ML_charN, ML_char) = markup_elem "ML_char";
+val (ML_stringN, ML_string) = markup_elem "ML_string";
+val (ML_commentN, ML_comment) = markup_elem "ML_comment";
+
+val ML_defN = "ML_def";
+val ML_openN = "ML_open";
+val ML_structN = "ML_struct";
+val (ML_typingN, ML_typing) = markup_elem "ML_typing";
+
+
+(* embedded source text *)
+
+val (ML_sourceN, ML_source) = markup_elem "ML_source";
+val (doc_sourceN, doc_source) = markup_elem "doc_source";
+
+val (antiqN, antiq) = markup_elem "antiq";
+val ML_antiquotationN = "ML_antiquotation";
+val document_antiquotationN = "document_antiquotation";
+val document_antiquotation_optionN = "document_antiquotation_option";
+
+
+(* text structure *)
+
+val (paragraphN, paragraph) = markup_elem "paragraph";
+
+
+(* outer syntax *)
+
+val (keywordN, keyword) = markup_elem "keyword";
+val (operatorN, operator) = markup_elem "operator";
+val (commandN, command) = markup_elem "command";
+val (stringN, string) = markup_elem "string";
+val (altstringN, altstring) = markup_elem "altstring";
+val (verbatimN, verbatim) = markup_elem "verbatim";
+val (commentN, comment) = markup_elem "comment";
+val (controlN, control) = markup_elem "control";
+
+val tokenN = "token";
+fun token props = (tokenN, props);
+
+val (keyword1N, keyword1) = markup_elem "keyword1";
+val (keyword2N, keyword2) = markup_elem "keyword2";
+
+
+(* timing *)
+
+val timingN = "timing";
+val elapsedN = "elapsed";
+val cpuN = "cpu";
+val gcN = "gc";
+
+fun timing {elapsed, cpu, gc} =
+ (timingN,
+ [(elapsedN, Time.toString elapsed),
+ (cpuN, Time.toString cpu),
+ (gcN, Time.toString gc)]);
+
+
+(* toplevel *)
+
+val subgoalsN = "subgoals";
+val (proof_stateN, proof_state) = markup_int "proof_state" subgoalsN;
+
+val (stateN, state) = markup_elem "state";
+val (subgoalN, subgoal) = markup_elem "subgoal";
+val (sendbackN, sendback) = markup_elem "sendback";
+val (intensifyN, intensify) = markup_elem "intensify";
+
+
+(* command status *)
+
+val taskN = "task";
+
+val (acceptedN, accepted) = markup_elem "accepted";
+val (forkedN, forked) = markup_elem "forked";
+val (joinedN, joined) = markup_elem "joined";
+val (runningN, running) = markup_elem "running";
+val (finishedN, finished) = markup_elem "finished";
+val (failedN, failed) = markup_elem "failed";
+
+
+(* messages *)
+
+val serialN = "serial";
+
+val initN = "init";
+val statusN = "status";
+val writelnN = "writeln";
+val tracingN = "tracing";
+val warningN = "warning";
+val errorN = "error";
+val protocolN = "protocol";
+
+val (legacyN, legacy) = markup_elem "legacy";
+val (promptN, prompt) = markup_elem "prompt";
+
+val (reportN, report) = markup_elem "report";
+val (no_reportN, no_report) = markup_elem "no_report";
+
+val (badN, bad) = markup_elem "bad";
+
+val graphviewN = "graphview";
+
+
+(* protocol message functions *)
+
+val functionN = "function"
+
+val assign_execs = [(functionN, "assign_execs")];
+val removed_versions = [(functionN, "removed_versions")];
+
+fun invoke_scala name id = [(functionN, "invoke_scala"), (nameN, name), (idN, id)];
+fun cancel_scala id = [(functionN, "cancel_scala"), (idN, id)];
+
+
(** print mode operations **)
--- a/src/Pure/PIDE/markup.scala Sun Nov 25 18:50:13 2012 +0100
+++ b/src/Pure/PIDE/markup.scala Sun Nov 25 19:49:24 2012 +0100
@@ -2,7 +2,7 @@
Module: PIDE
Author: Makarius
-Generic markup elements.
+Isabelle-specific implementation of quasi-abstract markup elements.
*/
package isabelle
@@ -19,10 +19,290 @@
val Kind = new Properties.String(KIND)
- /* elements */
+ /* basic markup */
val Empty = Markup("", Nil)
val Broken = Markup("broken", Nil)
+
+
+ /* formal entities */
+
+ val BINDING = "binding"
+ val ENTITY = "entity"
+ val DEF = "def"
+ val REF = "ref"
+
+ object Entity
+ {
+ def unapply(markup: Markup): Option[(String, String)] =
+ markup match {
+ case Markup(ENTITY, props @ Kind(kind)) =>
+ props match {
+ case Name(name) => Some(kind, name)
+ case _ => None
+ }
+ case _ => None
+ }
+ }
+
+
+ /* position */
+
+ val LINE = "line"
+ val OFFSET = "offset"
+ val END_OFFSET = "end_offset"
+ val FILE = "file"
+ val ID = "id"
+
+ val DEF_LINE = "def_line"
+ val DEF_OFFSET = "def_offset"
+ val DEF_END_OFFSET = "def_end_offset"
+ val DEF_FILE = "def_file"
+ val DEF_ID = "def_id"
+
+ val POSITION_PROPERTIES = Set(LINE, OFFSET, END_OFFSET, FILE, ID)
+ val POSITION = "position"
+
+
+ /* path */
+
+ val PATH = "path"
+
+ object Path
+ {
+ def unapply(markup: Markup): Option[String] =
+ markup match {
+ case Markup(PATH, Name(name)) => Some(name)
+ case _ => None
+ }
+ }
+
+
+ /* pretty printing */
+
+ val Indent = new Properties.Int("indent")
+ val BLOCK = "block"
+ val Width = new Properties.Int("width")
+ val BREAK = "break"
+
+ val SEPARATOR = "separator"
+
+
+ /* hidden text */
+
+ val HIDDEN = "hidden"
+
+
+ /* logical entities */
+
+ val CLASS = "class"
+ val TYPE_NAME = "type_name"
+ val FIXED = "fixed"
+ val CONSTANT = "constant"
+
+ val DYNAMIC_FACT = "dynamic_fact"
+
+
+ /* inner syntax */
+
+ val TFREE = "tfree"
+ val TVAR = "tvar"
+ val FREE = "free"
+ val SKOLEM = "skolem"
+ val BOUND = "bound"
+ val VAR = "var"
+ val NUMERAL = "numeral"
+ val LITERAL = "literal"
+ val DELIMITER = "delimiter"
+ val INNER_STRING = "inner_string"
+ val INNER_COMMENT = "inner_comment"
+
+ val TOKEN_RANGE = "token_range"
+
+ val SORT = "sort"
+ val TYP = "typ"
+ val TERM = "term"
+ val PROP = "prop"
+
+ val SORTING = "sorting"
+ val TYPING = "typing"
+
+ val ATTRIBUTE = "attribute"
+ val METHOD = "method"
+
+
+ /* embedded source text */
+
+ val ML_SOURCE = "ML_source"
+ val DOCUMENT_SOURCE = "document_source"
+
+ val ANTIQ = "antiq"
+ val ML_ANTIQUOTATION = "ML_antiquotation"
+ val DOCUMENT_ANTIQUOTATION = "document_antiquotation"
+ val DOCUMENT_ANTIQUOTATION_OPTION = "document_antiquotation_option"
+
+
+ /* text structure */
+
+ val PARAGRAPH = "paragraph"
+
+
+ /* ML syntax */
+
+ val ML_KEYWORD = "ML_keyword"
+ val ML_DELIMITER = "ML_delimiter"
+ val ML_TVAR = "ML_tvar"
+ val ML_NUMERAL = "ML_numeral"
+ val ML_CHAR = "ML_char"
+ val ML_STRING = "ML_string"
+ val ML_COMMENT = "ML_comment"
+
+ val ML_DEF = "ML_def"
+ val ML_OPEN = "ML_open"
+ val ML_STRUCT = "ML_struct"
+ val ML_TYPING = "ML_typing"
+
+
+ /* outer syntax */
+
+ val KEYWORD = "keyword"
+ val OPERATOR = "operator"
+ val COMMAND = "command"
+ val STRING = "string"
+ val ALTSTRING = "altstring"
+ val VERBATIM = "verbatim"
+ val COMMENT = "comment"
+ val CONTROL = "control"
+
+ val KEYWORD1 = "keyword1"
+ val KEYWORD2 = "keyword2"
+
+
+ /* timing */
+
+ val TIMING = "timing"
+ val ELAPSED = "elapsed"
+ val CPU = "cpu"
+ val GC = "gc"
+
+ object Timing
+ {
+ def apply(timing: isabelle.Timing): Markup =
+ Markup(TIMING, List(
+ (ELAPSED, Properties.Value.Double(timing.elapsed.seconds)),
+ (CPU, Properties.Value.Double(timing.cpu.seconds)),
+ (GC, Properties.Value.Double(timing.gc.seconds))))
+ def unapply(markup: Markup): Option[isabelle.Timing] =
+ markup match {
+ case Markup(TIMING, List(
+ (ELAPSED, Properties.Value.Double(elapsed)),
+ (CPU, Properties.Value.Double(cpu)),
+ (GC, Properties.Value.Double(gc)))) =>
+ Some(new isabelle.Timing(Time.seconds(elapsed), Time.seconds(cpu), Time.seconds(gc)))
+ case _ => None
+ }
+ }
+
+
+ /* toplevel */
+
+ val SUBGOALS = "subgoals"
+ val PROOF_STATE = "proof_state"
+
+ val STATE = "state"
+ val SUBGOAL = "subgoal"
+ val SENDBACK = "sendback"
+ val INTENSIFY = "intensify"
+
+
+ /* command status */
+
+ val TASK = "task"
+
+ val ACCEPTED = "accepted"
+ val FORKED = "forked"
+ val JOINED = "joined"
+ val RUNNING = "running"
+ val FINISHED = "finished"
+ val FAILED = "failed"
+
+
+ /* interactive documents */
+
+ val VERSION = "version"
+ val ASSIGN = "assign"
+
+
+ /* prover process */
+
+ val PROVER_COMMAND = "prover_command"
+ val PROVER_ARG = "prover_arg"
+
+
+ /* messages */
+
+ val Serial = new Properties.Long("serial")
+
+ val MESSAGE = "message"
+
+ val INIT = "init"
+ val STATUS = "status"
+ val REPORT = "report"
+ val WRITELN = "writeln"
+ val TRACING = "tracing"
+ val WARNING = "warning"
+ val ERROR = "error"
+ val PROTOCOL = "protocol"
+ val SYSTEM = "system"
+ val STDOUT = "stdout"
+ val STDERR = "stderr"
+ val EXIT = "exit"
+
+ val WRITELN_MESSAGE = "writeln_message"
+ val TRACING_MESSAGE = "tracing_message"
+ val WARNING_MESSAGE = "warning_message"
+ val ERROR_MESSAGE = "error_message"
+
+ val message: String => String =
+ Map(WRITELN -> WRITELN_MESSAGE, TRACING -> TRACING_MESSAGE,
+ WARNING -> WARNING_MESSAGE, ERROR -> ERROR_MESSAGE)
+ .withDefault((name: String) => name + "_message")
+
+ val Return_Code = new Properties.Int("return_code")
+
+ val LEGACY = "legacy"
+
+ val NO_REPORT = "no_report"
+
+ val BAD = "bad"
+
+ val GRAPHVIEW = "graphview"
+
+
+ /* protocol message functions */
+
+ val FUNCTION = "function"
+ val Function = new Properties.String(FUNCTION)
+
+ val Assign_Execs: Properties.T = List((FUNCTION, "assign_execs"))
+ val Removed_Versions: Properties.T = List((FUNCTION, "removed_versions"))
+
+ object Invoke_Scala
+ {
+ def unapply(props: Properties.T): Option[(String, String)] =
+ props match {
+ case List((FUNCTION, "invoke_scala"), (NAME, name), (ID, id)) => Some((name, id))
+ case _ => None
+ }
+ }
+ object Cancel_Scala
+ {
+ def unapply(props: Properties.T): Option[String] =
+ props match {
+ case List((FUNCTION, "cancel_scala"), (ID, id)) => Some(id)
+ case _ => None
+ }
+ }
}
--- a/src/Pure/PIDE/protocol.ML Sun Nov 25 18:50:13 2012 +0100
+++ b/src/Pure/PIDE/protocol.ML Sun Nov 25 19:49:24 2012 +0100
@@ -53,7 +53,7 @@
val (assignment, state') = Document.update old_id new_id edits state;
val _ =
- Output.protocol_message Isabelle_Markup.assign_execs
+ Output.protocol_message Markup.assign_execs
((new_id, assignment) |>
let open XML.Encode
in pair int (list (pair int (option int))) end
@@ -72,7 +72,7 @@
YXML.parse_body versions_yxml |>
let open XML.Decode in list int end;
val state1 = Document.remove_versions versions state;
- val _ = Output.protocol_message Isabelle_Markup.removed_versions versions_yxml;
+ val _ = Output.protocol_message Markup.removed_versions versions_yxml;
in state1 end));
val _ =
--- a/src/Pure/PIDE/protocol.scala Sun Nov 25 18:50:13 2012 +0100
+++ b/src/Pure/PIDE/protocol.scala Sun Nov 25 19:49:24 2012 +0100
@@ -66,17 +66,17 @@
}
val command_status_markup: Set[String] =
- Set(Isabelle_Markup.ACCEPTED, Isabelle_Markup.FORKED, Isabelle_Markup.JOINED,
- Isabelle_Markup.RUNNING, Isabelle_Markup.FINISHED, Isabelle_Markup.FAILED)
+ Set(Markup.ACCEPTED, Markup.FORKED, Markup.JOINED, Markup.RUNNING,
+ Markup.FINISHED, Markup.FAILED)
def command_status(status: Status, markup: Markup): Status =
markup match {
- case Markup(Isabelle_Markup.ACCEPTED, _) => status.copy(accepted = true)
- case Markup(Isabelle_Markup.FORKED, _) => status.copy(touched = true, forks = status.forks + 1)
- case Markup(Isabelle_Markup.JOINED, _) => status.copy(forks = status.forks - 1)
- case Markup(Isabelle_Markup.RUNNING, _) => status.copy(touched = true, runs = status.runs + 1)
- case Markup(Isabelle_Markup.FINISHED, _) => status.copy(runs = status.runs - 1)
- case Markup(Isabelle_Markup.FAILED, _) => status.copy(failed = true)
+ case Markup(Markup.ACCEPTED, _) => status.copy(accepted = true)
+ case Markup(Markup.FORKED, _) => status.copy(touched = true, forks = status.forks + 1)
+ case Markup(Markup.JOINED, _) => status.copy(forks = status.forks - 1)
+ case Markup(Markup.RUNNING, _) => status.copy(touched = true, runs = status.runs + 1)
+ case Markup(Markup.FINISHED, _) => status.copy(runs = status.runs - 1)
+ case Markup(Markup.FAILED, _) => status.copy(failed = true)
case _ => status
}
@@ -120,8 +120,8 @@
def clean_message(body: XML.Body): XML.Body =
body filter {
- case XML.Elem(Markup(Isabelle_Markup.REPORT, _), _) => false
- case XML.Elem(Markup(Isabelle_Markup.NO_REPORT, _), _) => false
+ case XML.Elem(Markup(Markup.REPORT, _), _) => false
+ case XML.Elem(Markup(Markup.NO_REPORT, _), _) => false
case _ => true
} map {
case XML.Wrapped_Elem(markup, body, ts) => XML.Wrapped_Elem(markup, body, clean_message(ts))
@@ -131,8 +131,8 @@
def message_reports(props: Properties.T, body: XML.Body): List[XML.Elem] =
body flatMap {
- case XML.Elem(Markup(Isabelle_Markup.REPORT, ps), ts) =>
- List(XML.Elem(Markup(Isabelle_Markup.REPORT, props ::: ps), ts))
+ case XML.Elem(Markup(Markup.REPORT, ps), ts) =>
+ List(XML.Elem(Markup(Markup.REPORT, props ::: ps), ts))
case XML.Wrapped_Elem(_, _, ts) => message_reports(props, ts)
case XML.Elem(_, ts) => message_reports(props, ts)
case XML.Text(_) => Nil
@@ -143,40 +143,38 @@
def is_tracing(msg: XML.Tree): Boolean =
msg match {
- case XML.Elem(Markup(Isabelle_Markup.TRACING, _), _) => true
- case XML.Elem(Markup(Isabelle_Markup.TRACING_MESSAGE, _), _) => true
+ case XML.Elem(Markup(Markup.TRACING, _), _) => true
+ case XML.Elem(Markup(Markup.TRACING_MESSAGE, _), _) => true
case _ => false
}
def is_warning(msg: XML.Tree): Boolean =
msg match {
- case XML.Elem(Markup(Isabelle_Markup.WARNING, _), _) => true
- case XML.Elem(Markup(Isabelle_Markup.WARNING_MESSAGE, _), _) => true
+ case XML.Elem(Markup(Markup.WARNING, _), _) => true
+ case XML.Elem(Markup(Markup.WARNING_MESSAGE, _), _) => true
case _ => false
}
def is_error(msg: XML.Tree): Boolean =
msg match {
- case XML.Elem(Markup(Isabelle_Markup.ERROR, _), _) => true
- case XML.Elem(Markup(Isabelle_Markup.ERROR_MESSAGE, _), _) => true
+ case XML.Elem(Markup(Markup.ERROR, _), _) => true
+ case XML.Elem(Markup(Markup.ERROR_MESSAGE, _), _) => true
case _ => false
}
def is_state(msg: XML.Tree): Boolean =
msg match {
- case XML.Elem(Markup(Isabelle_Markup.WRITELN, _),
- List(XML.Elem(Markup(Isabelle_Markup.STATE, _), _))) => true
- case XML.Elem(Markup(Isabelle_Markup.WRITELN_MESSAGE, _),
- List(XML.Elem(Markup(Isabelle_Markup.STATE, _), _))) => true
+ case XML.Elem(Markup(Markup.WRITELN, _),
+ List(XML.Elem(Markup(Markup.STATE, _), _))) => true
+ case XML.Elem(Markup(Markup.WRITELN_MESSAGE, _),
+ List(XML.Elem(Markup(Markup.STATE, _), _))) => true
case _ => false
}
/* reported positions */
- private val include_pos =
- Set(Isabelle_Markup.BINDING, Isabelle_Markup.ENTITY, Isabelle_Markup.REPORT,
- Isabelle_Markup.POSITION)
+ private val include_pos = Set(Markup.BINDING, Markup.ENTITY, Markup.REPORT, Markup.POSITION)
def message_positions(command: Command, message: XML.Elem): Set[Text.Range] =
{
--- a/src/Pure/PIDE/sendback.ML Sun Nov 25 18:50:13 2012 +0100
+++ b/src/Pure/PIDE/sendback.ML Sun Nov 25 19:49:24 2012 +0100
@@ -19,13 +19,13 @@
let
val props =
(case Position.get_id (Position.thread_data ()) of
- SOME id => [(Isabelle_Markup.idN, id)]
+ SOME id => [(Markup.idN, id)]
| NONE => []);
- in Markup.properties props Isabelle_Markup.sendback end;
+ in Markup.properties props Markup.sendback end;
fun markup s = Markup.markup (make_markup ()) s;
-fun markup_implicit s = Markup.markup Isabelle_Markup.sendback s;
+fun markup_implicit s = Markup.markup Markup.sendback s;
end;
--- a/src/Pure/ProofGeneral/proof_general_emacs.ML Sun Nov 25 18:50:13 2012 +0100
+++ b/src/Pure/ProofGeneral/proof_general_emacs.ML Sun Nov 25 19:49:24 2012 +0100
@@ -39,24 +39,24 @@
| XML.Elem ((name, props), ts) =>
let
val (bg1, en1) =
- if name <> Isabelle_Markup.promptN andalso print_mode_active test_markupN
+ if name <> Markup.promptN andalso print_mode_active test_markupN
then XML.output_markup (name, props)
else Markup.no_output;
val (bg2, en2) =
if null ts then Markup.no_output
- else if name = Isabelle_Markup.stateN then (special "O" ^ "\n", "\n" ^ special "P")
- else if name = Isabelle_Markup.sendbackN then (special "W", special "X")
- else if name = Isabelle_Markup.intensifyN then (special "0", special "1")
- else if name = Isabelle_Markup.tfreeN then (special "C", special "A")
- else if name = Isabelle_Markup.tvarN then (special "D", special "A")
- else if name = Isabelle_Markup.freeN then (special "E", special "A")
- else if name = Isabelle_Markup.boundN then (special "F", special "A")
- else if name = Isabelle_Markup.varN then (special "G", special "A")
- else if name = Isabelle_Markup.skolemN then (special "H", special "A")
+ else if name = Markup.stateN then (special "O" ^ "\n", "\n" ^ special "P")
+ else if name = Markup.sendbackN then (special "W", special "X")
+ else if name = Markup.intensifyN then (special "0", special "1")
+ else if name = Markup.tfreeN then (special "C", special "A")
+ else if name = Markup.tvarN then (special "D", special "A")
+ else if name = Markup.freeN then (special "E", special "A")
+ else if name = Markup.boundN then (special "F", special "A")
+ else if name = Markup.varN then (special "G", special "A")
+ else if name = Markup.skolemN then (special "H", special "A")
else
- (case Isabelle_Markup.get_entity_kind (name, props) of
+ (case Markup.get_entity_kind (name, props) of
SOME kind =>
- if kind = Isabelle_Markup.classN then (special "B", special "A")
+ if kind = Markup.classN then (special "B", special "A")
else Markup.no_output
| NONE => Markup.no_output);
in
--- a/src/Pure/ProofGeneral/proof_general_pgip.ML Sun Nov 25 18:50:13 2012 +0100
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML Sun Nov 25 19:49:24 2012 +0100
@@ -101,8 +101,7 @@
val pgml_syms = map pgml_sym o Symbol.explode;
val token_markups =
- [Isabelle_Markup.tfreeN, Isabelle_Markup.tvarN, Isabelle_Markup.freeN,
- Isabelle_Markup.boundN, Isabelle_Markup.varN, Isabelle_Markup.skolemN];
+ [Markup.tfreeN, Markup.tvarN, Markup.freeN, Markup.boundN, Markup.varN, Markup.skolemN];
fun get_int props name =
(case Properties.get props name of NONE => NONE | SOME s => Int.fromString s);
@@ -115,11 +114,10 @@
in [Pgml.Atoms {kind = SOME name, content = content}] end
else
let val content = maps pgml_terms body in
- if name = Isabelle_Markup.blockN then
- [Pgml.Box {orient = NONE,
- indent = get_int atts Isabelle_Markup.indentN, content = content}]
- else if name = Isabelle_Markup.breakN then
- [Pgml.Break {mandatory = NONE, indent = get_int atts Isabelle_Markup.widthN}]
+ if name = Markup.blockN then
+ [Pgml.Box {orient = NONE, indent = get_int atts Markup.indentN, content = content}]
+ else if name = Markup.breakN then
+ [Pgml.Break {mandatory = NONE, indent = get_int atts Markup.widthN}]
else content
end
| pgml_terms (XML.Text text) = map (Pgml.Raw o Pgml.atom_to_xml) (pgml_syms text);
@@ -138,7 +136,7 @@
val area =
(case body of
[XML.Elem ((name, _), _)] =>
- if name = Isabelle_Markup.stateN then PgipTypes.Display else default_area
+ if name = Markup.stateN then PgipTypes.Display else default_area
| _ => default_area);
in Pgml.pgml_to_xml (pgml area (maps pgml_terms body)) end;
--- a/src/Pure/ROOT Sun Nov 25 18:50:13 2012 +0100
+++ b/src/Pure/ROOT Sun Nov 25 19:49:24 2012 +0100
@@ -144,7 +144,6 @@
"ML/ml_thms.ML"
"PIDE/command.ML"
"PIDE/document.ML"
- "PIDE/isabelle_markup.ML"
"PIDE/markup.ML"
"PIDE/protocol.ML"
"PIDE/sendback.ML"
--- a/src/Pure/ROOT.ML Sun Nov 25 18:50:13 2012 +0100
+++ b/src/Pure/ROOT.ML Sun Nov 25 19:49:24 2012 +0100
@@ -30,8 +30,7 @@
use "General/output.ML";
use "General/timing.ML";
use "PIDE/markup.ML";
-use "PIDE/isabelle_markup.ML";
-fun legacy_feature s = warning (Markup.markup Isabelle_Markup.legacy ("Legacy feature! " ^ s));
+fun legacy_feature s = warning (Markup.markup Markup.legacy ("Legacy feature! " ^ s));
use "General/scan.ML";
use "General/source.ML";
use "General/symbol.ML";
--- a/src/Pure/Syntax/lexicon.ML Sun Nov 25 18:50:13 2012 +0100
+++ b/src/Pure/Syntax/lexicon.ML Sun Nov 25 19:49:24 2012 +0100
@@ -190,19 +190,17 @@
(* markup *)
fun literal_markup s =
- if is_ascii_identifier s
- then Isabelle_Markup.literal
- else Isabelle_Markup.delimiter;
+ if is_ascii_identifier s then Markup.literal else Markup.delimiter;
val token_kind_markup =
- fn VarSy => Isabelle_Markup.var
- | TFreeSy => Isabelle_Markup.tfree
- | TVarSy => Isabelle_Markup.tvar
- | NumSy => Isabelle_Markup.numeral
- | FloatSy => Isabelle_Markup.numeral
- | XNumSy => Isabelle_Markup.numeral
- | StrSy => Isabelle_Markup.inner_string
- | Comment => Isabelle_Markup.inner_comment
+ fn VarSy => Markup.var
+ | TFreeSy => Markup.tfree
+ | TVarSy => Markup.tvar
+ | NumSy => Markup.numeral
+ | FloatSy => Markup.numeral
+ | XNumSy => Markup.numeral
+ | StrSy => Markup.inner_string
+ | Comment => Markup.inner_comment
| _ => Markup.empty;
fun report_of_token (Token (kind, s, (pos, _))) =
@@ -211,7 +209,7 @@
fun reported_token_range ctxt tok =
if is_proper tok
- then Context_Position.reported_text ctxt (pos_of_token tok) Isabelle_Markup.token_range ""
+ then Context_Position.reported_text ctxt (pos_of_token tok) Markup.token_range ""
else "";
--- a/src/Pure/Syntax/syntax.ML Sun Nov 25 18:50:13 2012 +0100
+++ b/src/Pure/Syntax/syntax.ML Sun Nov 25 19:49:24 2012 +0100
@@ -167,7 +167,7 @@
(* outer syntax token -- with optional YXML content *)
fun token_position (XML.Elem ((name, props), _)) =
- if name = Isabelle_Markup.tokenN then Position.of_properties props
+ if name = Markup.tokenN then Position.of_properties props
else Position.none
| token_position (XML.Text _) = Position.none;
@@ -190,7 +190,7 @@
in
(case YXML.parse_body str handle Fail msg => error msg of
body as [tree as XML.Elem ((name, _), _)] =>
- if name = Isabelle_Markup.tokenN then parse_tree tree else decode body
+ if name = Markup.tokenN then parse_tree tree else decode body
| [tree as XML.Text _] => parse_tree tree
| body => decode body)
end;
--- a/src/Pure/Syntax/syntax_phases.ML Sun Nov 25 18:50:13 2012 +0100
+++ b/src/Pure/Syntax/syntax_phases.ML Sun Nov 25 19:49:24 2012 +0100
@@ -51,16 +51,16 @@
[Name_Space.markup (Consts.space_of (Proof_Context.consts_of ctxt)) c];
fun markup_free ctxt x =
- [if can Name.dest_skolem x then Isabelle_Markup.skolem else Isabelle_Markup.free] @
+ [if can Name.dest_skolem x then Markup.skolem else Markup.free] @
(if Variable.is_body ctxt orelse Variable.is_fixed ctxt x
then [Variable.markup_fixed ctxt x]
else []);
-fun markup_var xi = [Markup.name (Term.string_of_vname xi) Isabelle_Markup.var];
+fun markup_var xi = [Markup.name (Term.string_of_vname xi) Markup.var];
fun markup_bound def ps (name, id) =
- let val entity = Isabelle_Markup.entity Isabelle_Markup.boundN name in
- Isabelle_Markup.bound ::
+ let val entity = Markup.entity Markup.boundN name in
+ Markup.bound ::
map (fn pos => Markup.properties (Position.entity_properties_of def id pos) entity) ps
end;
@@ -298,8 +298,7 @@
val pts = Syntax.parse syn root (filter Lexicon.is_proper toks)
handle ERROR msg =>
error (msg ^
- implode
- (map (Markup.markup Isabelle_Markup.report o Lexicon.reported_token_range ctxt) toks));
+ implode (map (Markup.markup Markup.report o Lexicon.reported_token_range ctxt) toks));
val len = length pts;
val limit = Config.get ctxt Syntax.ambiguity_limit;
@@ -330,11 +329,10 @@
fun parse_failed ctxt pos msg kind =
cat_error msg ("Failed to parse " ^ kind ^
- Markup.markup Isabelle_Markup.report
- (Context_Position.reported_text ctxt pos Isabelle_Markup.bad ""));
+ Markup.markup Markup.report (Context_Position.reported_text ctxt pos Markup.bad ""));
fun parse_sort ctxt =
- Syntax.parse_token ctxt Term_XML.Decode.sort Isabelle_Markup.sort
+ Syntax.parse_token ctxt Term_XML.Decode.sort Markup.sort
(fn (syms, pos) =>
parse_tree ctxt "sort" (syms, pos)
|> uncurry (report_result ctxt pos)
@@ -343,7 +341,7 @@
handle ERROR msg => parse_failed ctxt pos msg "sort");
fun parse_typ ctxt =
- Syntax.parse_token ctxt Term_XML.Decode.typ Isabelle_Markup.typ
+ Syntax.parse_token ctxt Term_XML.Decode.typ Markup.typ
(fn (syms, pos) =>
parse_tree ctxt "type" (syms, pos)
|> uncurry (report_result ctxt pos)
@@ -354,8 +352,8 @@
let
val (markup, kind, root, constrain) =
if is_prop
- then (Isabelle_Markup.prop, "proposition", "prop", Type.constraint propT)
- else (Isabelle_Markup.term, "term", Config.get ctxt Syntax.root, I);
+ then (Markup.prop, "proposition", "prop", Type.constraint propT)
+ else (Markup.term, "term", Config.get ctxt Syntax.root, I);
val decode = constrain o Term_XML.Decode.term;
in
Syntax.parse_token ctxt decode markup
@@ -605,24 +603,23 @@
let
val m =
if Variable.is_fixed ctxt x orelse Syntax.is_pretty_global ctxt
- then Isabelle_Markup.fixed x
- else Isabelle_Markup.intensify;
+ then Markup.fixed x else Markup.intensify;
in
if can Name.dest_skolem x
- then ([m, Isabelle_Markup.skolem], Variable.revert_fixed ctxt x)
- else ([m, Isabelle_Markup.free], x)
+ then ([m, Markup.skolem], Variable.revert_fixed ctxt x)
+ else ([m, Markup.free], x)
end;
fun var_or_skolem s =
(case Lexicon.read_variable s of
SOME (x, i) =>
(case try Name.dest_skolem x of
- NONE => (Isabelle_Markup.var, s)
- | SOME x' => (Isabelle_Markup.skolem, Term.string_of_vname (x', i)))
- | NONE => (Isabelle_Markup.var, s));
+ NONE => (Markup.var, s)
+ | SOME x' => (Markup.skolem, Term.string_of_vname (x', i)))
+ | NONE => (Markup.var, s));
-val typing_elem = YXML.output_markup_elem Isabelle_Markup.typing;
-val sorting_elem = YXML.output_markup_elem Isabelle_Markup.sorting;
+val typing_elem = YXML.output_markup_elem Markup.typing;
+val sorting_elem = YXML.output_markup_elem Markup.sorting;
fun unparse_t t_to_ast prt_t markup ctxt t =
let
@@ -647,14 +644,14 @@
case_fixed = fn x => free_or_skolem ctxt x,
case_default = fn x => ([], x)});
- fun token_trans "_tfree" x = SOME (Pretty.mark_str (Isabelle_Markup.tfree, x))
- | token_trans "_tvar" x = SOME (Pretty.mark_str (Isabelle_Markup.tvar, x))
+ fun token_trans "_tfree" x = SOME (Pretty.mark_str (Markup.tfree, x))
+ | token_trans "_tvar" x = SOME (Pretty.mark_str (Markup.tvar, x))
| token_trans "_free" x = SOME (Pretty.marks_str (free_or_skolem ctxt x))
- | token_trans "_bound" x = SOME (Pretty.mark_str (Isabelle_Markup.bound, x))
- | token_trans "_loose" x = SOME (Pretty.mark_str (Isabelle_Markup.bad, x))
+ | token_trans "_bound" x = SOME (Pretty.mark_str (Markup.bound, x))
+ | token_trans "_loose" x = SOME (Pretty.mark_str (Markup.bad, x))
| token_trans "_var" x = SOME (Pretty.mark_str (var_or_skolem x))
- | token_trans "_numeral" x = SOME (Pretty.mark_str (Isabelle_Markup.numeral, x))
- | token_trans "_inner_string" x = SOME (Pretty.mark_str (Isabelle_Markup.inner_string, x))
+ | token_trans "_numeral" x = SOME (Pretty.mark_str (Markup.numeral, x))
+ | token_trans "_inner_string" x = SOME (Pretty.mark_str (Markup.inner_string, x))
| token_trans _ _ = NONE;
fun markup_trans a [Ast.Variable x] = token_trans a x
@@ -694,8 +691,8 @@
in
-val unparse_sort = unparse_t sort_to_ast Printer.pretty_typ_ast Isabelle_Markup.sort;
-val unparse_typ = unparse_t typ_to_ast Printer.pretty_typ_ast Isabelle_Markup.typ;
+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;
fun unparse_term ctxt =
let
@@ -705,7 +702,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)))
- Isabelle_Markup.term ctxt
+ Markup.term ctxt
end;
end;
@@ -871,7 +868,7 @@
val typing_report =
fold2 (fn (pos, _) => fn ty =>
if Position.is_reported pos then
- cons (Position.reported_text pos Isabelle_Markup.typing
+ cons (Position.reported_text pos Markup.typing
(Syntax.string_of_typ ctxt (Logic.dest_type ty)))
else I) ps tys' []
|> implode;
--- a/src/Pure/Syntax/term_position.ML Sun Nov 25 18:50:13 2012 +0100
+++ b/src/Pure/Syntax/term_position.ML Sun Nov 25 19:49:24 2012 +0100
@@ -26,15 +26,15 @@
val position_text = XML.Text position_dummy;
fun pretty pos =
- Pretty.markup (Position.markup pos Isabelle_Markup.position) [Pretty.str position_dummy];
+ Pretty.markup (Position.markup pos Markup.position) [Pretty.str position_dummy];
fun encode pos =
- YXML.string_of (XML.Elem (Position.markup pos Isabelle_Markup.position, [position_text]));
+ YXML.string_of (XML.Elem (Position.markup pos Markup.position, [position_text]));
fun decode str =
(case YXML.parse_body str handle Fail msg => error msg of
[XML.Elem ((name, props), [arg])] =>
- if name = Isabelle_Markup.positionN andalso arg = position_text
+ if name = Markup.positionN andalso arg = position_text
then SOME (Position.of_properties props)
else NONE
| _ => NONE);
--- a/src/Pure/System/invoke_scala.ML Sun Nov 25 18:50:13 2012 +0100
+++ b/src/Pure/System/invoke_scala.ML Sun Nov 25 19:49:24 2012 +0100
@@ -33,10 +33,10 @@
fun promise_method name arg =
let
val id = new_id ();
- fun abort () = Output.protocol_message (Isabelle_Markup.cancel_scala id) "";
+ fun abort () = Output.protocol_message (Markup.cancel_scala id) "";
val promise = Future.promise abort : string future;
val _ = Synchronized.change promises (Symtab.update (id, promise));
- val _ = Output.protocol_message (Isabelle_Markup.invoke_scala name id) arg;
+ val _ = Output.protocol_message (Markup.invoke_scala name id) arg;
in promise end;
fun method name arg = Future.join (promise_method name arg);
--- a/src/Pure/System/isabelle_process.ML Sun Nov 25 18:50:13 2012 +0100
+++ b/src/Pure/System/isabelle_process.ML Sun Nov 25 19:49:24 2012 +0100
@@ -99,7 +99,7 @@
if body = "" then ()
else
message false mbox name
- ((case opt_serial of SOME i => cons (Isabelle_Markup.serialN, string_of_int i) | _ => I)
+ ((case opt_serial of SOME i => cons (Markup.serialN, string_of_int i) | _ => I)
(Position.properties_of (Position.thread_data ()))) body;
fun message_output mbox channel =
@@ -124,22 +124,20 @@
val mbox = Mailbox.create () : (string list * bool) Mailbox.T;
val _ = Simple_Thread.fork false (message_output mbox channel);
in
- Output.Private_Hooks.status_fn := standard_message mbox NONE Isabelle_Markup.statusN;
- Output.Private_Hooks.report_fn := standard_message mbox NONE Isabelle_Markup.reportN;
+ Output.Private_Hooks.status_fn := standard_message mbox NONE Markup.statusN;
+ Output.Private_Hooks.report_fn := standard_message mbox NONE Markup.reportN;
Output.Private_Hooks.writeln_fn :=
- (fn s => standard_message mbox (SOME (serial ())) Isabelle_Markup.writelnN s);
+ (fn s => standard_message mbox (SOME (serial ())) Markup.writelnN s);
Output.Private_Hooks.tracing_fn :=
- (fn s =>
- (update_tracing_limits s;
- standard_message mbox (SOME (serial ())) Isabelle_Markup.tracingN s));
+ (fn s => (update_tracing_limits s; standard_message mbox (SOME (serial ())) Markup.tracingN s));
Output.Private_Hooks.warning_fn :=
- (fn s => standard_message mbox (SOME (serial ())) Isabelle_Markup.warningN s);
+ (fn s => standard_message mbox (SOME (serial ())) Markup.warningN s);
Output.Private_Hooks.error_fn :=
- (fn (i, s) => standard_message mbox (SOME i) Isabelle_Markup.errorN s);
- Output.Private_Hooks.protocol_message_fn := message true mbox Isabelle_Markup.protocolN;
+ (fn (i, s) => standard_message mbox (SOME i) Markup.errorN s);
+ Output.Private_Hooks.protocol_message_fn := message true mbox Markup.protocolN;
Output.Private_Hooks.urgent_message_fn := ! Output.Private_Hooks.writeln_fn;
Output.Private_Hooks.prompt_fn := ignore;
- message true mbox Isabelle_Markup.initN [] (Session.welcome ())
+ message true mbox Markup.initN [] (Session.welcome ())
end;
end;
--- a/src/Pure/System/isabelle_process.scala Sun Nov 25 18:50:13 2012 +0100
+++ b/src/Pure/System/isabelle_process.scala Sun Nov 25 19:49:24 2012 +0100
@@ -25,10 +25,9 @@
class Input(name: String, args: List[String]) extends Message
{
override def toString: String =
- XML.Elem(Markup(Isabelle_Markup.PROVER_COMMAND, List((Markup.NAME, name))),
+ XML.Elem(Markup(Markup.PROVER_COMMAND, List((Markup.NAME, name))),
args.map(s =>
- List(XML.Text("\n"),
- XML.elem(Isabelle_Markup.PROVER_ARG, YXML.parse_body(s)))).flatten).toString
+ List(XML.Text("\n"), XML.elem(Markup.PROVER_ARG, YXML.parse_body(s)))).flatten).toString
}
class Output(val message: XML.Elem) extends Message
@@ -37,14 +36,14 @@
def properties: Properties.T = message.markup.properties
def body: XML.Body = message.body
- def is_init = kind == Isabelle_Markup.INIT
- def is_exit = kind == Isabelle_Markup.EXIT
- def is_stdout = kind == Isabelle_Markup.STDOUT
- def is_stderr = kind == Isabelle_Markup.STDERR
- def is_system = kind == Isabelle_Markup.SYSTEM
- def is_status = kind == Isabelle_Markup.STATUS
- def is_report = kind == Isabelle_Markup.REPORT
- def is_protocol = kind == Isabelle_Markup.PROTOCOL
+ def is_init = kind == Markup.INIT
+ def is_exit = kind == Markup.EXIT
+ def is_stdout = kind == Markup.STDOUT
+ def is_stderr = kind == Markup.STDERR
+ def is_system = kind == Markup.SYSTEM
+ def is_status = kind == Markup.STATUS
+ def is_report = kind == Markup.REPORT
+ def is_protocol = kind == Markup.PROTOCOL
def is_syslog = is_init || is_exit || is_system || is_stderr
override def toString: String =
@@ -85,15 +84,15 @@
private def system_output(text: String)
{
- receiver(new Output(XML.Elem(Markup(Isabelle_Markup.SYSTEM, Nil), List(XML.Text(text)))))
+ receiver(new Output(XML.Elem(Markup(Markup.SYSTEM, Nil), List(XML.Text(text)))))
}
private val xml_cache = new XML.Cache()
private def output_message(kind: String, props: Properties.T, body: XML.Body)
{
- if (kind == Isabelle_Markup.INIT) system_channel.accepted()
- if (kind == Isabelle_Markup.PROTOCOL)
+ if (kind == Markup.INIT) system_channel.accepted()
+ if (kind == Markup.PROTOCOL)
receiver(new Output(XML.Elem(Markup(kind, props), body)))
else {
val main = XML.Elem(Markup(kind, props), Protocol.clean_message(body))
@@ -105,7 +104,7 @@
private def exit_message(rc: Int)
{
- output_message(Isabelle_Markup.EXIT, Isabelle_Markup.Return_Code(rc),
+ output_message(Markup.EXIT, Markup.Return_Code(rc),
List(XML.Text("Return code: " + rc.toString)))
}
@@ -247,8 +246,8 @@
private def physical_output_actor(err: Boolean): (Thread, Actor) =
{
val (name, reader, markup) =
- if (err) ("standard_error", process.stderr, Isabelle_Markup.STDERR)
- else ("standard_output", process.stdout, Isabelle_Markup.STDOUT)
+ if (err) ("standard_error", process.stderr, Markup.STDERR)
+ else ("standard_output", process.stdout, Markup.STDOUT)
Simple_Thread.actor(name) {
try {
@@ -364,7 +363,7 @@
header match {
case List(XML.Elem(Markup(name, props), Nil)) =>
val kind = name.intern
- val body = read_chunk(kind != Isabelle_Markup.PROTOCOL)
+ val body = read_chunk(kind != Markup.PROTOCOL)
output_message(kind, props, body)
case _ =>
read_chunk(false)
--- a/src/Pure/System/session.scala Sun Nov 25 18:50:13 2012 +0100
+++ b/src/Pure/System/session.scala Sun Nov 25 19:49:24 2012 +0100
@@ -314,7 +314,7 @@
case _: Document.State.Fail => bad_output(output)
}
- case Isabelle_Markup.Assign_Execs if output.is_protocol =>
+ case Markup.Assign_Execs if output.is_protocol =>
XML.content(output.body) match {
case Protocol.Assign(id, assign) =>
try {
@@ -331,7 +331,7 @@
prune_next = System.currentTimeMillis() + prune_delay.ms
}
- case Isabelle_Markup.Removed_Versions if output.is_protocol =>
+ case Markup.Removed_Versions if output.is_protocol =>
XML.content(output.body) match {
case Protocol.Removed(removed) =>
try {
@@ -341,7 +341,7 @@
case _ => bad_output(output)
}
- case Isabelle_Markup.Invoke_Scala(name, id) if output.is_protocol =>
+ case Markup.Invoke_Scala(name, id) if output.is_protocol =>
futures += (id ->
default_thread_pool.submit(() =>
{
@@ -350,7 +350,7 @@
this_actor ! Finished_Scala(id, tag, result)
}))
- case Isabelle_Markup.Cancel_Scala(id) if output.is_protocol =>
+ case Markup.Cancel_Scala(id) if output.is_protocol =>
futures.get(id) match {
case Some(future) =>
future.cancel(true)
@@ -361,7 +361,7 @@
case _ if output.is_init =>
phase = Session.Ready
- case Isabelle_Markup.Return_Code(rc) if output.is_exit =>
+ case Markup.Return_Code(rc) if output.is_exit =>
if (rc == 0) phase = Session.Inactive
else phase = Session.Failed
--- a/src/Pure/Thy/html.ML Sun Nov 25 18:50:13 2012 +0100
+++ b/src/Pure/Thy/html.ML Sun Nov 25 19:49:24 2012 +0100
@@ -54,7 +54,7 @@
(* symbol output *)
local
- val hidden = span Isabelle_Markup.hiddenN |-> enclose;
+ val hidden = span Markup.hiddenN |-> enclose;
(* FIXME proper unicode -- produced on Scala side *)
val html_syms = Symtab.make
--- a/src/Pure/Thy/html.scala Sun Nov 25 18:50:13 2012 +0100
+++ b/src/Pure/Thy/html.scala Sun Nov 25 19:49:24 2012 +0100
@@ -51,7 +51,7 @@
XML.Elem(Markup(SPAN, List((STYLE, "font-family: " + font))), List(XML.Text(txt)))
def hidden(txt: String): XML.Elem =
- span(Isabelle_Markup.HIDDEN, List(XML.Text(txt)))
+ span(Markup.HIDDEN, List(XML.Text(txt)))
def sub(txt: String): XML.Elem = XML.elem("sub", List(XML.Text(txt)))
def sup(txt: String): XML.Elem = XML.elem("sup", List(XML.Text(txt)))
--- a/src/Pure/Thy/latex.ML Sun Nov 25 18:50:13 2012 +0100
+++ b/src/Pure/Thy/latex.ML Sun Nov 25 19:49:24 2012 +0100
@@ -178,9 +178,9 @@
in (output_symbols syms, Symbol.length syms) end;
fun latex_markup (s, _) =
- if s = Isabelle_Markup.commandN orelse s = Isabelle_Markup.keyword1N
+ if s = Markup.commandN orelse s = Markup.keyword1N
then ("\\isacommand{", "}")
- else if s = Isabelle_Markup.keywordN orelse s = Isabelle_Markup.keyword2N
+ else if s = Markup.keywordN orelse s = Markup.keyword2N
then ("\\isakeyword{", "}")
else Markup.no_output;
--- a/src/Pure/Thy/thy_load.ML Sun Nov 25 18:50:13 2012 +0100
+++ b/src/Pure/Thy/thy_load.ML Sun Nov 25 19:49:24 2012 +0100
@@ -68,7 +68,7 @@
let
fun make_file file =
let
- val _ = Position.report pos (Isabelle_Markup.path (Path.implode file));
+ val _ = Position.report pos (Markup.path (Path.implode file));
val full_path = check_file dir file;
in {src_path = file, text = File.read full_path, pos = Path.position full_path} end;
val paths =
@@ -285,7 +285,7 @@
val _ =
if File.exists path then ()
else error ("Bad file: " ^ Path.print (Path.expand path) ^ Position.here pos);
- val _ = Position.report pos (Isabelle_Markup.path name);
+ val _ = Position.report pos (Markup.path name);
in Thy_Output.verb_text name end)));
--- a/src/Pure/Thy/thy_output.ML Sun Nov 25 18:50:13 2012 +0100
+++ b/src/Pure/Thy/thy_output.ML Sun Nov 25 19:49:24 2012 +0100
@@ -83,8 +83,8 @@
(Args.src -> Toplevel.state -> Proof.context -> string) Name_Space.table *
(string -> Proof.context -> Proof.context) Name_Space.table;
val empty : T =
- (Name_Space.empty_table Isabelle_Markup.document_antiquotationN,
- Name_Space.empty_table Isabelle_Markup.document_antiquotation_optionN);
+ (Name_Space.empty_table Markup.document_antiquotationN,
+ Name_Space.empty_table Markup.document_antiquotation_optionN);
val extend = I;
fun merge ((commands1, options1), (commands2, options2)) : T =
(Name_Space.merge_tables (commands1, commands2),
@@ -205,7 +205,7 @@
fun check_text (txt, pos) state =
- (Position.report pos Isabelle_Markup.doc_source;
+ (Position.report pos Markup.doc_source;
ignore (eval_antiquote (#1 (Keyword.get_lexicons ())) state (txt, pos)));
--- a/src/Pure/Thy/thy_syntax.ML Sun Nov 25 18:50:13 2012 +0100
+++ b/src/Pure/Thy/thy_syntax.ML Sun Nov 25 19:49:24 2012 +0100
@@ -38,29 +38,29 @@
local
val token_kind_markup =
- fn Token.Command => (Isabelle_Markup.command, "")
- | Token.Keyword => (Isabelle_Markup.keyword, "")
+ fn Token.Command => (Markup.command, "")
+ | Token.Keyword => (Markup.keyword, "")
| Token.Ident => (Markup.empty, "")
| Token.LongIdent => (Markup.empty, "")
| Token.SymIdent => (Markup.empty, "")
- | Token.Var => (Isabelle_Markup.var, "")
- | Token.TypeIdent => (Isabelle_Markup.tfree, "")
- | Token.TypeVar => (Isabelle_Markup.tvar, "")
+ | Token.Var => (Markup.var, "")
+ | Token.TypeIdent => (Markup.tfree, "")
+ | Token.TypeVar => (Markup.tvar, "")
| Token.Nat => (Markup.empty, "")
| Token.Float => (Markup.empty, "")
- | Token.String => (Isabelle_Markup.string, "")
- | Token.AltString => (Isabelle_Markup.altstring, "")
- | Token.Verbatim => (Isabelle_Markup.verbatim, "")
+ | Token.String => (Markup.string, "")
+ | Token.AltString => (Markup.altstring, "")
+ | Token.Verbatim => (Markup.verbatim, "")
| Token.Space => (Markup.empty, "")
- | Token.Comment => (Isabelle_Markup.comment, "")
+ | Token.Comment => (Markup.comment, "")
| Token.InternalValue => (Markup.empty, "")
- | Token.Error msg => (Isabelle_Markup.bad, msg)
- | Token.Sync => (Isabelle_Markup.control, "")
- | Token.EOF => (Isabelle_Markup.control, "");
+ | Token.Error msg => (Markup.bad, msg)
+ | Token.Sync => (Markup.control, "")
+ | Token.EOF => (Markup.control, "");
fun token_markup tok =
if Token.keyword_with (not o Lexicon.is_ascii_identifier) tok
- then (Isabelle_Markup.operator, "")
+ then (Markup.operator, "")
else
let
val kind = Token.kind_of tok;
@@ -77,7 +77,7 @@
Symbol_Pos.explode (Token.source_position_of tok)
|> map_filter (fn (sym, pos) =>
if Symbol.is_malformed sym
- then SOME ((pos, Isabelle_Markup.bad), "Malformed symbolic character") else NONE);
+ then SOME ((pos, Markup.bad), "Malformed symbolic character") else NONE);
val is_malformed = Token.is_error tok orelse not (null malformed_symbols);
val (markup, txt) = token_markup tok;
val reports = ((Token.position_of tok, markup), txt) :: malformed_symbols;
--- a/src/Pure/build-jars Sun Nov 25 18:50:13 2012 +0100
+++ b/src/Pure/build-jars Sun Nov 25 19:49:24 2012 +0100
@@ -32,7 +32,6 @@
Isar/token.scala
PIDE/command.scala
PIDE/document.scala
- PIDE/isabelle_markup.scala
PIDE/markup.scala
PIDE/markup_tree.scala
PIDE/protocol.scala
--- a/src/Pure/consts.ML Sun Nov 25 18:50:13 2012 +0100
+++ b/src/Pure/consts.ML Sun Nov 25 19:49:24 2012 +0100
@@ -311,7 +311,7 @@
(* empty and merge *)
val empty =
- make_consts (Name_Space.empty_table Isabelle_Markup.constantN, Symtab.empty, Symtab.empty);
+ make_consts (Name_Space.empty_table Markup.constantN, Symtab.empty, Symtab.empty);
fun merge
(Consts {decls = decls1, constraints = constraints1, rev_abbrevs = rev_abbrevs1},
--- a/src/Pure/global_theory.ML Sun Nov 25 18:50:13 2012 +0100
+++ b/src/Pure/global_theory.ML Sun Nov 25 19:49:24 2012 +0100
@@ -82,7 +82,7 @@
| SOME (static, ths) =>
(Context_Position.report_generic context pos (Name_Space.markup (Facts.space_of facts) name);
if static then ()
- else Context_Position.report_generic context pos (Isabelle_Markup.dynamic_fact name);
+ else Context_Position.report_generic context pos (Markup.dynamic_fact name);
Facts.select xthmref (map (Thm.transfer thy) ths)))
end;
--- a/src/Pure/goal.ML Sun Nov 25 18:50:13 2012 +0100
+++ b/src/Pure/goal.ML Sun Nov 25 19:49:24 2012 +0100
@@ -129,7 +129,7 @@
in (m, groups', tab') end);
fun status task markups =
- let val props = Markup.properties [(Isabelle_Markup.taskN, Task_Queue.str_of_task task)]
+ let val props = Markup.properties [(Markup.taskN, Task_Queue.str_of_task task)]
in Output.status (implode (map (Markup.markup_only o props) markups)) end;
in
@@ -148,21 +148,21 @@
(fn () =>
let
val task = the (Future.worker_task ());
- val _ = status task [Isabelle_Markup.running];
+ val _ = status task [Markup.running];
val result = Exn.capture (Future.interruptible_task e) ();
- val _ = status task [Isabelle_Markup.finished, Isabelle_Markup.joined];
+ val _ = status task [Markup.finished, Markup.joined];
val _ =
(case result of
Exn.Res _ => ()
| Exn.Exn exn =>
if id = 0 orelse Exn.is_interrupt exn then ()
else
- (status task [Isabelle_Markup.failed];
- Output.report (Markup.markup_only Isabelle_Markup.bad);
+ (status task [Markup.failed];
+ Output.report (Markup.markup_only Markup.bad);
Output.error_msg (ML_Compiler.exn_message exn)));
val _ = count_forked ~1;
in Exn.release result end);
- val _ = status (Future.task_of future) [Isabelle_Markup.forked];
+ val _ = status (Future.task_of future) [Markup.forked];
val _ = register_forked id future;
in future end) ();
--- a/src/Pure/goal_display.ML Sun Nov 25 18:50:13 2012 +0100
+++ b/src/Pure/goal_display.ML Sun Nov 25 19:49:24 2012 +0100
@@ -116,8 +116,7 @@
| pretty_list name prt lst = [Pretty.big_list name (map prt lst)];
fun pretty_subgoal (n, A) =
- Pretty.markup Isabelle_Markup.subgoal
- [Pretty.str (" " ^ string_of_int n ^ ". "), prt_term A];
+ Pretty.markup Markup.subgoal [Pretty.str (" " ^ string_of_int n ^ ". "), prt_term A];
fun pretty_subgoals As = map pretty_subgoal (1 upto length As ~~ As);
val pretty_ffpairs = pretty_list "flex-flex pairs:" (pretty_flexpair ctxt);
--- a/src/Pure/theory.ML Sun Nov 25 18:50:13 2012 +0100
+++ b/src/Pure/theory.ML Sun Nov 25 19:49:24 2012 +0100
@@ -133,7 +133,7 @@
if id = 0 then Markup.empty
else
Markup.properties (Position.entity_properties_of def id pos)
- (Isabelle_Markup.entity Isabelle_Markup.theoryN name);
+ (Markup.entity Markup.theoryN name);
fun init_markup (name, pos) thy =
let
--- a/src/Pure/type.ML Sun Nov 25 18:50:13 2012 +0100
+++ b/src/Pure/type.ML Sun Nov 25 19:49:24 2012 +0100
@@ -187,8 +187,8 @@
build_tsig (f (classes, default, types));
val empty_tsig =
- build_tsig ((Name_Space.empty Isabelle_Markup.classN, Sorts.empty_algebra), [],
- Name_Space.empty_table Isabelle_Markup.type_nameN);
+ build_tsig ((Name_Space.empty Markup.classN, Sorts.empty_algebra), [],
+ Name_Space.empty_table Markup.type_nameN);
(* classes and sorts *)
--- a/src/Pure/variable.ML Sun Nov 25 18:50:13 2012 +0100
+++ b/src/Pure/variable.ML Sun Nov 25 19:49:24 2012 +0100
@@ -81,7 +81,7 @@
(** local context data **)
type fixes = string Name_Space.table;
-val empty_fixes: fixes = Name_Space.empty_table Isabelle_Markup.fixedN;
+val empty_fixes: fixes = Name_Space.empty_table Markup.fixedN;
datatype data = Data of
{is_body: bool, (*inner body mode*)
--- a/src/Tools/jEdit/src/graphview_dockable.scala Sun Nov 25 18:50:13 2012 +0100
+++ b/src/Tools/jEdit/src/graphview_dockable.scala Sun Nov 25 19:49:24 2012 +0100
@@ -81,9 +81,9 @@
val new_graph =
if (!restriction.isDefined || restriction.get.contains(new_state.command)) {
new_state.markup.cumulate[Option[XML.Body]](
- new_state.command.range, None, Some(Set(Isabelle_Markup.GRAPHVIEW)),
+ new_state.command.range, None, Some(Set(Markup.GRAPHVIEW)),
{
- case (_, Text.Info(_, XML.Elem(Markup(Isabelle_Markup.GRAPHVIEW, _), graph))) =>
+ case (_, Text.Info(_, XML.Elem(Markup(Markup.GRAPHVIEW, _), graph))) =>
Some(graph)
}).filter(_.info.isDefined) match {
case Text.Info(_, Some(graph)) #:: _ => graph
--- a/src/Tools/jEdit/src/isabelle_rendering.scala Sun Nov 25 18:50:13 2012 +0100
+++ b/src/Tools/jEdit/src/isabelle_rendering.scala Sun Nov 25 19:49:24 2012 +0100
@@ -34,10 +34,10 @@
private val error_pri = 5
private val message_pri = Map(
- Isabelle_Markup.WRITELN -> writeln_pri, Isabelle_Markup.WRITELN_MESSAGE -> writeln_pri,
- Isabelle_Markup.TRACING -> tracing_pri, Isabelle_Markup.TRACING_MESSAGE -> tracing_pri,
- Isabelle_Markup.WARNING -> warning_pri, Isabelle_Markup.WARNING_MESSAGE -> warning_pri,
- Isabelle_Markup.ERROR -> error_pri, Isabelle_Markup.ERROR_MESSAGE -> error_pri)
+ Markup.WRITELN -> writeln_pri, Markup.WRITELN_MESSAGE -> writeln_pri,
+ Markup.TRACING -> tracing_pri, Markup.TRACING_MESSAGE -> tracing_pri,
+ Markup.WARNING -> warning_pri, Markup.WARNING_MESSAGE -> warning_pri,
+ Markup.ERROR -> error_pri, Markup.ERROR_MESSAGE -> error_pri)
/* icons */
@@ -156,10 +156,10 @@
val results =
snapshot.cumulate_markup[(Protocol.Status, Int)](
range, (Protocol.Status.init, 0),
- Some(Protocol.command_status_markup + Isabelle_Markup.WARNING + Isabelle_Markup.ERROR),
+ Some(Protocol.command_status_markup + Markup.WARNING + Markup.ERROR),
{
case ((status, pri), Text.Info(_, XML.Elem(markup, _))) =>
- if (markup.name == Isabelle_Markup.WARNING || markup.name == Isabelle_Markup.ERROR)
+ if (markup.name == Markup.WARNING || markup.name == Markup.ERROR)
(status, pri max Rendering.message_pri(markup.name))
else (Protocol.command_status(status, markup), pri)
})
@@ -183,11 +183,9 @@
/* markup selectors */
private val highlight_include =
- Set(Isabelle_Markup.SORT, Isabelle_Markup.TYP, Isabelle_Markup.TERM, Isabelle_Markup.PROP,
- Isabelle_Markup.ML_TYPING, Isabelle_Markup.TOKEN_RANGE, Isabelle_Markup.ENTITY,
- Isabelle_Markup.PATH, Isabelle_Markup.SORTING, Isabelle_Markup.TYPING, Isabelle_Markup.FREE,
- Isabelle_Markup.SKOLEM, Isabelle_Markup.BOUND, Isabelle_Markup.VAR, Isabelle_Markup.TFREE,
- Isabelle_Markup.TVAR, Isabelle_Markup.ML_SOURCE, Isabelle_Markup.DOCUMENT_SOURCE)
+ Set(Markup.SORT, Markup.TYP, Markup.TERM, Markup.PROP, Markup.ML_TYPING, Markup.TOKEN_RANGE,
+ Markup.ENTITY, Markup.PATH, Markup.SORTING, Markup.TYPING, Markup.FREE, Markup.SKOLEM,
+ Markup.BOUND, Markup.VAR, Markup.TFREE, Markup.TVAR, Markup.ML_SOURCE, Markup.DOCUMENT_SOURCE)
def highlight(range: Text.Range): Option[Text.Info[Color]] =
{
@@ -199,21 +197,21 @@
}
- private val hyperlink_include = Set(Isabelle_Markup.ENTITY, Isabelle_Markup.PATH)
+ private val hyperlink_include = Set(Markup.ENTITY, Markup.PATH)
def hyperlink(range: Text.Range): Option[Text.Info[Hyperlink]] =
{
snapshot.cumulate_markup[List[Text.Info[Hyperlink]]](range, Nil, Some(hyperlink_include),
{
- case (links, Text.Info(info_range, XML.Elem(Isabelle_Markup.Path(name), _)))
+ case (links, Text.Info(info_range, XML.Elem(Markup.Path(name), _)))
if Path.is_ok(name) =>
val jedit_file = Isabelle.thy_load.append(snapshot.node_name.dir, Path.explode(name))
Text.Info(snapshot.convert(info_range), Hyperlink(jedit_file, 0, 0)) :: links
- case (links, Text.Info(info_range, XML.Elem(Markup(Isabelle_Markup.ENTITY, props), _)))
+ case (links, Text.Info(info_range, XML.Elem(Markup(Markup.ENTITY, props), _)))
if !props.exists(
- { case (Markup.KIND, Isabelle_Markup.ML_OPEN) => true
- case (Markup.KIND, Isabelle_Markup.ML_STRUCT) => true
+ { case (Markup.KIND, Markup.ML_OPEN) => true
+ case (Markup.KIND, Markup.ML_STRUCT) => true
case _ => false }) =>
props match {
@@ -244,9 +242,9 @@
def sendback(range: Text.Range): Option[Text.Info[Option[Document.Exec_ID]]] =
- snapshot.select_markup(range, Some(Set(Isabelle_Markup.SENDBACK)),
+ snapshot.select_markup(range, Some(Set(Markup.SENDBACK)),
{
- case Text.Info(info_range, XML.Elem(Markup(Isabelle_Markup.SENDBACK, props), _)) =>
+ case Text.Info(info_range, XML.Elem(Markup(Markup.SENDBACK, props), _)) =>
Text.Info(snapshot.convert(info_range), Position.Id.unapply(props))
}) match { case Text.Info(_, info) #:: _ => Some(info) case _ => None }
@@ -255,16 +253,14 @@
{
val msgs =
snapshot.cumulate_markup[SortedMap[Long, XML.Tree]](range, SortedMap.empty,
- Some(Set(Isabelle_Markup.WRITELN, Isabelle_Markup.WARNING, Isabelle_Markup.ERROR,
- Isabelle_Markup.BAD)),
+ Some(Set(Markup.WRITELN, Markup.WARNING, Markup.ERROR, Markup.BAD)),
{
- case (msgs, Text.Info(_,
- XML.Elem(Markup(name, props @ Isabelle_Markup.Serial(serial)), body)))
- if name == Isabelle_Markup.WRITELN ||
- name == Isabelle_Markup.WARNING ||
- name == Isabelle_Markup.ERROR =>
- msgs + (serial -> XML.Elem(Markup(Isabelle_Markup.message(name), props), body))
- case (msgs, Text.Info(_, msg @ XML.Elem(Markup(Isabelle_Markup.BAD, _), body)))
+ case (msgs, Text.Info(_, XML.Elem(Markup(name, props @ Markup.Serial(serial)), body)))
+ if name == Markup.WRITELN ||
+ name == Markup.WARNING ||
+ name == Markup.ERROR =>
+ msgs + (serial -> XML.Elem(Markup(Markup.message(name), props), body))
+ case (msgs, Text.Info(_, msg @ XML.Elem(Markup(Markup.BAD, _), body)))
if !body.isEmpty => msgs + (Document.new_id() -> msg)
}).toList.flatMap(_.info)
Pretty.separate(msgs.iterator.map(_._2).toList)
@@ -273,23 +269,23 @@
private val tooltips: Map[String, String] =
Map(
- Isabelle_Markup.SORT -> "sort",
- Isabelle_Markup.TYP -> "type",
- Isabelle_Markup.TERM -> "term",
- Isabelle_Markup.PROP -> "proposition",
- Isabelle_Markup.TOKEN_RANGE -> "inner syntax token",
- Isabelle_Markup.FREE -> "free variable",
- Isabelle_Markup.SKOLEM -> "skolem variable",
- Isabelle_Markup.BOUND -> "bound variable",
- Isabelle_Markup.VAR -> "schematic variable",
- Isabelle_Markup.TFREE -> "free type variable",
- Isabelle_Markup.TVAR -> "schematic type variable",
- Isabelle_Markup.ML_SOURCE -> "ML source",
- Isabelle_Markup.DOCUMENT_SOURCE -> "document source")
+ 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")
private val tooltip_elements =
- Set(Isabelle_Markup.ENTITY, Isabelle_Markup.SORTING, Isabelle_Markup.TYPING,
- Isabelle_Markup.ML_TYPING, Isabelle_Markup.PATH) ++ tooltips.keys
+ Set(Markup.ENTITY, Markup.SORTING, Markup.TYPING, Markup.ML_TYPING, Markup.PATH) ++
+ tooltips.keys
private def pretty_typing(kind: String, body: XML.Body): XML.Tree =
Pretty.block(XML.Text(kind) :: Pretty.Break(1) :: body)
@@ -303,17 +299,17 @@
snapshot.cumulate_markup[Text.Info[(List[(Boolean, XML.Tree)])]](
range, Text.Info(range, Nil), Some(tooltip_elements),
{
- case (prev, Text.Info(r, XML.Elem(Isabelle_Markup.Entity(kind, name), _))) =>
+ case (prev, Text.Info(r, XML.Elem(Markup.Entity(kind, name), _))) =>
val kind1 = space_explode('_', kind).mkString(" ")
add(prev, r, (true, XML.Text(kind1 + " " + quote(name))))
- case (prev, Text.Info(r, XML.Elem(Isabelle_Markup.Path(name), _)))
+ case (prev, Text.Info(r, XML.Elem(Markup.Path(name), _)))
if Path.is_ok(name) =>
val jedit_file = Isabelle.thy_load.append(snapshot.node_name.dir, Path.explode(name))
add(prev, r, (true, XML.Text("file " + quote(jedit_file))))
case (prev, Text.Info(r, XML.Elem(Markup(name, _), body)))
- if name == Isabelle_Markup.SORTING || name == Isabelle_Markup.TYPING =>
+ if name == Markup.SORTING || name == Markup.TYPING =>
add(prev, r, (true, pretty_typing("::", body)))
- case (prev, Text.Info(r, XML.Elem(Markup(Isabelle_Markup.ML_TYPING, _), body))) =>
+ case (prev, Text.Info(r, XML.Elem(Markup(Markup.ML_TYPING, _), body))) =>
add(prev, r, (false, pretty_typing("ML:", body)))
case (prev, Text.Info(r, XML.Elem(Markup(name, _), _)))
if tooltips.isDefinedAt(name) => add(prev, r, (true, XML.Text(tooltips(name))))
@@ -328,16 +324,15 @@
def gutter_message(range: Text.Range): Option[Icon] =
{
val results =
- snapshot.cumulate_markup[Int](range, 0,
- Some(Set(Isabelle_Markup.WARNING, Isabelle_Markup.ERROR)),
+ snapshot.cumulate_markup[Int](range, 0, Some(Set(Markup.WARNING, Markup.ERROR)),
{
- case (pri, Text.Info(_, XML.Elem(Markup(Isabelle_Markup.WARNING, _), body))) =>
+ case (pri, Text.Info(_, XML.Elem(Markup(Markup.WARNING, _), body))) =>
body match {
- case List(XML.Elem(Markup(Isabelle_Markup.LEGACY, _), _)) =>
+ case List(XML.Elem(Markup(Markup.LEGACY, _), _)) =>
pri max Rendering.legacy_pri
case _ => pri max Rendering.warning_pri
}
- case (pri, Text.Info(_, XML.Elem(Markup(Isabelle_Markup.ERROR, _), _))) =>
+ case (pri, Text.Info(_, XML.Elem(Markup(Markup.ERROR, _), _))) =>
pri max Rendering.error_pri
})
val pri = (0 /: results) { case (p1, Text.Info(_, p2)) => p1 max p2 }
@@ -354,12 +349,12 @@
{
val results =
snapshot.cumulate_markup[Int](range, 0,
- Some(Set(Isabelle_Markup.WRITELN, Isabelle_Markup.WARNING, Isabelle_Markup.ERROR)),
+ Some(Set(Markup.WRITELN, Markup.WARNING, Markup.ERROR)),
{
case (pri, Text.Info(_, XML.Elem(Markup(name, _), _)))
- if name == Isabelle_Markup.WRITELN ||
- name == Isabelle_Markup.WARNING ||
- name == Isabelle_Markup.ERROR => pri max Rendering.message_pri(name)
+ if name == Markup.WRITELN ||
+ name == Markup.WARNING ||
+ name == Markup.ERROR => pri max Rendering.message_pri(name)
})
for {
Text.Info(r, pri) <- results
@@ -369,8 +364,7 @@
private val messages_include =
- Set(Isabelle_Markup.WRITELN_MESSAGE, Isabelle_Markup.TRACING_MESSAGE,
- Isabelle_Markup.WARNING_MESSAGE, Isabelle_Markup.ERROR_MESSAGE)
+ Set(Markup.WRITELN_MESSAGE, Markup.TRACING_MESSAGE, Markup.WARNING_MESSAGE, Markup.ERROR_MESSAGE)
private val message_colors = Map(
Rendering.writeln_pri -> writeln_message_color,
@@ -384,17 +378,17 @@
snapshot.cumulate_markup[Int](range, 0, Some(messages_include),
{
case (pri, Text.Info(_, XML.Elem(Markup(name, _), _)))
- if name == Isabelle_Markup.WRITELN_MESSAGE ||
- name == Isabelle_Markup.TRACING_MESSAGE ||
- name == Isabelle_Markup.WARNING_MESSAGE ||
- name == Isabelle_Markup.ERROR_MESSAGE => pri max Rendering.message_pri(name)
+ if name == Markup.WRITELN_MESSAGE ||
+ name == Markup.TRACING_MESSAGE ||
+ name == Markup.WARNING_MESSAGE ||
+ name == Markup.ERROR_MESSAGE => pri max Rendering.message_pri(name)
})
val pri = (0 /: results) { case (p1, Text.Info(_, p2)) => p1 max p2 }
val is_separator = pri > 0 &&
- snapshot.cumulate_markup[Boolean](range, false, Some(Set(Isabelle_Markup.SEPARATOR)),
+ snapshot.cumulate_markup[Boolean](range, false, Some(Set(Markup.SEPARATOR)),
{
- case (_, Text.Info(_, XML.Elem(Markup(Isabelle_Markup.SEPARATOR, _), _))) => true
+ case (_, Text.Info(_, XML.Elem(Markup(Markup.SEPARATOR, _), _))) => true
}).exists(_.info)
message_colors.get(pri).map((_, is_separator))
@@ -402,10 +396,9 @@
private val background1_include =
- Protocol.command_status_markup + Isabelle_Markup.WRITELN_MESSAGE +
- Isabelle_Markup.TRACING_MESSAGE + Isabelle_Markup.WARNING_MESSAGE +
- Isabelle_Markup.ERROR_MESSAGE + Isabelle_Markup.BAD + Isabelle_Markup.INTENSIFY +
- Isabelle_Markup.SENDBACK
+ Protocol.command_status_markup + Markup.WRITELN_MESSAGE + Markup.TRACING_MESSAGE +
+ Markup.WARNING_MESSAGE + Markup.ERROR_MESSAGE + Markup.BAD + Markup.INTENSIFY +
+ Markup.SENDBACK
def background1(range: Text.Range): Stream[Text.Info[Color]] =
{
@@ -419,11 +412,11 @@
case (((Some(status), color), Text.Info(_, XML.Elem(markup, _))))
if (Protocol.command_status_markup(markup.name)) =>
(Some(Protocol.command_status(status, markup)), color)
- case (_, Text.Info(_, XML.Elem(Markup(Isabelle_Markup.BAD, _), _))) =>
+ case (_, Text.Info(_, XML.Elem(Markup(Markup.BAD, _), _))) =>
(None, Some(bad_color))
- case (_, Text.Info(_, XML.Elem(Markup(Isabelle_Markup.INTENSIFY, _), _))) =>
+ case (_, Text.Info(_, XML.Elem(Markup(Markup.INTENSIFY, _), _))) =>
(None, Some(intensify_color))
- case (_, Text.Info(_, XML.Elem(Markup(Isabelle_Markup.SENDBACK, _), _))) =>
+ case (_, Text.Info(_, XML.Elem(Markup(Markup.SENDBACK, _), _))) =>
(None, Some(sendback_color))
})
color <-
@@ -439,47 +432,45 @@
def background2(range: Text.Range): Stream[Text.Info[Color]] =
- snapshot.select_markup(range,
- Some(Set(Isabelle_Markup.TOKEN_RANGE)),
+ snapshot.select_markup(range, Some(Set(Markup.TOKEN_RANGE)),
{
- case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.TOKEN_RANGE, _), _)) => light_color
+ case Text.Info(_, XML.Elem(Markup(Markup.TOKEN_RANGE, _), _)) => light_color
})
def foreground(range: Text.Range): Stream[Text.Info[Color]] =
- snapshot.select_markup(range,
- Some(Set(Isabelle_Markup.STRING, Isabelle_Markup.ALTSTRING, Isabelle_Markup.VERBATIM)),
+ snapshot.select_markup(range, Some(Set(Markup.STRING, Markup.ALTSTRING, Markup.VERBATIM)),
{
- case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.STRING, _), _)) => quoted_color
- case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.ALTSTRING, _), _)) => quoted_color
- case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.VERBATIM, _), _)) => quoted_color
+ case Text.Info(_, XML.Elem(Markup(Markup.STRING, _), _)) => quoted_color
+ case Text.Info(_, XML.Elem(Markup(Markup.ALTSTRING, _), _)) => quoted_color
+ case Text.Info(_, XML.Elem(Markup(Markup.VERBATIM, _), _)) => quoted_color
})
private val text_colors: Map[String, Color] = Map(
- Isabelle_Markup.KEYWORD1 -> keyword1_color,
- Isabelle_Markup.KEYWORD2 -> keyword2_color,
- Isabelle_Markup.STRING -> Color.BLACK,
- Isabelle_Markup.ALTSTRING -> Color.BLACK,
- Isabelle_Markup.VERBATIM -> Color.BLACK,
- Isabelle_Markup.LITERAL -> keyword1_color,
- Isabelle_Markup.DELIMITER -> Color.BLACK,
- Isabelle_Markup.TFREE -> tfree_color,
- Isabelle_Markup.TVAR -> tvar_color,
- Isabelle_Markup.FREE -> free_color,
- Isabelle_Markup.SKOLEM -> skolem_color,
- Isabelle_Markup.BOUND -> bound_color,
- Isabelle_Markup.VAR -> var_color,
- Isabelle_Markup.INNER_STRING -> inner_quoted_color,
- Isabelle_Markup.INNER_COMMENT -> inner_comment_color,
- Isabelle_Markup.DYNAMIC_FACT -> dynamic_color,
- Isabelle_Markup.ML_KEYWORD -> keyword1_color,
- Isabelle_Markup.ML_DELIMITER -> Color.BLACK,
- Isabelle_Markup.ML_NUMERAL -> inner_numeral_color,
- Isabelle_Markup.ML_CHAR -> inner_quoted_color,
- Isabelle_Markup.ML_STRING -> inner_quoted_color,
- Isabelle_Markup.ML_COMMENT -> inner_comment_color,
- Isabelle_Markup.ANTIQ -> antiquotation_color)
+ Markup.KEYWORD1 -> keyword1_color,
+ Markup.KEYWORD2 -> keyword2_color,
+ Markup.STRING -> Color.BLACK,
+ Markup.ALTSTRING -> Color.BLACK,
+ Markup.VERBATIM -> Color.BLACK,
+ Markup.LITERAL -> keyword1_color,
+ Markup.DELIMITER -> Color.BLACK,
+ Markup.TFREE -> tfree_color,
+ Markup.TVAR -> tvar_color,
+ Markup.FREE -> free_color,
+ Markup.SKOLEM -> skolem_color,
+ Markup.BOUND -> bound_color,
+ Markup.VAR -> var_color,
+ Markup.INNER_STRING -> inner_quoted_color,
+ Markup.INNER_COMMENT -> inner_comment_color,
+ Markup.DYNAMIC_FACT -> dynamic_color,
+ Markup.ML_KEYWORD -> keyword1_color,
+ Markup.ML_DELIMITER -> Color.BLACK,
+ Markup.ML_NUMERAL -> inner_numeral_color,
+ Markup.ML_CHAR -> inner_quoted_color,
+ Markup.ML_STRING -> inner_quoted_color,
+ Markup.ML_COMMENT -> inner_comment_color,
+ Markup.ANTIQ -> antiquotation_color)
private val text_color_elements = Set.empty[String] ++ text_colors.keys
--- a/src/Tools/quickcheck.ML Sun Nov 25 18:50:13 2012 +0100
+++ b/src/Tools/quickcheck.ML Sun Nov 25 19:49:24 2012 +0100
@@ -529,7 +529,7 @@
state
|> (if auto then
Proof.goal_message (K (Pretty.chunks [Pretty.str "",
- Pretty.mark Isabelle_Markup.intensify msg]))
+ Pretty.mark Markup.intensify msg]))
else
tap (fn _ => Output.urgent_message (Pretty.string_of msg))))
else
--- a/src/Tools/solve_direct.ML Sun Nov 25 18:50:13 2012 +0100
+++ b/src/Tools/solve_direct.ML Sun Nov 25 19:49:24 2012 +0100
@@ -89,7 +89,7 @@
Proof.goal_message
(fn () =>
Pretty.chunks
- [Pretty.str "", Pretty.markup Isabelle_Markup.intensify (message results)])
+ [Pretty.str "", Pretty.markup Markup.intensify (message results)])
else
tap (fn _ =>
Output.urgent_message (Pretty.string_of (Pretty.chunks (message results))))))