# HG changeset patch # User wenzelm # Date 1353869364 -3600 # Node ID c26369c9eda677e64578dac994ffe6608ee07e91 # Parent 2c94c065564ecbaf8acb640ec953764c8877e364 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d; diff -r 2c94c065564e -r c26369c9eda6 src/Doc/antiquote_setup.ML --- 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; diff -r 2c94c065564e -r c26369c9eda6 src/HOL/Tools/Nitpick/nitpick.ML --- 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 diff -r 2c94c065564e -r c26369c9eda6 src/HOL/Tools/Sledgehammer/sledgehammer_run.ML --- 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 diff -r 2c94c065564e -r c26369c9eda6 src/HOL/Tools/try0.ML --- 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)))) diff -r 2c94c065564e -r c26369c9eda6 src/Pure/General/antiquote.ML --- 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 *) diff -r 2c94c065564e -r c26369c9eda6 src/Pure/General/binding.ML --- 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; diff -r 2c94c065564e -r c26369c9eda6 src/Pure/General/graph_display.ML --- 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 diff -r 2c94c065564e -r c26369c9eda6 src/Pure/General/name_space.ML --- 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); diff -r 2c94c065564e -r c26369c9eda6 src/Pure/General/path.ML --- 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; diff -r 2c94c065564e -r c26369c9eda6 src/Pure/General/position.ML --- 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; diff -r 2c94c065564e -r c26369c9eda6 src/Pure/General/position.scala --- 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 */ diff -r 2c94c065564e -r c26369c9eda6 src/Pure/General/pretty.ML --- 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; diff -r 2c94c065564e -r c26369c9eda6 src/Pure/General/pretty.scala --- 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 diff -r 2c94c065564e -r c26369c9eda6 src/Pure/General/symbol_pos.ML --- 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; diff -r 2c94c065564e -r c26369c9eda6 src/Pure/Isar/obtain.ML --- 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]] = diff -r 2c94c065564e -r c26369c9eda6 src/Pure/Isar/outer_syntax.ML --- 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 *) diff -r 2c94c065564e -r c26369c9eda6 src/Pure/Isar/proof.ML --- 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) diff -r 2c94c065564e -r c26369c9eda6 src/Pure/Isar/proof_context.ML --- 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 = diff -r 2c94c065564e -r c26369c9eda6 src/Pure/Isar/runtime.ML --- 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 diff -r 2c94c065564e -r c26369c9eda6 src/Pure/Isar/token.ML --- 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); diff -r 2c94c065564e -r c26369c9eda6 src/Pure/Isar/toplevel.ML --- 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 (""); diff -r 2c94c065564e -r c26369c9eda6 src/Pure/ML/ml_compiler_polyml.ML --- 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 diff -r 2c94c065564e -r c26369c9eda6 src/Pure/ML/ml_context.ML --- 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 *) diff -r 2c94c065564e -r c26369c9eda6 src/Pure/ML/ml_lex.ML --- 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 [] diff -r 2c94c065564e -r c26369c9eda6 src/Pure/PIDE/command.ML --- 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 diff -r 2c94c065564e -r c26369c9eda6 src/Pure/PIDE/command.scala --- 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)) diff -r 2c94c065564e -r c26369c9eda6 src/Pure/PIDE/document.ML --- 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; diff -r 2c94c065564e -r c26369c9eda6 src/Pure/PIDE/isabelle_markup.ML --- 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; diff -r 2c94c065564e -r c26369c9eda6 src/Pure/PIDE/isabelle_markup.scala --- 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 - } - } -} - diff -r 2c94c065564e -r c26369c9eda6 src/Pure/PIDE/markup.ML --- 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 **) diff -r 2c94c065564e -r c26369c9eda6 src/Pure/PIDE/markup.scala --- 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 + } + } } diff -r 2c94c065564e -r c26369c9eda6 src/Pure/PIDE/protocol.ML --- 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 _ = diff -r 2c94c065564e -r c26369c9eda6 src/Pure/PIDE/protocol.scala --- 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] = { diff -r 2c94c065564e -r c26369c9eda6 src/Pure/PIDE/sendback.ML --- 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; diff -r 2c94c065564e -r c26369c9eda6 src/Pure/ProofGeneral/proof_general_emacs.ML --- 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 diff -r 2c94c065564e -r c26369c9eda6 src/Pure/ProofGeneral/proof_general_pgip.ML --- 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; diff -r 2c94c065564e -r c26369c9eda6 src/Pure/ROOT --- 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" diff -r 2c94c065564e -r c26369c9eda6 src/Pure/ROOT.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"; diff -r 2c94c065564e -r c26369c9eda6 src/Pure/Syntax/lexicon.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 ""; diff -r 2c94c065564e -r c26369c9eda6 src/Pure/Syntax/syntax.ML --- 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; diff -r 2c94c065564e -r c26369c9eda6 src/Pure/Syntax/syntax_phases.ML --- 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; diff -r 2c94c065564e -r c26369c9eda6 src/Pure/Syntax/term_position.ML --- 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); diff -r 2c94c065564e -r c26369c9eda6 src/Pure/System/invoke_scala.ML --- 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); diff -r 2c94c065564e -r c26369c9eda6 src/Pure/System/isabelle_process.ML --- 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; diff -r 2c94c065564e -r c26369c9eda6 src/Pure/System/isabelle_process.scala --- 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) diff -r 2c94c065564e -r c26369c9eda6 src/Pure/System/session.scala --- 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 diff -r 2c94c065564e -r c26369c9eda6 src/Pure/Thy/html.ML --- 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 diff -r 2c94c065564e -r c26369c9eda6 src/Pure/Thy/html.scala --- 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))) diff -r 2c94c065564e -r c26369c9eda6 src/Pure/Thy/latex.ML --- 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; diff -r 2c94c065564e -r c26369c9eda6 src/Pure/Thy/thy_load.ML --- 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))); diff -r 2c94c065564e -r c26369c9eda6 src/Pure/Thy/thy_output.ML --- 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))); diff -r 2c94c065564e -r c26369c9eda6 src/Pure/Thy/thy_syntax.ML --- 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; diff -r 2c94c065564e -r c26369c9eda6 src/Pure/build-jars --- 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 diff -r 2c94c065564e -r c26369c9eda6 src/Pure/consts.ML --- 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}, diff -r 2c94c065564e -r c26369c9eda6 src/Pure/global_theory.ML --- 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; diff -r 2c94c065564e -r c26369c9eda6 src/Pure/goal.ML --- 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) (); diff -r 2c94c065564e -r c26369c9eda6 src/Pure/goal_display.ML --- 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); diff -r 2c94c065564e -r c26369c9eda6 src/Pure/theory.ML --- 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 diff -r 2c94c065564e -r c26369c9eda6 src/Pure/type.ML --- 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 *) diff -r 2c94c065564e -r c26369c9eda6 src/Pure/variable.ML --- 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*) diff -r 2c94c065564e -r c26369c9eda6 src/Tools/jEdit/src/graphview_dockable.scala --- 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 diff -r 2c94c065564e -r c26369c9eda6 src/Tools/jEdit/src/isabelle_rendering.scala --- 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 diff -r 2c94c065564e -r c26369c9eda6 src/Tools/quickcheck.ML --- 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 diff -r 2c94c065564e -r c26369c9eda6 src/Tools/solve_direct.ML --- 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))))))