Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
authorwenzelm
Sun Nov 25 19:49:24 2012 +0100 (2012-11-25 ago)
changeset 50201c26369c9eda6
parent 50200 2c94c065564e
child 50202 ec0f2f8dbeb9
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
src/Doc/antiquote_setup.ML
src/HOL/Tools/Nitpick/nitpick.ML
src/HOL/Tools/Sledgehammer/sledgehammer_run.ML
src/HOL/Tools/try0.ML
src/Pure/General/antiquote.ML
src/Pure/General/binding.ML
src/Pure/General/graph_display.ML
src/Pure/General/name_space.ML
src/Pure/General/path.ML
src/Pure/General/position.ML
src/Pure/General/position.scala
src/Pure/General/pretty.ML
src/Pure/General/pretty.scala
src/Pure/General/symbol_pos.ML
src/Pure/Isar/obtain.ML
src/Pure/Isar/outer_syntax.ML
src/Pure/Isar/proof.ML
src/Pure/Isar/proof_context.ML
src/Pure/Isar/runtime.ML
src/Pure/Isar/token.ML
src/Pure/Isar/toplevel.ML
src/Pure/ML/ml_compiler_polyml.ML
src/Pure/ML/ml_context.ML
src/Pure/ML/ml_lex.ML
src/Pure/PIDE/command.ML
src/Pure/PIDE/command.scala
src/Pure/PIDE/document.ML
src/Pure/PIDE/isabelle_markup.ML
src/Pure/PIDE/isabelle_markup.scala
src/Pure/PIDE/markup.ML
src/Pure/PIDE/markup.scala
src/Pure/PIDE/protocol.ML
src/Pure/PIDE/protocol.scala
src/Pure/PIDE/sendback.ML
src/Pure/ProofGeneral/proof_general_emacs.ML
src/Pure/ProofGeneral/proof_general_pgip.ML
src/Pure/ROOT
src/Pure/ROOT.ML
src/Pure/Syntax/lexicon.ML
src/Pure/Syntax/syntax.ML
src/Pure/Syntax/syntax_phases.ML
src/Pure/Syntax/term_position.ML
src/Pure/System/invoke_scala.ML
src/Pure/System/isabelle_process.ML
src/Pure/System/isabelle_process.scala
src/Pure/System/session.scala
src/Pure/Thy/html.ML
src/Pure/Thy/html.scala
src/Pure/Thy/latex.ML
src/Pure/Thy/thy_load.ML
src/Pure/Thy/thy_output.ML
src/Pure/Thy/thy_syntax.ML
src/Pure/build-jars
src/Pure/consts.ML
src/Pure/global_theory.ML
src/Pure/goal.ML
src/Pure/goal_display.ML
src/Pure/theory.ML
src/Pure/type.ML
src/Pure/variable.ML
src/Tools/jEdit/src/graphview_dockable.scala
src/Tools/jEdit/src/isabelle_rendering.scala
src/Tools/quickcheck.ML
src/Tools/solve_direct.ML
     1.1 --- a/src/Doc/antiquote_setup.ML	Sun Nov 25 18:50:13 2012 +0100
     1.2 +++ b/src/Doc/antiquote_setup.ML	Sun Nov 25 19:49:24 2012 +0100
     1.3 @@ -210,7 +210,7 @@
     1.4    entity_antiqs no_check "isatt" "executable" #>
     1.5    entity_antiqs (K check_tool) "isatool" "tool" #>
     1.6    entity_antiqs (thy_check ML_Context.intern_antiq ML_Context.defined_antiq)
     1.7 -    "" Isabelle_Markup.ML_antiquotationN;
     1.8 +    "" Markup.ML_antiquotationN;
     1.9  
    1.10  end;
    1.11  
     2.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML	Sun Nov 25 18:50:13 2012 +0100
     2.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML	Sun Nov 25 19:49:24 2012 +0100
     2.3 @@ -245,7 +245,7 @@
     2.4        if mode = Auto_Try then
     2.5          Unsynchronized.change state_ref o Proof.goal_message o K
     2.6          o Pretty.chunks o cons (Pretty.str "") o single
     2.7 -        o Pretty.mark Isabelle_Markup.intensify
     2.8 +        o Pretty.mark Markup.intensify
     2.9        else
    2.10          print o Pretty.string_of
    2.11      val pprint_a = pprint Output.urgent_message
     3.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Sun Nov 25 18:50:13 2012 +0100
     3.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Sun Nov 25 19:49:24 2012 +0100
     3.3 @@ -137,7 +137,7 @@
     3.4           |> outcome_code = someN
     3.5              ? Proof.goal_message (fn () =>
     3.6                    [Pretty.str "",
     3.7 -                   Pretty.mark Isabelle_Markup.intensify (Pretty.str (message ()))]
     3.8 +                   Pretty.mark Markup.intensify (Pretty.str (message ()))]
     3.9                    |> Pretty.chunks))
    3.10        end
    3.11      else if blocking then
     4.1 --- a/src/HOL/Tools/try0.ML	Sun Nov 25 18:50:13 2012 +0100
     4.2 +++ b/src/HOL/Tools/try0.ML	Sun Nov 25 19:49:24 2012 +0100
     4.3 @@ -146,7 +146,7 @@
     4.4          (true, (s, st |> (if mode = Auto_Try then
     4.5                              Proof.goal_message
     4.6                                  (fn () => Pretty.chunks [Pretty.str "",
     4.7 -                                          Pretty.markup Isabelle_Markup.intensify
     4.8 +                                          Pretty.markup Markup.intensify
     4.9                                                          [Pretty.str message]])
    4.10                            else
    4.11                              tap (fn _ => Output.urgent_message message))))
     5.1 --- a/src/Pure/General/antiquote.ML	Sun Nov 25 18:50:13 2012 +0100
     5.2 +++ b/src/Pure/General/antiquote.ML	Sun Nov 25 19:49:24 2012 +0100
     5.3 @@ -41,9 +41,9 @@
     5.4  fun reports_of text =
     5.5    maps
     5.6      (fn Text x => text x
     5.7 -      | Antiq (_, (pos, _)) => [((pos, Isabelle_Markup.antiq), "")]
     5.8 -      | Open pos => [((pos, Isabelle_Markup.antiq), "")]
     5.9 -      | Close pos => [((pos, Isabelle_Markup.antiq), "")]);
    5.10 +      | Antiq (_, (pos, _)) => [((pos, Markup.antiq), "")]
    5.11 +      | Open pos => [((pos, Markup.antiq), "")]
    5.12 +      | Close pos => [((pos, Markup.antiq), "")]);
    5.13  
    5.14  
    5.15  (* check_nesting *)
     6.1 --- a/src/Pure/General/binding.ML	Sun Nov 25 18:50:13 2012 +0100
     6.2 +++ b/src/Pure/General/binding.ML	Sun Nov 25 19:49:24 2012 +0100
     6.3 @@ -124,7 +124,7 @@
     6.4  fun pretty (Binding {prefix, qualifier, name, pos, ...}) =
     6.5    if name = "" then Pretty.str "\"\""
     6.6    else
     6.7 -    Pretty.markup (Position.markup pos Isabelle_Markup.binding)
     6.8 +    Pretty.markup (Position.markup pos Markup.binding)
     6.9        [Pretty.str (Long_Name.implode (map #1 (prefix @ qualifier) @ [name]))]
    6.10      |> Pretty.quote;
    6.11  
     7.1 --- a/src/Pure/General/graph_display.ML	Sun Nov 25 18:50:13 2012 +0100
     7.2 +++ b/src/Pure/General/graph_display.ML	Sun Nov 25 19:49:24 2012 +0100
     7.3 @@ -58,7 +58,7 @@
     7.4  fun display_graph graph =
     7.5    if print_mode_active graphview_reportN then
     7.6      (Output.report
     7.7 -      (YXML.string_of (XML.Elem ((Isabelle_Markup.graphviewN, []), encode_graphview graph)));
     7.8 +      (YXML.string_of (XML.Elem ((Markup.graphviewN, []), encode_graphview graph)));
     7.9        writeln "(see graphview)")
    7.10    else
    7.11      let
     8.1 --- a/src/Pure/General/name_space.ML	Sun Nov 25 18:50:13 2012 +0100
     8.2 +++ b/src/Pure/General/name_space.ML	Sun Nov 25 19:49:24 2012 +0100
     8.3 @@ -88,7 +88,7 @@
     8.4    id: serial};
     8.5  
     8.6  fun entry_markup def kind (name, {pos, id, ...}: entry) =
     8.7 -  Markup.properties (Position.entity_properties_of def id pos) (Isabelle_Markup.entity kind name);
     8.8 +  Markup.properties (Position.entity_properties_of def id pos) (Markup.entity kind name);
     8.9  
    8.10  fun print_entry_ref kind (name, entry) =
    8.11    quote (Markup.markup (entry_markup false kind (name, entry)) name);
    8.12 @@ -133,7 +133,7 @@
    8.13  
    8.14  fun markup (Name_Space {kind, entries, ...}) name =
    8.15    (case Symtab.lookup entries name of
    8.16 -    NONE => Isabelle_Markup.intensify
    8.17 +    NONE => Markup.intensify
    8.18    | SOME (_, entry) => entry_markup false kind (name, entry));
    8.19  
    8.20  fun is_concealed space name = #concealed (the_entry space name);
     9.1 --- a/src/Pure/General/path.ML	Sun Nov 25 18:50:13 2012 +0100
     9.2 +++ b/src/Pure/General/path.ML	Sun Nov 25 19:49:24 2012 +0100
     9.3 @@ -155,7 +155,7 @@
     9.4  
     9.5  fun pretty path =
     9.6    let val s = implode_path path
     9.7 -  in Pretty.mark (Isabelle_Markup.path s) (Pretty.str (quote s)) end;
     9.8 +  in Pretty.mark (Markup.path s) (Pretty.str (quote s)) end;
     9.9  
    9.10  val print = Pretty.str_of o pretty;
    9.11  
    10.1 --- a/src/Pure/General/position.ML	Sun Nov 25 18:50:13 2012 +0100
    10.2 +++ b/src/Pure/General/position.ML	Sun Nov 25 19:49:24 2012 +0100
    10.3 @@ -62,7 +62,7 @@
    10.4  
    10.5  fun norm_props (props: Properties.T) =
    10.6    maps (fn a => the_list (find_first (fn (b, _) => a = b) props))
    10.7 -    Isabelle_Markup.position_properties';
    10.8 +    Markup.position_properties';
    10.9  
   10.10  fun make {line = i, offset = j, end_offset = k, props} = Pos ((i, j, k), norm_props props);
   10.11  fun dest (Pos ((i, j, k), props)) = {line = i, offset = j, end_offset = k, props = props};
   10.12 @@ -77,7 +77,7 @@
   10.13  fun offset_of (Pos ((_, j, _), _)) = if valid j then SOME j else NONE;
   10.14  fun end_offset_of (Pos ((_, _, k), _)) = if valid k then SOME k else NONE;
   10.15  
   10.16 -fun file_of (Pos (_, props)) = Properties.get props Isabelle_Markup.fileN;
   10.17 +fun file_of (Pos (_, props)) = Properties.get props Markup.fileN;
   10.18  
   10.19  
   10.20  (* advance *)
   10.21 @@ -109,7 +109,7 @@
   10.22  
   10.23  
   10.24  fun file_name "" = []
   10.25 -  | file_name name = [(Isabelle_Markup.fileN, name)];
   10.26 +  | file_name name = [(Markup.fileN, name)];
   10.27  
   10.28  fun file_only name = Pos ((0, 0, 0), file_name name);
   10.29  fun file name = Pos ((1, 1, 0), file_name name);
   10.30 @@ -117,11 +117,11 @@
   10.31  fun line_file i name = Pos ((i, 1, 0), file_name name);
   10.32  fun line i = line_file i "";
   10.33  
   10.34 -fun id id = Pos ((0, 1, 0), [(Isabelle_Markup.idN, id)]);
   10.35 -fun id_only id = Pos ((0, 0, 0), [(Isabelle_Markup.idN, id)]);
   10.36 +fun id id = Pos ((0, 1, 0), [(Markup.idN, id)]);
   10.37 +fun id_only id = Pos ((0, 0, 0), [(Markup.idN, id)]);
   10.38  
   10.39 -fun get_id (Pos (_, props)) = Properties.get props Isabelle_Markup.idN;
   10.40 -fun put_id id (Pos (count, props)) = Pos (count, Properties.put (Isabelle_Markup.idN, id) props);
   10.41 +fun get_id (Pos (_, props)) = Properties.get props Markup.idN;
   10.42 +fun put_id id (Pos (count, props)) = Pos (count, Properties.put (Markup.idN, id) props);
   10.43  
   10.44  
   10.45  (* markup properties *)
   10.46 @@ -133,26 +133,24 @@
   10.47          NONE => 0
   10.48        | SOME s => the_default 0 (Int.fromString s));
   10.49    in
   10.50 -    make {line = get Isabelle_Markup.lineN, offset = get Isabelle_Markup.offsetN,
   10.51 -      end_offset = get Isabelle_Markup.end_offsetN, props = props}
   10.52 +    make {line = get Markup.lineN, offset = get Markup.offsetN,
   10.53 +      end_offset = get Markup.end_offsetN, props = props}
   10.54    end;
   10.55  
   10.56  
   10.57  fun value k i = if valid i then [(k, string_of_int i)] else [];
   10.58  
   10.59  fun properties_of (Pos ((i, j, k), props)) =
   10.60 -  value Isabelle_Markup.lineN i @
   10.61 -  value Isabelle_Markup.offsetN j @
   10.62 -  value Isabelle_Markup.end_offsetN k @ props;
   10.63 +  value Markup.lineN i @ value Markup.offsetN j @ value Markup.end_offsetN k @ props;
   10.64  
   10.65  val def_properties_of = properties_of #> (map (fn (x, y) => ("def_" ^ x, y)));
   10.66  
   10.67  fun entity_properties_of def id pos =
   10.68 -  if def then (Isabelle_Markup.defN, string_of_int id) :: properties_of pos
   10.69 -  else (Isabelle_Markup.refN, string_of_int id) :: def_properties_of pos;
   10.70 +  if def then (Markup.defN, string_of_int id) :: properties_of pos
   10.71 +  else (Markup.refN, string_of_int id) :: def_properties_of pos;
   10.72  
   10.73  fun default_properties default props =
   10.74 -  if exists (member (op =) Isabelle_Markup.position_properties o #1) props then props
   10.75 +  if exists (member (op =) Markup.position_properties o #1) props then props
   10.76    else properties_of default @ props;
   10.77  
   10.78  val markup = Markup.properties o properties_of;
   10.79 @@ -194,9 +192,7 @@
   10.80        | _ => "");
   10.81    in
   10.82      if null props then ""
   10.83 -    else
   10.84 -      (if s = "" then "" else " ") ^
   10.85 -        Markup.markup (Markup.properties props Isabelle_Markup.position) s
   10.86 +    else (if s = "" then "" else " ") ^ Markup.markup (Markup.properties props Markup.position) s
   10.87    end;
   10.88  
   10.89  val here_list = space_implode " " o map here;
    11.1 --- a/src/Pure/General/position.scala	Sun Nov 25 18:50:13 2012 +0100
    11.2 +++ b/src/Pure/General/position.scala	Sun Nov 25 19:49:24 2012 +0100
    11.3 @@ -14,17 +14,17 @@
    11.4  {
    11.5    type T = Properties.T
    11.6  
    11.7 -  val Line = new Properties.Int(Isabelle_Markup.LINE)
    11.8 -  val Offset = new Properties.Int(Isabelle_Markup.OFFSET)
    11.9 -  val End_Offset = new Properties.Int(Isabelle_Markup.END_OFFSET)
   11.10 -  val File = new Properties.String(Isabelle_Markup.FILE)
   11.11 -  val Id = new Properties.Long(Isabelle_Markup.ID)
   11.12 +  val Line = new Properties.Int(Markup.LINE)
   11.13 +  val Offset = new Properties.Int(Markup.OFFSET)
   11.14 +  val End_Offset = new Properties.Int(Markup.END_OFFSET)
   11.15 +  val File = new Properties.String(Markup.FILE)
   11.16 +  val Id = new Properties.Long(Markup.ID)
   11.17  
   11.18 -  val Def_Line = new Properties.Int(Isabelle_Markup.DEF_LINE)
   11.19 -  val Def_Offset = new Properties.Int(Isabelle_Markup.DEF_OFFSET)
   11.20 -  val Def_End_Offset = new Properties.Int(Isabelle_Markup.DEF_END_OFFSET)
   11.21 -  val Def_File = new Properties.String(Isabelle_Markup.DEF_FILE)
   11.22 -  val Def_Id = new Properties.Long(Isabelle_Markup.DEF_ID)
   11.23 +  val Def_Line = new Properties.Int(Markup.DEF_LINE)
   11.24 +  val Def_Offset = new Properties.Int(Markup.DEF_OFFSET)
   11.25 +  val Def_End_Offset = new Properties.Int(Markup.DEF_END_OFFSET)
   11.26 +  val Def_File = new Properties.String(Markup.DEF_FILE)
   11.27 +  val Def_Id = new Properties.Long(Markup.DEF_ID)
   11.28  
   11.29    object Line_File
   11.30    {
   11.31 @@ -84,7 +84,7 @@
   11.32        }
   11.33    }
   11.34  
   11.35 -  def purge(props: T): T = props.filterNot(p => Isabelle_Markup.POSITION_PROPERTIES(p._1))
   11.36 +  def purge(props: T): T = props.filterNot(p => Markup.POSITION_PROPERTIES(p._1))
   11.37  
   11.38  
   11.39    /* here: inlined formal markup */
    12.1 --- a/src/Pure/General/pretty.ML	Sun Nov 25 18:50:13 2012 +0100
    12.2 +++ b/src/Pure/General/pretty.ML	Sun Nov 25 19:49:24 2012 +0100
    12.3 @@ -156,11 +156,11 @@
    12.4  fun mark_str (m, s) = mark m (str s);
    12.5  fun marks_str (ms, s) = fold_rev mark ms (str s);
    12.6  
    12.7 -fun command name = mark_str (Isabelle_Markup.keyword1, name);
    12.8 -fun keyword name = mark_str (Isabelle_Markup.keyword2, name);
    12.9 +fun command name = mark_str (Markup.keyword1, name);
   12.10 +fun keyword name = mark_str (Markup.keyword2, name);
   12.11  
   12.12  val text = breaks o map str o Symbol.explode_words;
   12.13 -val paragraph = markup Isabelle_Markup.paragraph;
   12.14 +val paragraph = markup Markup.paragraph;
   12.15  val para = paragraph o text;
   12.16  
   12.17  fun markup_chunks m prts = markup m (fbreaks prts);
   12.18 @@ -304,11 +304,11 @@
   12.19      fun out (Block ((bg, en), [], _, _)) = Buffer.add bg #> Buffer.add en
   12.20        | out (Block ((bg, en), prts, indent, _)) =
   12.21            Buffer.add bg #>
   12.22 -          Buffer.markup (Isabelle_Markup.block indent) (fold out prts) #>
   12.23 +          Buffer.markup (Markup.block indent) (fold out prts) #>
   12.24            Buffer.add en
   12.25        | out (String (s, _)) = Buffer.add s
   12.26        | out (Break (false, wd)) =
   12.27 -          Buffer.markup (Isabelle_Markup.break wd) (Buffer.add (output_spaces wd))
   12.28 +          Buffer.markup (Markup.break wd) (Buffer.add (output_spaces wd))
   12.29        | out (Break (true, _)) = Buffer.add (Output.output "\n");
   12.30    in out prt Buffer.empty end;
   12.31  
    13.1 --- a/src/Pure/General/pretty.scala	Sun Nov 25 18:50:13 2012 +0100
    13.2 +++ b/src/Pure/General/pretty.scala	Sun Nov 25 19:49:24 2012 +0100
    13.3 @@ -34,11 +34,11 @@
    13.4    object Block
    13.5    {
    13.6      def apply(i: Int, body: XML.Body): XML.Tree =
    13.7 -      XML.Elem(Markup(Isabelle_Markup.BLOCK, Isabelle_Markup.Indent(i)), body)
    13.8 +      XML.Elem(Markup(Markup.BLOCK, Markup.Indent(i)), body)
    13.9  
   13.10      def unapply(tree: XML.Tree): Option[(Int, XML.Body)] =
   13.11        tree match {
   13.12 -        case XML.Elem(Markup(Isabelle_Markup.BLOCK, Isabelle_Markup.Indent(i)), body) =>
   13.13 +        case XML.Elem(Markup(Markup.BLOCK, Markup.Indent(i)), body) =>
   13.14            Some((i, body))
   13.15          case _ => None
   13.16        }
   13.17 @@ -47,19 +47,19 @@
   13.18    object Break
   13.19    {
   13.20      def apply(w: Int): XML.Tree =
   13.21 -      XML.Elem(Markup(Isabelle_Markup.BREAK, Isabelle_Markup.Width(w)),
   13.22 +      XML.Elem(Markup(Markup.BREAK, Markup.Width(w)),
   13.23          List(XML.Text(spaces(w))))
   13.24  
   13.25      def unapply(tree: XML.Tree): Option[Int] =
   13.26        tree match {
   13.27 -        case XML.Elem(Markup(Isabelle_Markup.BREAK, Isabelle_Markup.Width(w)), _) => Some(w)
   13.28 +        case XML.Elem(Markup(Markup.BREAK, Markup.Width(w)), _) => Some(w)
   13.29          case _ => None
   13.30        }
   13.31    }
   13.32  
   13.33    val FBreak = XML.Text("\n")
   13.34  
   13.35 -  val Separator = List(XML.elem(Isabelle_Markup.SEPARATOR, List(XML.Text(space))), FBreak)
   13.36 +  val Separator = List(XML.elem(Markup.SEPARATOR, List(XML.Text(space))), FBreak)
   13.37    def separate(ts: List[XML.Tree]): XML.Body = Library.separate(Separator, ts.map(List(_))).flatten
   13.38  
   13.39  
    14.1 --- a/src/Pure/General/symbol_pos.ML	Sun Nov 25 18:50:13 2012 +0100
    14.2 +++ b/src/Pure/General/symbol_pos.ML	Sun Nov 25 19:49:24 2012 +0100
    14.3 @@ -71,7 +71,7 @@
    14.4  
    14.5      fun err (syms, msg) = fn () =>
    14.6        text () ^ get_pos syms ^
    14.7 -      Markup.markup Isabelle_Markup.no_report (" at " ^ Symbol.beginning 10 (map symbol syms)) ^
    14.8 +      Markup.markup Markup.no_report (" at " ^ Symbol.beginning 10 (map symbol syms)) ^
    14.9        (case msg of NONE => "" | SOME m => "\n" ^ m ());
   14.10    in Scan.!! err scan end;
   14.11  
    15.1 --- a/src/Pure/Isar/obtain.ML	Sun Nov 25 18:50:13 2012 +0100
    15.2 +++ b/src/Pure/Isar/obtain.ML	Sun Nov 25 19:49:24 2012 +0100
    15.3 @@ -299,7 +299,7 @@
    15.4  
    15.5      val goal = Var (("guess", 0), propT);
    15.6      fun print_result ctxt' (k, [(s, [_, th])]) =
    15.7 -      Proof_Display.print_results Isabelle_Markup.state int ctxt' (k, [(s, [th])]);
    15.8 +      Proof_Display.print_results Markup.state int ctxt' (k, [(s, [th])]);
    15.9      val before_qed = SOME (Method.primitive_text (Goal.conclude #> Raw_Simplifier.norm_hhf #>
   15.10          (fn th => Goal.protect (Conjunction.intr (Drule.mk_term (Thm.cprop_of th)) th))));
   15.11      fun after_qed [[_, res]] =
    16.1 --- a/src/Pure/Isar/outer_syntax.ML	Sun Nov 25 18:50:13 2012 +0100
    16.2 +++ b/src/Pure/Isar/outer_syntax.ML	Sun Nov 25 19:49:24 2012 +0100
    16.3 @@ -60,7 +60,7 @@
    16.4  
    16.5  fun command_markup def (name, Command {pos, id, ...}) =
    16.6    Markup.properties (Position.entity_properties_of def id pos)
    16.7 -    (Isabelle_Markup.entity Isabelle_Markup.commandN name);
    16.8 +    (Markup.entity Markup.commandN name);
    16.9  
   16.10  
   16.11  (* parse command *)
    17.1 --- a/src/Pure/Isar/proof.ML	Sun Nov 25 18:50:13 2012 +0100
    17.2 +++ b/src/Pure/Isar/proof.ML	Sun Nov 25 19:49:24 2012 +0100
    17.3 @@ -536,7 +536,7 @@
    17.4  
    17.5  fun status_markup state =
    17.6    (case try goal state of
    17.7 -    SOME {goal, ...} => Isabelle_Markup.proof_state (Thm.nprems_of goal)
    17.8 +    SOME {goal, ...} => Markup.proof_state (Thm.nprems_of goal)
    17.9    | NONE => Markup.empty);
   17.10  
   17.11  fun method_error kind pos state =
   17.12 @@ -1031,7 +1031,7 @@
   17.13  
   17.14  fun skipped_proof state =
   17.15    Context_Position.if_visible (context_of state) Output.report
   17.16 -    (Markup.markup Isabelle_Markup.bad "Skipped proof");
   17.17 +    (Markup.markup Markup.bad "Skipped proof");
   17.18  
   17.19  in
   17.20  
   17.21 @@ -1051,7 +1051,7 @@
   17.22  local
   17.23  
   17.24  fun gen_have prep_att prepp before_qed after_qed stmt int =
   17.25 -  local_goal (Proof_Display.print_results Isabelle_Markup.state int)
   17.26 +  local_goal (Proof_Display.print_results Markup.state int)
   17.27      prep_att prepp "have" before_qed after_qed stmt;
   17.28  
   17.29  fun gen_show prep_att prepp before_qed after_qed stmt int state =
   17.30 @@ -1065,12 +1065,11 @@
   17.31  
   17.32      fun print_results ctxt res =
   17.33        if ! testing then ()
   17.34 -      else Proof_Display.print_results Isabelle_Markup.state int ctxt res;
   17.35 +      else Proof_Display.print_results Markup.state int ctxt res;
   17.36      fun print_rule ctxt th =
   17.37        if ! testing then rule := SOME th
   17.38        else if int then
   17.39 -        writeln
   17.40 -          (Markup.markup Isabelle_Markup.state (Proof_Display.string_of_rule ctxt "Successful" th))
   17.41 +        writeln (Markup.markup Markup.state (Proof_Display.string_of_rule ctxt "Successful" th))
   17.42        else ();
   17.43      val test_proof =
   17.44        try (local_skip_proof true)
    18.1 --- a/src/Pure/Isar/proof_context.ML	Sun Nov 25 18:50:13 2012 +0100
    18.2 +++ b/src/Pure/Isar/proof_context.ML	Sun Nov 25 19:49:24 2012 +0100
    18.3 @@ -444,7 +444,7 @@
    18.4      val (c, pos) = token_content text;
    18.5    in
    18.6      if Lexicon.is_tid c then
    18.7 -     (Context_Position.report ctxt pos Isabelle_Markup.tfree;
    18.8 +     (Context_Position.report ctxt pos Markup.tfree;
    18.9        TFree (c, default_sort ctxt (c, ~1)))
   18.10      else
   18.11        let
   18.12 @@ -476,8 +476,7 @@
   18.13      (case (Variable.lookup_fixed ctxt c, Variable.is_const ctxt c) of
   18.14        (SOME x, false) =>
   18.15          (Context_Position.report ctxt pos
   18.16 -            (Markup.name x
   18.17 -              (if can Name.dest_skolem x then Isabelle_Markup.skolem else Isabelle_Markup.free));
   18.18 +            (Markup.name x (if can Name.dest_skolem x then Markup.skolem else Markup.free));
   18.19            Free (x, infer_type ctxt (x, ty)))
   18.20      | _ => prep_const_proper ctxt strict (c, pos))
   18.21    end;
   18.22 @@ -650,8 +649,7 @@
   18.23  
   18.24      fun add_report S pos reports =
   18.25        if Position.is_reported pos andalso not (AList.defined (op =) reports pos) then
   18.26 -        (pos, Position.reported_text pos Isabelle_Markup.sorting (Syntax.string_of_sort ctxt S))
   18.27 -          :: reports
   18.28 +        (pos, Position.reported_text pos Markup.sorting (Syntax.string_of_sort ctxt S)) :: reports
   18.29        else reports;
   18.30  
   18.31      fun get_sort_reports xi raw_S =
    19.1 --- a/src/Pure/Isar/runtime.ML	Sun Nov 25 18:50:13 2012 +0100
    19.2 +++ b/src/Pure/Isar/runtime.ML	Sun Nov 25 19:49:24 2012 +0100
    19.3 @@ -65,7 +65,7 @@
    19.4      fun exn_msgs (context, (i, exn)) =
    19.5        (case exn of
    19.6          EXCURSION_FAIL (exn, loc) =>
    19.7 -          map (apsnd (fn msg => msg ^ Markup.markup Isabelle_Markup.no_report ("\n" ^ loc)))
    19.8 +          map (apsnd (fn msg => msg ^ Markup.markup Markup.no_report ("\n" ^ loc)))
    19.9              (sorted_msgs context exn)
   19.10        | _ =>
   19.11          let
    20.1 --- a/src/Pure/Isar/token.ML	Sun Nov 25 18:50:13 2012 +0100
    20.2 +++ b/src/Pure/Isar/token.ML	Sun Nov 25 19:49:24 2012 +0100
    20.3 @@ -204,9 +204,7 @@
    20.4  
    20.5  fun source_of (Token ((source, (pos, _)), (_, x), _)) =
    20.6    if YXML.detect x then x
    20.7 -  else
    20.8 -    YXML.string_of
    20.9 -      (XML.Elem (Isabelle_Markup.token (Position.properties_of pos), [XML.Text source]));
   20.10 +  else YXML.string_of (XML.Elem (Markup.token (Position.properties_of pos), [XML.Text source]));
   20.11  
   20.12  fun source_position_of (Token ((source, (pos, _)), _, _)) = (source, pos);
   20.13  
    21.1 --- a/src/Pure/Isar/toplevel.ML	Sun Nov 25 18:50:13 2012 +0100
    21.2 +++ b/src/Pure/Isar/toplevel.ML	Sun Nov 25 19:49:24 2012 +0100
    21.3 @@ -211,7 +211,7 @@
    21.4    | SOME (Proof (prf, _)) =>
    21.5        Proof.pretty_state (Proof_Node.position prf) (Proof_Node.current prf)
    21.6    | SOME (SkipProof (d, _)) => [Pretty.str ("skipped proof: depth " ^ string_of_int d)])
    21.7 -  |> Pretty.markup_chunks Isabelle_Markup.state |> Pretty.writeln;
    21.8 +  |> Pretty.markup_chunks Markup.state |> Pretty.writeln;
    21.9  
   21.10  fun pretty_abstract state = Pretty.str ("<Isar " ^ str_of_state state ^ ">");
   21.11  
    22.1 --- a/src/Pure/ML/ml_compiler_polyml.ML	Sun Nov 25 18:50:13 2012 +0100
    22.2 +++ b/src/Pure/ML/ml_compiler_polyml.ML	Sun Nov 25 19:49:24 2012 +0100
    22.3 @@ -15,7 +15,7 @@
    22.4        endLine = _, endPosition = end_offset} = loc;
    22.5      val props =
    22.6        (case YXML.parse text of
    22.7 -        XML.Elem ((e, atts), _) => if e = Isabelle_Markup.positionN then atts else []
    22.8 +        XML.Elem ((e, atts), _) => if e = Markup.positionN then atts else []
    22.9        | XML.Text s => Position.file_name s);
   22.10    in
   22.11      Position.make {line = line, offset = offset, end_offset = end_offset, props = props}
   22.12 @@ -41,20 +41,19 @@
   22.13  
   22.14      fun reported_entity kind loc decl =
   22.15        reported_text (position_of loc)
   22.16 -        (Isabelle_Markup.entityN,
   22.17 -          (Markup.kindN, kind) :: Position.def_properties_of (position_of decl)) "";
   22.18 +        (Markup.entityN, (Markup.kindN, kind) :: Position.def_properties_of (position_of decl)) "";
   22.19  
   22.20      fun reported loc (PolyML.PTtype types) =
   22.21            cons
   22.22              (PolyML.NameSpace.displayTypeExpression (types, depth, space)
   22.23                |> pretty_ml |> Pretty.from_ML |> Pretty.string_of
   22.24 -              |> reported_text (position_of loc) Isabelle_Markup.ML_typing)
   22.25 +              |> reported_text (position_of loc) Markup.ML_typing)
   22.26        | reported loc (PolyML.PTdeclaredAt decl) =
   22.27 -          cons (reported_entity Isabelle_Markup.ML_defN loc decl)
   22.28 +          cons (reported_entity Markup.ML_defN loc decl)
   22.29        | reported loc (PolyML.PTopenedAt decl) =
   22.30 -          cons (reported_entity Isabelle_Markup.ML_openN loc decl)
   22.31 +          cons (reported_entity Markup.ML_openN loc decl)
   22.32        | reported loc (PolyML.PTstructureAt decl) =
   22.33 -          cons (reported_entity Isabelle_Markup.ML_structN loc decl)
   22.34 +          cons (reported_entity Markup.ML_structN loc decl)
   22.35        | reported _ (PolyML.PTnextSibling tree) = reported_tree (tree ())
   22.36        | reported _ (PolyML.PTfirstChild tree) = reported_tree (tree ())
   22.37        | reported _ _ = I
   22.38 @@ -73,9 +72,9 @@
   22.39      (* input *)
   22.40  
   22.41      val location_props =
   22.42 -      op ^ (YXML.output_markup (Isabelle_Markup.position |> Markup.properties
   22.43 -            (filter (member (op =)
   22.44 -              [Isabelle_Markup.idN, Isabelle_Markup.fileN] o #1) (Position.properties_of pos))));
   22.45 +      op ^
   22.46 +        (YXML.output_markup (Markup.position |> Markup.properties
   22.47 +          (filter (member (op =) [Markup.idN, Markup.fileN] o #1) (Position.properties_of pos))));
   22.48  
   22.49      val input_buffer =
   22.50        Unsynchronized.ref (toks |> map
    23.1 --- a/src/Pure/ML/ml_context.ML	Sun Nov 25 18:50:13 2012 +0100
    23.2 +++ b/src/Pure/ML/ml_context.ML	Sun Nov 25 19:49:24 2012 +0100
    23.3 @@ -103,7 +103,7 @@
    23.4  structure Antiq_Parsers = Theory_Data
    23.5  (
    23.6    type T = (Position.T -> antiq context_parser) Name_Space.table;
    23.7 -  val empty : T = Name_Space.empty_table Isabelle_Markup.ML_antiquotationN;
    23.8 +  val empty : T = Name_Space.empty_table Markup.ML_antiquotationN;
    23.9    val extend = I;
   23.10    fun merge data : T = Name_Space.merge_tables data;
   23.11  );
   23.12 @@ -119,7 +119,7 @@
   23.13      val thy = Proof_Context.theory_of ctxt;
   23.14      val ((xname, _), pos) = Args.dest_src src;
   23.15      val (_, scan) = Name_Space.check (Context.Proof ctxt) (Antiq_Parsers.get thy) (xname, pos);
   23.16 -  in Args.context_syntax Isabelle_Markup.ML_antiquotationN (scan pos) src ctxt end;
   23.17 +  in Args.context_syntax Markup.ML_antiquotationN (scan pos) src ctxt end;
   23.18  
   23.19  
   23.20  (* parsing and evaluation *)
    24.1 --- a/src/Pure/ML/ml_lex.ML	Sun Nov 25 18:50:13 2012 +0100
    24.2 +++ b/src/Pure/ML/ml_lex.ML	Sun Nov 25 19:49:24 2012 +0100
    24.3 @@ -104,23 +104,23 @@
    24.4  local
    24.5  
    24.6  val token_kind_markup =
    24.7 - fn Keyword   => (Isabelle_Markup.ML_keyword, "")
    24.8 + fn Keyword   => (Markup.ML_keyword, "")
    24.9    | Ident     => (Markup.empty, "")
   24.10    | LongIdent => (Markup.empty, "")
   24.11 -  | TypeVar   => (Isabelle_Markup.ML_tvar, "")
   24.12 -  | Word      => (Isabelle_Markup.ML_numeral, "")
   24.13 -  | Int       => (Isabelle_Markup.ML_numeral, "")
   24.14 -  | Real      => (Isabelle_Markup.ML_numeral, "")
   24.15 -  | Char      => (Isabelle_Markup.ML_char, "")
   24.16 -  | String    => (Isabelle_Markup.ML_string, "")
   24.17 +  | TypeVar   => (Markup.ML_tvar, "")
   24.18 +  | Word      => (Markup.ML_numeral, "")
   24.19 +  | Int       => (Markup.ML_numeral, "")
   24.20 +  | Real      => (Markup.ML_numeral, "")
   24.21 +  | Char      => (Markup.ML_char, "")
   24.22 +  | String    => (Markup.ML_string, "")
   24.23    | Space     => (Markup.empty, "")
   24.24 -  | Comment   => (Isabelle_Markup.ML_comment, "")
   24.25 -  | Error msg => (Isabelle_Markup.bad, msg)
   24.26 +  | Comment   => (Markup.ML_comment, "")
   24.27 +  | Error msg => (Markup.bad, msg)
   24.28    | EOF       => (Markup.empty, "");
   24.29  
   24.30  fun token_markup kind x =
   24.31    if kind = Keyword andalso exists_string (not o Symbol.is_ascii_letter) x
   24.32 -  then (Isabelle_Markup.ML_delimiter, "")
   24.33 +  then (Markup.ML_delimiter, "")
   24.34    else token_kind_markup kind;
   24.35  
   24.36  in
   24.37 @@ -289,7 +289,7 @@
   24.38  
   24.39  fun read pos txt =
   24.40    let
   24.41 -    val _ = Position.report pos Isabelle_Markup.ML_source;
   24.42 +    val _ = Position.report pos Markup.ML_source;
   24.43      val syms = Symbol_Pos.explode (txt, pos);
   24.44      val termination =
   24.45        if null syms then []
    25.1 --- a/src/Pure/PIDE/command.ML	Sun Nov 25 18:50:13 2012 +0100
    25.2 +++ b/src/Pure/PIDE/command.ML	Sun Nov 25 19:49:24 2012 +0100
    25.3 @@ -75,7 +75,7 @@
    25.4            handle exn => ML_Compiler.exn_messages exn)) ();
    25.5  
    25.6  fun timing tr t =
    25.7 -  if Timing.is_relevant t then Toplevel.status tr (Isabelle_Markup.timing t) else ();
    25.8 +  if Timing.is_relevant t then Toplevel.status tr (Markup.timing t) else ();
    25.9  
   25.10  fun proof_status tr st =
   25.11    (case try Toplevel.proof_of st of
   25.12 @@ -99,20 +99,20 @@
   25.13        val is_proof = Keyword.is_proof (Toplevel.name_of tr);
   25.14  
   25.15        val _ = Multithreading.interrupted ();
   25.16 -      val _ = Toplevel.status tr Isabelle_Markup.running;
   25.17 +      val _ = Toplevel.status tr Markup.running;
   25.18        val start = Timing.start ();
   25.19        val (errs1, result) = run (is_init orelse is_proof) (Toplevel.set_print false tr) st;
   25.20        val errs2 = (case result of NONE => [] | SOME st' => check_cmts tr cmts st');
   25.21        val errs = errs1 @ errs2;
   25.22        val _ = timing tr (Timing.result start);
   25.23 -      val _ = Toplevel.status tr Isabelle_Markup.finished;
   25.24 +      val _ = Toplevel.status tr Markup.finished;
   25.25        val _ = List.app (Toplevel.error_msg tr) errs;
   25.26      in
   25.27        (case result of
   25.28          NONE =>
   25.29            let
   25.30              val _ = if null errs then Exn.interrupt () else ();
   25.31 -            val _ = Toplevel.status tr Isabelle_Markup.failed;
   25.32 +            val _ = Toplevel.status tr Markup.failed;
   25.33            in ((st, malformed'), no_print) end
   25.34        | SOME st' =>
   25.35            let
    26.1 --- a/src/Pure/PIDE/command.scala	Sun Nov 25 18:50:13 2012 +0100
    26.2 +++ b/src/Pure/PIDE/command.scala	Sun Nov 25 19:49:24 2012 +0100
    26.3 @@ -34,7 +34,7 @@
    26.4  
    26.5      def + (alt_id: Document.ID, message: XML.Elem): Command.State =
    26.6        message match {
    26.7 -        case XML.Elem(Markup(Isabelle_Markup.STATUS, _), msgs) =>
    26.8 +        case XML.Elem(Markup(Markup.STATUS, _), msgs) =>
    26.9            (this /: msgs)((state, msg) =>
   26.10              msg match {
   26.11                case elem @ XML.Elem(markup, Nil) =>
   26.12 @@ -43,7 +43,7 @@
   26.13                case _ => System.err.println("Ignored status message: " + msg); state
   26.14              })
   26.15  
   26.16 -        case XML.Elem(Markup(Isabelle_Markup.REPORT, _), msgs) =>
   26.17 +        case XML.Elem(Markup(Markup.REPORT, _), msgs) =>
   26.18            (this /: msgs)((state, msg) =>
   26.19              msg match {
   26.20                case XML.Elem(Markup(name, atts @ Position.Id_Range(id, raw_range)), args)
   26.21 @@ -54,7 +54,7 @@
   26.22                  val info: Text.Markup = Text.Info(range, XML.Elem(Markup(name, props), args))
   26.23                  state.add_markup(info)
   26.24                case XML.Elem(Markup(name, atts), args)
   26.25 -              if !atts.exists({ case (a, _) => Isabelle_Markup.POSITION_PROPERTIES(a) }) =>
   26.26 +              if !atts.exists({ case (a, _) => Markup.POSITION_PROPERTIES(a) }) =>
   26.27                  val range = command.proper_range
   26.28                  val props = Position.purge(atts)
   26.29                  val info: Text.Markup = Text.Info(range, XML.Elem(Markup(name, props), args))
   26.30 @@ -65,9 +65,9 @@
   26.31              })
   26.32          case XML.Elem(Markup(name, atts), body) =>
   26.33            atts match {
   26.34 -            case Isabelle_Markup.Serial(i) =>
   26.35 +            case Markup.Serial(i) =>
   26.36                val props = Position.purge(atts)
   26.37 -              val message1 = XML.Elem(Markup(Isabelle_Markup.message(name), props), body)
   26.38 +              val message1 = XML.Elem(Markup(Markup.message(name), props), body)
   26.39                val message2 = XML.Elem(Markup(name, props), body)
   26.40  
   26.41                val st0 = copy(results = results + (i -> message1))
    27.1 --- a/src/Pure/PIDE/document.ML	Sun Nov 25 18:50:13 2012 +0100
    27.2 +++ b/src/Pure/PIDE/document.ML	Sun Nov 25 19:49:24 2012 +0100
    27.3 @@ -272,7 +272,7 @@
    27.4                (#1 (Outer_Syntax.get_syntax ())) (Position.id id_string) text) ());
    27.5        val _ =
    27.6          Position.setmp_thread_data (Position.id_only id_string)
    27.7 -          (fn () => Output.status (Markup.markup_only Isabelle_Markup.accepted)) ();
    27.8 +          (fn () => Output.status (Markup.markup_only Markup.accepted)) ();
    27.9        val commands' =
   27.10          Inttab.update_new (id, (name, span)) commands
   27.11            handle Inttab.DUP dup => err_dup "command" dup;
    28.1 --- a/src/Pure/PIDE/isabelle_markup.ML	Sun Nov 25 18:50:13 2012 +0100
    28.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    28.3 @@ -1,336 +0,0 @@
    28.4 -(*  Title:      Pure/PIDE/isabelle_markup.ML
    28.5 -    Author:     Makarius
    28.6 -
    28.7 -Isabelle markup elements.
    28.8 -*)
    28.9 -
   28.10 -signature ISABELLE_MARKUP =
   28.11 -sig
   28.12 -  val bindingN: string val binding: Markup.T
   28.13 -  val entityN: string val entity: string -> string -> Markup.T
   28.14 -  val get_entity_kind: Markup.T -> string option
   28.15 -  val defN: string
   28.16 -  val refN: string
   28.17 -  val lineN: string
   28.18 -  val offsetN: string
   28.19 -  val end_offsetN: string
   28.20 -  val fileN: string
   28.21 -  val idN: string
   28.22 -  val position_properties': string list
   28.23 -  val position_properties: string list
   28.24 -  val positionN: string val position: Markup.T
   28.25 -  val pathN: string val path: string -> Markup.T
   28.26 -  val indentN: string
   28.27 -  val blockN: string val block: int -> Markup.T
   28.28 -  val widthN: string
   28.29 -  val breakN: string val break: int -> Markup.T
   28.30 -  val fbreakN: string val fbreak: Markup.T
   28.31 -  val hiddenN: string val hidden: Markup.T
   28.32 -  val theoryN: string
   28.33 -  val classN: string
   28.34 -  val type_nameN: string
   28.35 -  val constantN: string
   28.36 -  val fixedN: string val fixed: string -> Markup.T
   28.37 -  val dynamic_factN: string val dynamic_fact: string -> Markup.T
   28.38 -  val tfreeN: string val tfree: Markup.T
   28.39 -  val tvarN: string val tvar: Markup.T
   28.40 -  val freeN: string val free: Markup.T
   28.41 -  val skolemN: string val skolem: Markup.T
   28.42 -  val boundN: string val bound: Markup.T
   28.43 -  val varN: string val var: Markup.T
   28.44 -  val numeralN: string val numeral: Markup.T
   28.45 -  val literalN: string val literal: Markup.T
   28.46 -  val delimiterN: string val delimiter: Markup.T
   28.47 -  val inner_stringN: string val inner_string: Markup.T
   28.48 -  val inner_commentN: string val inner_comment: Markup.T
   28.49 -  val token_rangeN: string val token_range: Markup.T
   28.50 -  val sortN: string val sort: Markup.T
   28.51 -  val typN: string val typ: Markup.T
   28.52 -  val termN: string val term: Markup.T
   28.53 -  val propN: string val prop: Markup.T
   28.54 -  val sortingN: string val sorting: Markup.T
   28.55 -  val typingN: string val typing: Markup.T
   28.56 -  val ML_keywordN: string val ML_keyword: Markup.T
   28.57 -  val ML_delimiterN: string val ML_delimiter: Markup.T
   28.58 -  val ML_tvarN: string val ML_tvar: Markup.T
   28.59 -  val ML_numeralN: string val ML_numeral: Markup.T
   28.60 -  val ML_charN: string val ML_char: Markup.T
   28.61 -  val ML_stringN: string val ML_string: Markup.T
   28.62 -  val ML_commentN: string val ML_comment: Markup.T
   28.63 -  val ML_defN: string
   28.64 -  val ML_openN: string
   28.65 -  val ML_structN: string
   28.66 -  val ML_typingN: string val ML_typing: Markup.T
   28.67 -  val ML_sourceN: string val ML_source: Markup.T
   28.68 -  val doc_sourceN: string val doc_source: Markup.T
   28.69 -  val antiqN: string val antiq: Markup.T
   28.70 -  val ML_antiquotationN: string
   28.71 -  val document_antiquotationN: string
   28.72 -  val document_antiquotation_optionN: string
   28.73 -  val paragraphN: string val paragraph: Markup.T
   28.74 -  val keywordN: string val keyword: Markup.T
   28.75 -  val operatorN: string val operator: Markup.T
   28.76 -  val commandN: string val command: Markup.T
   28.77 -  val stringN: string val string: Markup.T
   28.78 -  val altstringN: string val altstring: Markup.T
   28.79 -  val verbatimN: string val verbatim: Markup.T
   28.80 -  val commentN: string val comment: Markup.T
   28.81 -  val controlN: string val control: Markup.T
   28.82 -  val tokenN: string val token: Properties.T -> Markup.T
   28.83 -  val keyword1N: string val keyword1: Markup.T
   28.84 -  val keyword2N: string val keyword2: Markup.T
   28.85 -  val elapsedN: string
   28.86 -  val cpuN: string
   28.87 -  val gcN: string
   28.88 -  val timingN: string val timing: Timing.timing -> Markup.T
   28.89 -  val subgoalsN: string
   28.90 -  val proof_stateN: string val proof_state: int -> Markup.T
   28.91 -  val stateN: string val state: Markup.T
   28.92 -  val subgoalN: string val subgoal: Markup.T
   28.93 -  val sendbackN: string val sendback: Markup.T
   28.94 -  val intensifyN: string val intensify: Markup.T
   28.95 -  val taskN: string
   28.96 -  val acceptedN: string val accepted: Markup.T
   28.97 -  val forkedN: string val forked: Markup.T
   28.98 -  val joinedN: string val joined: Markup.T
   28.99 -  val runningN: string val running: Markup.T
  28.100 -  val finishedN: string val finished: Markup.T
  28.101 -  val failedN: string val failed: Markup.T
  28.102 -  val serialN: string
  28.103 -  val initN: string
  28.104 -  val statusN: string
  28.105 -  val writelnN: string
  28.106 -  val tracingN: string
  28.107 -  val warningN: string
  28.108 -  val errorN: string
  28.109 -  val protocolN: string
  28.110 -  val legacyN: string val legacy: Markup.T
  28.111 -  val promptN: string val prompt: Markup.T
  28.112 -  val reportN: string val report: Markup.T
  28.113 -  val no_reportN: string val no_report: Markup.T
  28.114 -  val badN: string val bad: Markup.T
  28.115 -  val graphviewN: string
  28.116 -  val functionN: string
  28.117 -  val assign_execs: Properties.T
  28.118 -  val removed_versions: Properties.T
  28.119 -  val invoke_scala: string -> string -> Properties.T
  28.120 -  val cancel_scala: string -> Properties.T
  28.121 -end;
  28.122 -
  28.123 -structure Isabelle_Markup: ISABELLE_MARKUP =
  28.124 -struct
  28.125 -
  28.126 -(** markup elements **)
  28.127 -
  28.128 -fun markup_elem elem = (elem, (elem, []): Markup.T);
  28.129 -fun markup_string elem prop = (elem, fn s => (elem, [(prop, s)]): Markup.T);
  28.130 -fun markup_int elem prop = (elem, fn i => (elem, [(prop, Markup.print_int i)]): Markup.T);
  28.131 -
  28.132 -
  28.133 -(* formal entities *)
  28.134 -
  28.135 -val (bindingN, binding) = markup_elem "binding";
  28.136 -
  28.137 -val entityN = "entity";
  28.138 -fun entity kind name = (entityN, [(Markup.nameN, name), (Markup.kindN, kind)]);
  28.139 -
  28.140 -fun get_entity_kind (name, props) =
  28.141 -  if name = entityN then AList.lookup (op =) props Markup.kindN
  28.142 -  else NONE;
  28.143 -
  28.144 -val defN = "def";
  28.145 -val refN = "ref";
  28.146 -
  28.147 -
  28.148 -(* position *)
  28.149 -
  28.150 -val lineN = "line";
  28.151 -val offsetN = "offset";
  28.152 -val end_offsetN = "end_offset";
  28.153 -val fileN = "file";
  28.154 -val idN = "id";
  28.155 -
  28.156 -val position_properties' = [fileN, idN];
  28.157 -val position_properties = [lineN, offsetN, end_offsetN] @ position_properties';
  28.158 -
  28.159 -val (positionN, position) = markup_elem "position";
  28.160 -
  28.161 -
  28.162 -(* path *)
  28.163 -
  28.164 -val (pathN, path) = markup_string "path" Markup.nameN;
  28.165 -
  28.166 -
  28.167 -(* pretty printing *)
  28.168 -
  28.169 -val indentN = "indent";
  28.170 -val (blockN, block) = markup_int "block" indentN;
  28.171 -
  28.172 -val widthN = "width";
  28.173 -val (breakN, break) = markup_int "break" widthN;
  28.174 -
  28.175 -val (fbreakN, fbreak) = markup_elem "fbreak";
  28.176 -
  28.177 -
  28.178 -(* hidden text *)
  28.179 -
  28.180 -val (hiddenN, hidden) = markup_elem "hidden";
  28.181 -
  28.182 -
  28.183 -(* logical entities *)
  28.184 -
  28.185 -val theoryN = "theory";
  28.186 -val classN = "class";
  28.187 -val type_nameN = "type_name";
  28.188 -val constantN = "constant";
  28.189 -
  28.190 -val (fixedN, fixed) = markup_string "fixed" Markup.nameN;
  28.191 -val (dynamic_factN, dynamic_fact) = markup_string "dynamic_fact" Markup.nameN;
  28.192 -
  28.193 -
  28.194 -(* inner syntax *)
  28.195 -
  28.196 -val (tfreeN, tfree) = markup_elem "tfree";
  28.197 -val (tvarN, tvar) = markup_elem "tvar";
  28.198 -val (freeN, free) = markup_elem "free";
  28.199 -val (skolemN, skolem) = markup_elem "skolem";
  28.200 -val (boundN, bound) = markup_elem "bound";
  28.201 -val (varN, var) = markup_elem "var";
  28.202 -val (numeralN, numeral) = markup_elem "numeral";
  28.203 -val (literalN, literal) = markup_elem "literal";
  28.204 -val (delimiterN, delimiter) = markup_elem "delimiter";
  28.205 -val (inner_stringN, inner_string) = markup_elem "inner_string";
  28.206 -val (inner_commentN, inner_comment) = markup_elem "inner_comment";
  28.207 -
  28.208 -val (token_rangeN, token_range) = markup_elem "token_range";
  28.209 -
  28.210 -val (sortN, sort) = markup_elem "sort";
  28.211 -val (typN, typ) = markup_elem "typ";
  28.212 -val (termN, term) = markup_elem "term";
  28.213 -val (propN, prop) = markup_elem "prop";
  28.214 -
  28.215 -val (sortingN, sorting) = markup_elem "sorting";
  28.216 -val (typingN, typing) = markup_elem "typing";
  28.217 -
  28.218 -
  28.219 -(* ML syntax *)
  28.220 -
  28.221 -val (ML_keywordN, ML_keyword) = markup_elem "ML_keyword";
  28.222 -val (ML_delimiterN, ML_delimiter) = markup_elem "ML_delimiter";
  28.223 -val (ML_tvarN, ML_tvar) = markup_elem "ML_tvar";
  28.224 -val (ML_numeralN, ML_numeral) = markup_elem "ML_numeral";
  28.225 -val (ML_charN, ML_char) = markup_elem "ML_char";
  28.226 -val (ML_stringN, ML_string) = markup_elem "ML_string";
  28.227 -val (ML_commentN, ML_comment) = markup_elem "ML_comment";
  28.228 -
  28.229 -val ML_defN = "ML_def";
  28.230 -val ML_openN = "ML_open";
  28.231 -val ML_structN = "ML_struct";
  28.232 -val (ML_typingN, ML_typing) = markup_elem "ML_typing";
  28.233 -
  28.234 -
  28.235 -(* embedded source text *)
  28.236 -
  28.237 -val (ML_sourceN, ML_source) = markup_elem "ML_source";
  28.238 -val (doc_sourceN, doc_source) = markup_elem "doc_source";
  28.239 -
  28.240 -val (antiqN, antiq) = markup_elem "antiq";
  28.241 -val ML_antiquotationN = "ML_antiquotation";
  28.242 -val document_antiquotationN = "document_antiquotation";
  28.243 -val document_antiquotation_optionN = "document_antiquotation_option";
  28.244 -
  28.245 -
  28.246 -(* text structure *)
  28.247 -
  28.248 -val (paragraphN, paragraph) = markup_elem "paragraph";
  28.249 -
  28.250 -
  28.251 -(* outer syntax *)
  28.252 -
  28.253 -val (keywordN, keyword) = markup_elem "keyword";
  28.254 -val (operatorN, operator) = markup_elem "operator";
  28.255 -val (commandN, command) = markup_elem "command";
  28.256 -val (stringN, string) = markup_elem "string";
  28.257 -val (altstringN, altstring) = markup_elem "altstring";
  28.258 -val (verbatimN, verbatim) = markup_elem "verbatim";
  28.259 -val (commentN, comment) = markup_elem "comment";
  28.260 -val (controlN, control) = markup_elem "control";
  28.261 -
  28.262 -val tokenN = "token";
  28.263 -fun token props = (tokenN, props);
  28.264 -
  28.265 -val (keyword1N, keyword1) = markup_elem "keyword1";
  28.266 -val (keyword2N, keyword2) = markup_elem "keyword2";
  28.267 -
  28.268 -
  28.269 -(* timing *)
  28.270 -
  28.271 -val timingN = "timing";
  28.272 -val elapsedN = "elapsed";
  28.273 -val cpuN = "cpu";
  28.274 -val gcN = "gc";
  28.275 -
  28.276 -fun timing {elapsed, cpu, gc} =
  28.277 -  (timingN,
  28.278 -   [(elapsedN, Time.toString elapsed),
  28.279 -    (cpuN, Time.toString cpu),
  28.280 -    (gcN, Time.toString gc)]);
  28.281 -
  28.282 -
  28.283 -(* toplevel *)
  28.284 -
  28.285 -val subgoalsN = "subgoals";
  28.286 -val (proof_stateN, proof_state) = markup_int "proof_state" subgoalsN;
  28.287 -
  28.288 -val (stateN, state) = markup_elem "state";
  28.289 -val (subgoalN, subgoal) = markup_elem "subgoal";
  28.290 -val (sendbackN, sendback) = markup_elem "sendback";
  28.291 -val (intensifyN, intensify) = markup_elem "intensify";
  28.292 -
  28.293 -
  28.294 -(* command status *)
  28.295 -
  28.296 -val taskN = "task";
  28.297 -
  28.298 -val (acceptedN, accepted) = markup_elem "accepted";
  28.299 -val (forkedN, forked) = markup_elem "forked";
  28.300 -val (joinedN, joined) = markup_elem "joined";
  28.301 -val (runningN, running) = markup_elem "running";
  28.302 -val (finishedN, finished) = markup_elem "finished";
  28.303 -val (failedN, failed) = markup_elem "failed";
  28.304 -
  28.305 -
  28.306 -(* messages *)
  28.307 -
  28.308 -val serialN = "serial";
  28.309 -
  28.310 -val initN = "init";
  28.311 -val statusN = "status";
  28.312 -val writelnN = "writeln";
  28.313 -val tracingN = "tracing";
  28.314 -val warningN = "warning";
  28.315 -val errorN = "error";
  28.316 -val protocolN = "protocol";
  28.317 -
  28.318 -val (legacyN, legacy) = markup_elem "legacy";
  28.319 -val (promptN, prompt) = markup_elem "prompt";
  28.320 -
  28.321 -val (reportN, report) = markup_elem "report";
  28.322 -val (no_reportN, no_report) = markup_elem "no_report";
  28.323 -
  28.324 -val (badN, bad) = markup_elem "bad";
  28.325 -
  28.326 -val graphviewN = "graphview";
  28.327 -
  28.328 -
  28.329 -(* protocol message functions *)
  28.330 -
  28.331 -val functionN = "function"
  28.332 -
  28.333 -val assign_execs = [(functionN, "assign_execs")];
  28.334 -val removed_versions = [(functionN, "removed_versions")];
  28.335 -
  28.336 -fun invoke_scala name id = [(functionN, "invoke_scala"), (Markup.nameN, name), (idN, id)];
  28.337 -fun cancel_scala id = [(functionN, "cancel_scala"), (idN, id)];
  28.338 -
  28.339 -end;
    29.1 --- a/src/Pure/PIDE/isabelle_markup.scala	Sun Nov 25 18:50:13 2012 +0100
    29.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    29.3 @@ -1,291 +0,0 @@
    29.4 -/*  Title:      Pure/PIDE/isabelle_markup.scala
    29.5 -    Author:     Makarius
    29.6 -
    29.7 -Isabelle markup elements.
    29.8 -*/
    29.9 -
   29.10 -package isabelle
   29.11 -
   29.12 -
   29.13 -object Isabelle_Markup
   29.14 -{
   29.15 -  /* formal entities */
   29.16 -
   29.17 -  val BINDING = "binding"
   29.18 -  val ENTITY = "entity"
   29.19 -  val DEF = "def"
   29.20 -  val REF = "ref"
   29.21 -
   29.22 -  object Entity
   29.23 -  {
   29.24 -    def unapply(markup: Markup): Option[(String, String)] =
   29.25 -      markup match {
   29.26 -        case Markup(ENTITY, props @ Markup.Kind(kind)) =>
   29.27 -          props match {
   29.28 -            case Markup.Name(name) => Some(kind, name)
   29.29 -            case _ => None
   29.30 -          }
   29.31 -        case _ => None
   29.32 -      }
   29.33 -  }
   29.34 -
   29.35 -
   29.36 -  /* position */
   29.37 -
   29.38 -  val LINE = "line"
   29.39 -  val OFFSET = "offset"
   29.40 -  val END_OFFSET = "end_offset"
   29.41 -  val FILE = "file"
   29.42 -  val ID = "id"
   29.43 -
   29.44 -  val DEF_LINE = "def_line"
   29.45 -  val DEF_OFFSET = "def_offset"
   29.46 -  val DEF_END_OFFSET = "def_end_offset"
   29.47 -  val DEF_FILE = "def_file"
   29.48 -  val DEF_ID = "def_id"
   29.49 -
   29.50 -  val POSITION_PROPERTIES = Set(LINE, OFFSET, END_OFFSET, FILE, ID)
   29.51 -  val POSITION = "position"
   29.52 -
   29.53 -
   29.54 -  /* path */
   29.55 -
   29.56 -  val PATH = "path"
   29.57 -
   29.58 -  object Path
   29.59 -  {
   29.60 -    def unapply(markup: Markup): Option[String] =
   29.61 -      markup match {
   29.62 -        case Markup(PATH, Markup.Name(name)) => Some(name)
   29.63 -        case _ => None
   29.64 -      }
   29.65 -  }
   29.66 -
   29.67 -
   29.68 -  /* pretty printing */
   29.69 -
   29.70 -  val Indent = new Properties.Int("indent")
   29.71 -  val BLOCK = "block"
   29.72 -  val Width = new Properties.Int("width")
   29.73 -  val BREAK = "break"
   29.74 -
   29.75 -  val SEPARATOR = "separator"
   29.76 -
   29.77 -
   29.78 -  /* hidden text */
   29.79 -
   29.80 -  val HIDDEN = "hidden"
   29.81 -
   29.82 -
   29.83 -  /* logical entities */
   29.84 -
   29.85 -  val CLASS = "class"
   29.86 -  val TYPE_NAME = "type_name"
   29.87 -  val FIXED = "fixed"
   29.88 -  val CONSTANT = "constant"
   29.89 -
   29.90 -  val DYNAMIC_FACT = "dynamic_fact"
   29.91 -
   29.92 -
   29.93 -  /* inner syntax */
   29.94 -
   29.95 -  val TFREE = "tfree"
   29.96 -  val TVAR = "tvar"
   29.97 -  val FREE = "free"
   29.98 -  val SKOLEM = "skolem"
   29.99 -  val BOUND = "bound"
  29.100 -  val VAR = "var"
  29.101 -  val NUMERAL = "numeral"
  29.102 -  val LITERAL = "literal"
  29.103 -  val DELIMITER = "delimiter"
  29.104 -  val INNER_STRING = "inner_string"
  29.105 -  val INNER_COMMENT = "inner_comment"
  29.106 -
  29.107 -  val TOKEN_RANGE = "token_range"
  29.108 -
  29.109 -  val SORT = "sort"
  29.110 -  val TYP = "typ"
  29.111 -  val TERM = "term"
  29.112 -  val PROP = "prop"
  29.113 -
  29.114 -  val SORTING = "sorting"
  29.115 -  val TYPING = "typing"
  29.116 -
  29.117 -  val ATTRIBUTE = "attribute"
  29.118 -  val METHOD = "method"
  29.119 -
  29.120 -
  29.121 -  /* embedded source text */
  29.122 -
  29.123 -  val ML_SOURCE = "ML_source"
  29.124 -  val DOCUMENT_SOURCE = "document_source"
  29.125 -
  29.126 -  val ANTIQ = "antiq"
  29.127 -  val ML_ANTIQUOTATION = "ML_antiquotation"
  29.128 -  val DOCUMENT_ANTIQUOTATION = "document_antiquotation"
  29.129 -  val DOCUMENT_ANTIQUOTATION_OPTION = "document_antiquotation_option"
  29.130 -
  29.131 -
  29.132 -  /* text structure */
  29.133 -
  29.134 -  val PARAGRAPH = "paragraph"
  29.135 -
  29.136 -
  29.137 -  /* ML syntax */
  29.138 -
  29.139 -  val ML_KEYWORD = "ML_keyword"
  29.140 -  val ML_DELIMITER = "ML_delimiter"
  29.141 -  val ML_TVAR = "ML_tvar"
  29.142 -  val ML_NUMERAL = "ML_numeral"
  29.143 -  val ML_CHAR = "ML_char"
  29.144 -  val ML_STRING = "ML_string"
  29.145 -  val ML_COMMENT = "ML_comment"
  29.146 -
  29.147 -  val ML_DEF = "ML_def"
  29.148 -  val ML_OPEN = "ML_open"
  29.149 -  val ML_STRUCT = "ML_struct"
  29.150 -  val ML_TYPING = "ML_typing"
  29.151 -
  29.152 -
  29.153 -  /* outer syntax */
  29.154 -
  29.155 -  val KEYWORD = "keyword"
  29.156 -  val OPERATOR = "operator"
  29.157 -  val COMMAND = "command"
  29.158 -  val STRING = "string"
  29.159 -  val ALTSTRING = "altstring"
  29.160 -  val VERBATIM = "verbatim"
  29.161 -  val COMMENT = "comment"
  29.162 -  val CONTROL = "control"
  29.163 -
  29.164 -  val KEYWORD1 = "keyword1"
  29.165 -  val KEYWORD2 = "keyword2"
  29.166 -
  29.167 -
  29.168 -  /* timing */
  29.169 -
  29.170 -  val TIMING = "timing"
  29.171 -  val ELAPSED = "elapsed"
  29.172 -  val CPU = "cpu"
  29.173 -  val GC = "gc"
  29.174 -
  29.175 -  object Timing
  29.176 -  {
  29.177 -    def apply(timing: isabelle.Timing): Markup =
  29.178 -      Markup(TIMING, List(
  29.179 -        (ELAPSED, Properties.Value.Double(timing.elapsed.seconds)),
  29.180 -        (CPU, Properties.Value.Double(timing.cpu.seconds)),
  29.181 -        (GC, Properties.Value.Double(timing.gc.seconds))))
  29.182 -    def unapply(markup: Markup): Option[isabelle.Timing] =
  29.183 -      markup match {
  29.184 -        case Markup(TIMING, List(
  29.185 -          (ELAPSED, Properties.Value.Double(elapsed)),
  29.186 -          (CPU, Properties.Value.Double(cpu)),
  29.187 -          (GC, Properties.Value.Double(gc)))) =>
  29.188 -            Some(new isabelle.Timing(Time.seconds(elapsed), Time.seconds(cpu), Time.seconds(gc)))
  29.189 -        case _ => None
  29.190 -      }
  29.191 -  }
  29.192 -
  29.193 -
  29.194 -  /* toplevel */
  29.195 -
  29.196 -  val SUBGOALS = "subgoals"
  29.197 -  val PROOF_STATE = "proof_state"
  29.198 -
  29.199 -  val STATE = "state"
  29.200 -  val SUBGOAL = "subgoal"
  29.201 -  val SENDBACK = "sendback"
  29.202 -  val INTENSIFY = "intensify"
  29.203 -
  29.204 -
  29.205 -  /* command status */
  29.206 -
  29.207 -  val TASK = "task"
  29.208 -
  29.209 -  val ACCEPTED = "accepted"
  29.210 -  val FORKED = "forked"
  29.211 -  val JOINED = "joined"
  29.212 -  val RUNNING = "running"
  29.213 -  val FINISHED = "finished"
  29.214 -  val FAILED = "failed"
  29.215 -
  29.216 -
  29.217 -  /* interactive documents */
  29.218 -
  29.219 -  val VERSION = "version"
  29.220 -  val ASSIGN = "assign"
  29.221 -
  29.222 -
  29.223 -  /* prover process */
  29.224 -
  29.225 -  val PROVER_COMMAND = "prover_command"
  29.226 -  val PROVER_ARG = "prover_arg"
  29.227 -
  29.228 -
  29.229 -  /* messages */
  29.230 -
  29.231 -  val Serial = new Properties.Long("serial")
  29.232 -
  29.233 -  val MESSAGE = "message"
  29.234 -
  29.235 -  val INIT = "init"
  29.236 -  val STATUS = "status"
  29.237 -  val REPORT = "report"
  29.238 -  val WRITELN = "writeln"
  29.239 -  val TRACING = "tracing"
  29.240 -  val WARNING = "warning"
  29.241 -  val ERROR = "error"
  29.242 -  val PROTOCOL = "protocol"
  29.243 -  val SYSTEM = "system"
  29.244 -  val STDOUT = "stdout"
  29.245 -  val STDERR = "stderr"
  29.246 -  val EXIT = "exit"
  29.247 -
  29.248 -  val WRITELN_MESSAGE = "writeln_message"
  29.249 -  val TRACING_MESSAGE = "tracing_message"
  29.250 -  val WARNING_MESSAGE = "warning_message"
  29.251 -  val ERROR_MESSAGE = "error_message"
  29.252 -
  29.253 -  val message: String => String =
  29.254 -    Map(WRITELN -> WRITELN_MESSAGE, TRACING -> TRACING_MESSAGE,
  29.255 -        WARNING -> WARNING_MESSAGE, ERROR -> ERROR_MESSAGE)
  29.256 -      .withDefault((name: String) => name + "_message")
  29.257 -
  29.258 -  val Return_Code = new Properties.Int("return_code")
  29.259 -
  29.260 -  val LEGACY = "legacy"
  29.261 -
  29.262 -  val NO_REPORT = "no_report"
  29.263 -
  29.264 -  val BAD = "bad"
  29.265 -
  29.266 -  val GRAPHVIEW = "graphview"
  29.267 -
  29.268 -
  29.269 -  /* protocol message functions */
  29.270 -
  29.271 -  val FUNCTION = "function"
  29.272 -  val Function = new Properties.String(FUNCTION)
  29.273 -
  29.274 -  val Assign_Execs: Properties.T = List((FUNCTION, "assign_execs"))
  29.275 -  val Removed_Versions: Properties.T = List((FUNCTION, "removed_versions"))
  29.276 -
  29.277 -  object Invoke_Scala
  29.278 -  {
  29.279 -    def unapply(props: Properties.T): Option[(String, String)] =
  29.280 -      props match {
  29.281 -        case List((FUNCTION, "invoke_scala"), (Markup.NAME, name), (ID, id)) => Some((name, id))
  29.282 -        case _ => None
  29.283 -      }
  29.284 -  }
  29.285 -  object Cancel_Scala
  29.286 -  {
  29.287 -    def unapply(props: Properties.T): Option[String] =
  29.288 -      props match {
  29.289 -        case List((FUNCTION, "cancel_scala"), (ID, id)) => Some(id)
  29.290 -        case _ => None
  29.291 -      }
  29.292 -  }
  29.293 -}
  29.294 -
    30.1 --- a/src/Pure/PIDE/markup.ML	Sun Nov 25 18:50:13 2012 +0100
    30.2 +++ b/src/Pure/PIDE/markup.ML	Sun Nov 25 19:49:24 2012 +0100
    30.3 @@ -1,7 +1,7 @@
    30.4  (*  Title:      Pure/PIDE/markup.ML
    30.5      Author:     Makarius
    30.6  
    30.7 -Generic markup elements.
    30.8 +Isabelle-specific implementation of quasi-abstract markup elements.
    30.9  *)
   30.10  
   30.11  signature MARKUP =
   30.12 @@ -15,6 +15,115 @@
   30.13    val nameN: string
   30.14    val name: string -> T -> T
   30.15    val kindN: string
   30.16 +  val bindingN: string val binding: T
   30.17 +  val entityN: string val entity: string -> string -> T
   30.18 +  val get_entity_kind: T -> string option
   30.19 +  val defN: string
   30.20 +  val refN: string
   30.21 +  val lineN: string
   30.22 +  val offsetN: string
   30.23 +  val end_offsetN: string
   30.24 +  val fileN: string
   30.25 +  val idN: string
   30.26 +  val position_properties': string list
   30.27 +  val position_properties: string list
   30.28 +  val positionN: string val position: T
   30.29 +  val pathN: string val path: string -> T
   30.30 +  val indentN: string
   30.31 +  val blockN: string val block: int -> T
   30.32 +  val widthN: string
   30.33 +  val breakN: string val break: int -> T
   30.34 +  val fbreakN: string val fbreak: T
   30.35 +  val hiddenN: string val hidden: T
   30.36 +  val theoryN: string
   30.37 +  val classN: string
   30.38 +  val type_nameN: string
   30.39 +  val constantN: string
   30.40 +  val fixedN: string val fixed: string -> T
   30.41 +  val dynamic_factN: string val dynamic_fact: string -> T
   30.42 +  val tfreeN: string val tfree: T
   30.43 +  val tvarN: string val tvar: T
   30.44 +  val freeN: string val free: T
   30.45 +  val skolemN: string val skolem: T
   30.46 +  val boundN: string val bound: T
   30.47 +  val varN: string val var: T
   30.48 +  val numeralN: string val numeral: T
   30.49 +  val literalN: string val literal: T
   30.50 +  val delimiterN: string val delimiter: T
   30.51 +  val inner_stringN: string val inner_string: T
   30.52 +  val inner_commentN: string val inner_comment: T
   30.53 +  val token_rangeN: string val token_range: T
   30.54 +  val sortN: string val sort: T
   30.55 +  val typN: string val typ: T
   30.56 +  val termN: string val term: T
   30.57 +  val propN: string val prop: T
   30.58 +  val sortingN: string val sorting: T
   30.59 +  val typingN: string val typing: T
   30.60 +  val ML_keywordN: string val ML_keyword: T
   30.61 +  val ML_delimiterN: string val ML_delimiter: T
   30.62 +  val ML_tvarN: string val ML_tvar: T
   30.63 +  val ML_numeralN: string val ML_numeral: T
   30.64 +  val ML_charN: string val ML_char: T
   30.65 +  val ML_stringN: string val ML_string: T
   30.66 +  val ML_commentN: string val ML_comment: T
   30.67 +  val ML_defN: string
   30.68 +  val ML_openN: string
   30.69 +  val ML_structN: string
   30.70 +  val ML_typingN: string val ML_typing: T
   30.71 +  val ML_sourceN: string val ML_source: T
   30.72 +  val doc_sourceN: string val doc_source: T
   30.73 +  val antiqN: string val antiq: T
   30.74 +  val ML_antiquotationN: string
   30.75 +  val document_antiquotationN: string
   30.76 +  val document_antiquotation_optionN: string
   30.77 +  val paragraphN: string val paragraph: T
   30.78 +  val keywordN: string val keyword: T
   30.79 +  val operatorN: string val operator: T
   30.80 +  val commandN: string val command: T
   30.81 +  val stringN: string val string: T
   30.82 +  val altstringN: string val altstring: T
   30.83 +  val verbatimN: string val verbatim: T
   30.84 +  val commentN: string val comment: T
   30.85 +  val controlN: string val control: T
   30.86 +  val tokenN: string val token: Properties.T -> T
   30.87 +  val keyword1N: string val keyword1: T
   30.88 +  val keyword2N: string val keyword2: T
   30.89 +  val elapsedN: string
   30.90 +  val cpuN: string
   30.91 +  val gcN: string
   30.92 +  val timingN: string val timing: Timing.timing -> T
   30.93 +  val subgoalsN: string
   30.94 +  val proof_stateN: string val proof_state: int -> T
   30.95 +  val stateN: string val state: T
   30.96 +  val subgoalN: string val subgoal: T
   30.97 +  val sendbackN: string val sendback: T
   30.98 +  val intensifyN: string val intensify: T
   30.99 +  val taskN: string
  30.100 +  val acceptedN: string val accepted: T
  30.101 +  val forkedN: string val forked: T
  30.102 +  val joinedN: string val joined: T
  30.103 +  val runningN: string val running: T
  30.104 +  val finishedN: string val finished: T
  30.105 +  val failedN: string val failed: T
  30.106 +  val serialN: string
  30.107 +  val initN: string
  30.108 +  val statusN: string
  30.109 +  val writelnN: string
  30.110 +  val tracingN: string
  30.111 +  val warningN: string
  30.112 +  val errorN: string
  30.113 +  val protocolN: string
  30.114 +  val legacyN: string val legacy: T
  30.115 +  val promptN: string val prompt: T
  30.116 +  val reportN: string val report: T
  30.117 +  val no_reportN: string val no_report: T
  30.118 +  val badN: string val bad: T
  30.119 +  val graphviewN: string
  30.120 +  val functionN: string
  30.121 +  val assign_execs: Properties.T
  30.122 +  val removed_versions: Properties.T
  30.123 +  val invoke_scala: string -> string -> Properties.T
  30.124 +  val cancel_scala: string -> Properties.T
  30.125    val no_output: Output.output * Output.output
  30.126    val default_output: T -> Output.output * Output.output
  30.127    val add_mode: string -> (T -> Output.output * Output.output) -> unit
  30.128 @@ -54,6 +163,10 @@
  30.129  fun properties more_props ((elem, props): T) =
  30.130    (elem, fold_rev Properties.put more_props props);
  30.131  
  30.132 +fun markup_elem elem = (elem, (elem, []): T);
  30.133 +fun markup_string elem prop = (elem, fn s => (elem, [(prop, s)]): T);
  30.134 +fun markup_int elem prop = (elem, fn i => (elem, [(prop, print_int i)]): T);
  30.135 +
  30.136  
  30.137  (* misc properties *)
  30.138  
  30.139 @@ -63,6 +176,213 @@
  30.140  val kindN = "kind";
  30.141  
  30.142  
  30.143 +(* formal entities *)
  30.144 +
  30.145 +val (bindingN, binding) = markup_elem "binding";
  30.146 +
  30.147 +val entityN = "entity";
  30.148 +fun entity kind name = (entityN, [(nameN, name), (kindN, kind)]);
  30.149 +
  30.150 +fun get_entity_kind (name, props) =
  30.151 +  if name = entityN then AList.lookup (op =) props kindN
  30.152 +  else NONE;
  30.153 +
  30.154 +val defN = "def";
  30.155 +val refN = "ref";
  30.156 +
  30.157 +
  30.158 +(* position *)
  30.159 +
  30.160 +val lineN = "line";
  30.161 +val offsetN = "offset";
  30.162 +val end_offsetN = "end_offset";
  30.163 +val fileN = "file";
  30.164 +val idN = "id";
  30.165 +
  30.166 +val position_properties' = [fileN, idN];
  30.167 +val position_properties = [lineN, offsetN, end_offsetN] @ position_properties';
  30.168 +
  30.169 +val (positionN, position) = markup_elem "position";
  30.170 +
  30.171 +
  30.172 +(* path *)
  30.173 +
  30.174 +val (pathN, path) = markup_string "path" nameN;
  30.175 +
  30.176 +
  30.177 +(* pretty printing *)
  30.178 +
  30.179 +val indentN = "indent";
  30.180 +val (blockN, block) = markup_int "block" indentN;
  30.181 +
  30.182 +val widthN = "width";
  30.183 +val (breakN, break) = markup_int "break" widthN;
  30.184 +
  30.185 +val (fbreakN, fbreak) = markup_elem "fbreak";
  30.186 +
  30.187 +
  30.188 +(* hidden text *)
  30.189 +
  30.190 +val (hiddenN, hidden) = markup_elem "hidden";
  30.191 +
  30.192 +
  30.193 +(* logical entities *)
  30.194 +
  30.195 +val theoryN = "theory";
  30.196 +val classN = "class";
  30.197 +val type_nameN = "type_name";
  30.198 +val constantN = "constant";
  30.199 +
  30.200 +val (fixedN, fixed) = markup_string "fixed" nameN;
  30.201 +val (dynamic_factN, dynamic_fact) = markup_string "dynamic_fact" nameN;
  30.202 +
  30.203 +
  30.204 +(* inner syntax *)
  30.205 +
  30.206 +val (tfreeN, tfree) = markup_elem "tfree";
  30.207 +val (tvarN, tvar) = markup_elem "tvar";
  30.208 +val (freeN, free) = markup_elem "free";
  30.209 +val (skolemN, skolem) = markup_elem "skolem";
  30.210 +val (boundN, bound) = markup_elem "bound";
  30.211 +val (varN, var) = markup_elem "var";
  30.212 +val (numeralN, numeral) = markup_elem "numeral";
  30.213 +val (literalN, literal) = markup_elem "literal";
  30.214 +val (delimiterN, delimiter) = markup_elem "delimiter";
  30.215 +val (inner_stringN, inner_string) = markup_elem "inner_string";
  30.216 +val (inner_commentN, inner_comment) = markup_elem "inner_comment";
  30.217 +
  30.218 +val (token_rangeN, token_range) = markup_elem "token_range";
  30.219 +
  30.220 +val (sortN, sort) = markup_elem "sort";
  30.221 +val (typN, typ) = markup_elem "typ";
  30.222 +val (termN, term) = markup_elem "term";
  30.223 +val (propN, prop) = markup_elem "prop";
  30.224 +
  30.225 +val (sortingN, sorting) = markup_elem "sorting";
  30.226 +val (typingN, typing) = markup_elem "typing";
  30.227 +
  30.228 +
  30.229 +(* ML syntax *)
  30.230 +
  30.231 +val (ML_keywordN, ML_keyword) = markup_elem "ML_keyword";
  30.232 +val (ML_delimiterN, ML_delimiter) = markup_elem "ML_delimiter";
  30.233 +val (ML_tvarN, ML_tvar) = markup_elem "ML_tvar";
  30.234 +val (ML_numeralN, ML_numeral) = markup_elem "ML_numeral";
  30.235 +val (ML_charN, ML_char) = markup_elem "ML_char";
  30.236 +val (ML_stringN, ML_string) = markup_elem "ML_string";
  30.237 +val (ML_commentN, ML_comment) = markup_elem "ML_comment";
  30.238 +
  30.239 +val ML_defN = "ML_def";
  30.240 +val ML_openN = "ML_open";
  30.241 +val ML_structN = "ML_struct";
  30.242 +val (ML_typingN, ML_typing) = markup_elem "ML_typing";
  30.243 +
  30.244 +
  30.245 +(* embedded source text *)
  30.246 +
  30.247 +val (ML_sourceN, ML_source) = markup_elem "ML_source";
  30.248 +val (doc_sourceN, doc_source) = markup_elem "doc_source";
  30.249 +
  30.250 +val (antiqN, antiq) = markup_elem "antiq";
  30.251 +val ML_antiquotationN = "ML_antiquotation";
  30.252 +val document_antiquotationN = "document_antiquotation";
  30.253 +val document_antiquotation_optionN = "document_antiquotation_option";
  30.254 +
  30.255 +
  30.256 +(* text structure *)
  30.257 +
  30.258 +val (paragraphN, paragraph) = markup_elem "paragraph";
  30.259 +
  30.260 +
  30.261 +(* outer syntax *)
  30.262 +
  30.263 +val (keywordN, keyword) = markup_elem "keyword";
  30.264 +val (operatorN, operator) = markup_elem "operator";
  30.265 +val (commandN, command) = markup_elem "command";
  30.266 +val (stringN, string) = markup_elem "string";
  30.267 +val (altstringN, altstring) = markup_elem "altstring";
  30.268 +val (verbatimN, verbatim) = markup_elem "verbatim";
  30.269 +val (commentN, comment) = markup_elem "comment";
  30.270 +val (controlN, control) = markup_elem "control";
  30.271 +
  30.272 +val tokenN = "token";
  30.273 +fun token props = (tokenN, props);
  30.274 +
  30.275 +val (keyword1N, keyword1) = markup_elem "keyword1";
  30.276 +val (keyword2N, keyword2) = markup_elem "keyword2";
  30.277 +
  30.278 +
  30.279 +(* timing *)
  30.280 +
  30.281 +val timingN = "timing";
  30.282 +val elapsedN = "elapsed";
  30.283 +val cpuN = "cpu";
  30.284 +val gcN = "gc";
  30.285 +
  30.286 +fun timing {elapsed, cpu, gc} =
  30.287 +  (timingN,
  30.288 +   [(elapsedN, Time.toString elapsed),
  30.289 +    (cpuN, Time.toString cpu),
  30.290 +    (gcN, Time.toString gc)]);
  30.291 +
  30.292 +
  30.293 +(* toplevel *)
  30.294 +
  30.295 +val subgoalsN = "subgoals";
  30.296 +val (proof_stateN, proof_state) = markup_int "proof_state" subgoalsN;
  30.297 +
  30.298 +val (stateN, state) = markup_elem "state";
  30.299 +val (subgoalN, subgoal) = markup_elem "subgoal";
  30.300 +val (sendbackN, sendback) = markup_elem "sendback";
  30.301 +val (intensifyN, intensify) = markup_elem "intensify";
  30.302 +
  30.303 +
  30.304 +(* command status *)
  30.305 +
  30.306 +val taskN = "task";
  30.307 +
  30.308 +val (acceptedN, accepted) = markup_elem "accepted";
  30.309 +val (forkedN, forked) = markup_elem "forked";
  30.310 +val (joinedN, joined) = markup_elem "joined";
  30.311 +val (runningN, running) = markup_elem "running";
  30.312 +val (finishedN, finished) = markup_elem "finished";
  30.313 +val (failedN, failed) = markup_elem "failed";
  30.314 +
  30.315 +
  30.316 +(* messages *)
  30.317 +
  30.318 +val serialN = "serial";
  30.319 +
  30.320 +val initN = "init";
  30.321 +val statusN = "status";
  30.322 +val writelnN = "writeln";
  30.323 +val tracingN = "tracing";
  30.324 +val warningN = "warning";
  30.325 +val errorN = "error";
  30.326 +val protocolN = "protocol";
  30.327 +
  30.328 +val (legacyN, legacy) = markup_elem "legacy";
  30.329 +val (promptN, prompt) = markup_elem "prompt";
  30.330 +
  30.331 +val (reportN, report) = markup_elem "report";
  30.332 +val (no_reportN, no_report) = markup_elem "no_report";
  30.333 +
  30.334 +val (badN, bad) = markup_elem "bad";
  30.335 +
  30.336 +val graphviewN = "graphview";
  30.337 +
  30.338 +
  30.339 +(* protocol message functions *)
  30.340 +
  30.341 +val functionN = "function"
  30.342 +
  30.343 +val assign_execs = [(functionN, "assign_execs")];
  30.344 +val removed_versions = [(functionN, "removed_versions")];
  30.345 +
  30.346 +fun invoke_scala name id = [(functionN, "invoke_scala"), (nameN, name), (idN, id)];
  30.347 +fun cancel_scala id = [(functionN, "cancel_scala"), (idN, id)];
  30.348 +
  30.349 +
  30.350  
  30.351  (** print mode operations **)
  30.352  
    31.1 --- a/src/Pure/PIDE/markup.scala	Sun Nov 25 18:50:13 2012 +0100
    31.2 +++ b/src/Pure/PIDE/markup.scala	Sun Nov 25 19:49:24 2012 +0100
    31.3 @@ -2,7 +2,7 @@
    31.4      Module:     PIDE
    31.5      Author:     Makarius
    31.6  
    31.7 -Generic markup elements.
    31.8 +Isabelle-specific implementation of quasi-abstract markup elements.
    31.9  */
   31.10  
   31.11  package isabelle
   31.12 @@ -19,10 +19,290 @@
   31.13    val Kind = new Properties.String(KIND)
   31.14  
   31.15  
   31.16 -  /* elements */
   31.17 +  /* basic markup */
   31.18  
   31.19    val Empty = Markup("", Nil)
   31.20    val Broken = Markup("broken", Nil)
   31.21 +
   31.22 +
   31.23 +  /* formal entities */
   31.24 +
   31.25 +  val BINDING = "binding"
   31.26 +  val ENTITY = "entity"
   31.27 +  val DEF = "def"
   31.28 +  val REF = "ref"
   31.29 +
   31.30 +  object Entity
   31.31 +  {
   31.32 +    def unapply(markup: Markup): Option[(String, String)] =
   31.33 +      markup match {
   31.34 +        case Markup(ENTITY, props @ Kind(kind)) =>
   31.35 +          props match {
   31.36 +            case Name(name) => Some(kind, name)
   31.37 +            case _ => None
   31.38 +          }
   31.39 +        case _ => None
   31.40 +      }
   31.41 +  }
   31.42 +
   31.43 +
   31.44 +  /* position */
   31.45 +
   31.46 +  val LINE = "line"
   31.47 +  val OFFSET = "offset"
   31.48 +  val END_OFFSET = "end_offset"
   31.49 +  val FILE = "file"
   31.50 +  val ID = "id"
   31.51 +
   31.52 +  val DEF_LINE = "def_line"
   31.53 +  val DEF_OFFSET = "def_offset"
   31.54 +  val DEF_END_OFFSET = "def_end_offset"
   31.55 +  val DEF_FILE = "def_file"
   31.56 +  val DEF_ID = "def_id"
   31.57 +
   31.58 +  val POSITION_PROPERTIES = Set(LINE, OFFSET, END_OFFSET, FILE, ID)
   31.59 +  val POSITION = "position"
   31.60 +
   31.61 +
   31.62 +  /* path */
   31.63 +
   31.64 +  val PATH = "path"
   31.65 +
   31.66 +  object Path
   31.67 +  {
   31.68 +    def unapply(markup: Markup): Option[String] =
   31.69 +      markup match {
   31.70 +        case Markup(PATH, Name(name)) => Some(name)
   31.71 +        case _ => None
   31.72 +      }
   31.73 +  }
   31.74 +
   31.75 +
   31.76 +  /* pretty printing */
   31.77 +
   31.78 +  val Indent = new Properties.Int("indent")
   31.79 +  val BLOCK = "block"
   31.80 +  val Width = new Properties.Int("width")
   31.81 +  val BREAK = "break"
   31.82 +
   31.83 +  val SEPARATOR = "separator"
   31.84 +
   31.85 +
   31.86 +  /* hidden text */
   31.87 +
   31.88 +  val HIDDEN = "hidden"
   31.89 +
   31.90 +
   31.91 +  /* logical entities */
   31.92 +
   31.93 +  val CLASS = "class"
   31.94 +  val TYPE_NAME = "type_name"
   31.95 +  val FIXED = "fixed"
   31.96 +  val CONSTANT = "constant"
   31.97 +
   31.98 +  val DYNAMIC_FACT = "dynamic_fact"
   31.99 +
  31.100 +
  31.101 +  /* inner syntax */
  31.102 +
  31.103 +  val TFREE = "tfree"
  31.104 +  val TVAR = "tvar"
  31.105 +  val FREE = "free"
  31.106 +  val SKOLEM = "skolem"
  31.107 +  val BOUND = "bound"
  31.108 +  val VAR = "var"
  31.109 +  val NUMERAL = "numeral"
  31.110 +  val LITERAL = "literal"
  31.111 +  val DELIMITER = "delimiter"
  31.112 +  val INNER_STRING = "inner_string"
  31.113 +  val INNER_COMMENT = "inner_comment"
  31.114 +
  31.115 +  val TOKEN_RANGE = "token_range"
  31.116 +
  31.117 +  val SORT = "sort"
  31.118 +  val TYP = "typ"
  31.119 +  val TERM = "term"
  31.120 +  val PROP = "prop"
  31.121 +
  31.122 +  val SORTING = "sorting"
  31.123 +  val TYPING = "typing"
  31.124 +
  31.125 +  val ATTRIBUTE = "attribute"
  31.126 +  val METHOD = "method"
  31.127 +
  31.128 +
  31.129 +  /* embedded source text */
  31.130 +
  31.131 +  val ML_SOURCE = "ML_source"
  31.132 +  val DOCUMENT_SOURCE = "document_source"
  31.133 +
  31.134 +  val ANTIQ = "antiq"
  31.135 +  val ML_ANTIQUOTATION = "ML_antiquotation"
  31.136 +  val DOCUMENT_ANTIQUOTATION = "document_antiquotation"
  31.137 +  val DOCUMENT_ANTIQUOTATION_OPTION = "document_antiquotation_option"
  31.138 +
  31.139 +
  31.140 +  /* text structure */
  31.141 +
  31.142 +  val PARAGRAPH = "paragraph"
  31.143 +
  31.144 +
  31.145 +  /* ML syntax */
  31.146 +
  31.147 +  val ML_KEYWORD = "ML_keyword"
  31.148 +  val ML_DELIMITER = "ML_delimiter"
  31.149 +  val ML_TVAR = "ML_tvar"
  31.150 +  val ML_NUMERAL = "ML_numeral"
  31.151 +  val ML_CHAR = "ML_char"
  31.152 +  val ML_STRING = "ML_string"
  31.153 +  val ML_COMMENT = "ML_comment"
  31.154 +
  31.155 +  val ML_DEF = "ML_def"
  31.156 +  val ML_OPEN = "ML_open"
  31.157 +  val ML_STRUCT = "ML_struct"
  31.158 +  val ML_TYPING = "ML_typing"
  31.159 +
  31.160 +
  31.161 +  /* outer syntax */
  31.162 +
  31.163 +  val KEYWORD = "keyword"
  31.164 +  val OPERATOR = "operator"
  31.165 +  val COMMAND = "command"
  31.166 +  val STRING = "string"
  31.167 +  val ALTSTRING = "altstring"
  31.168 +  val VERBATIM = "verbatim"
  31.169 +  val COMMENT = "comment"
  31.170 +  val CONTROL = "control"
  31.171 +
  31.172 +  val KEYWORD1 = "keyword1"
  31.173 +  val KEYWORD2 = "keyword2"
  31.174 +
  31.175 +
  31.176 +  /* timing */
  31.177 +
  31.178 +  val TIMING = "timing"
  31.179 +  val ELAPSED = "elapsed"
  31.180 +  val CPU = "cpu"
  31.181 +  val GC = "gc"
  31.182 +
  31.183 +  object Timing
  31.184 +  {
  31.185 +    def apply(timing: isabelle.Timing): Markup =
  31.186 +      Markup(TIMING, List(
  31.187 +        (ELAPSED, Properties.Value.Double(timing.elapsed.seconds)),
  31.188 +        (CPU, Properties.Value.Double(timing.cpu.seconds)),
  31.189 +        (GC, Properties.Value.Double(timing.gc.seconds))))
  31.190 +    def unapply(markup: Markup): Option[isabelle.Timing] =
  31.191 +      markup match {
  31.192 +        case Markup(TIMING, List(
  31.193 +          (ELAPSED, Properties.Value.Double(elapsed)),
  31.194 +          (CPU, Properties.Value.Double(cpu)),
  31.195 +          (GC, Properties.Value.Double(gc)))) =>
  31.196 +            Some(new isabelle.Timing(Time.seconds(elapsed), Time.seconds(cpu), Time.seconds(gc)))
  31.197 +        case _ => None
  31.198 +      }
  31.199 +  }
  31.200 +
  31.201 +
  31.202 +  /* toplevel */
  31.203 +
  31.204 +  val SUBGOALS = "subgoals"
  31.205 +  val PROOF_STATE = "proof_state"
  31.206 +
  31.207 +  val STATE = "state"
  31.208 +  val SUBGOAL = "subgoal"
  31.209 +  val SENDBACK = "sendback"
  31.210 +  val INTENSIFY = "intensify"
  31.211 +
  31.212 +
  31.213 +  /* command status */
  31.214 +
  31.215 +  val TASK = "task"
  31.216 +
  31.217 +  val ACCEPTED = "accepted"
  31.218 +  val FORKED = "forked"
  31.219 +  val JOINED = "joined"
  31.220 +  val RUNNING = "running"
  31.221 +  val FINISHED = "finished"
  31.222 +  val FAILED = "failed"
  31.223 +
  31.224 +
  31.225 +  /* interactive documents */
  31.226 +
  31.227 +  val VERSION = "version"
  31.228 +  val ASSIGN = "assign"
  31.229 +
  31.230 +
  31.231 +  /* prover process */
  31.232 +
  31.233 +  val PROVER_COMMAND = "prover_command"
  31.234 +  val PROVER_ARG = "prover_arg"
  31.235 +
  31.236 +
  31.237 +  /* messages */
  31.238 +
  31.239 +  val Serial = new Properties.Long("serial")
  31.240 +
  31.241 +  val MESSAGE = "message"
  31.242 +
  31.243 +  val INIT = "init"
  31.244 +  val STATUS = "status"
  31.245 +  val REPORT = "report"
  31.246 +  val WRITELN = "writeln"
  31.247 +  val TRACING = "tracing"
  31.248 +  val WARNING = "warning"
  31.249 +  val ERROR = "error"
  31.250 +  val PROTOCOL = "protocol"
  31.251 +  val SYSTEM = "system"
  31.252 +  val STDOUT = "stdout"
  31.253 +  val STDERR = "stderr"
  31.254 +  val EXIT = "exit"
  31.255 +
  31.256 +  val WRITELN_MESSAGE = "writeln_message"
  31.257 +  val TRACING_MESSAGE = "tracing_message"
  31.258 +  val WARNING_MESSAGE = "warning_message"
  31.259 +  val ERROR_MESSAGE = "error_message"
  31.260 +
  31.261 +  val message: String => String =
  31.262 +    Map(WRITELN -> WRITELN_MESSAGE, TRACING -> TRACING_MESSAGE,
  31.263 +        WARNING -> WARNING_MESSAGE, ERROR -> ERROR_MESSAGE)
  31.264 +      .withDefault((name: String) => name + "_message")
  31.265 +
  31.266 +  val Return_Code = new Properties.Int("return_code")
  31.267 +
  31.268 +  val LEGACY = "legacy"
  31.269 +
  31.270 +  val NO_REPORT = "no_report"
  31.271 +
  31.272 +  val BAD = "bad"
  31.273 +
  31.274 +  val GRAPHVIEW = "graphview"
  31.275 +
  31.276 +
  31.277 +  /* protocol message functions */
  31.278 +
  31.279 +  val FUNCTION = "function"
  31.280 +  val Function = new Properties.String(FUNCTION)
  31.281 +
  31.282 +  val Assign_Execs: Properties.T = List((FUNCTION, "assign_execs"))
  31.283 +  val Removed_Versions: Properties.T = List((FUNCTION, "removed_versions"))
  31.284 +
  31.285 +  object Invoke_Scala
  31.286 +  {
  31.287 +    def unapply(props: Properties.T): Option[(String, String)] =
  31.288 +      props match {
  31.289 +        case List((FUNCTION, "invoke_scala"), (NAME, name), (ID, id)) => Some((name, id))
  31.290 +        case _ => None
  31.291 +      }
  31.292 +  }
  31.293 +  object Cancel_Scala
  31.294 +  {
  31.295 +    def unapply(props: Properties.T): Option[String] =
  31.296 +      props match {
  31.297 +        case List((FUNCTION, "cancel_scala"), (ID, id)) => Some(id)
  31.298 +        case _ => None
  31.299 +      }
  31.300 +  }
  31.301  }
  31.302  
  31.303  
    32.1 --- a/src/Pure/PIDE/protocol.ML	Sun Nov 25 18:50:13 2012 +0100
    32.2 +++ b/src/Pure/PIDE/protocol.ML	Sun Nov 25 19:49:24 2012 +0100
    32.3 @@ -53,7 +53,7 @@
    32.4  
    32.5          val (assignment, state') = Document.update old_id new_id edits state;
    32.6          val _ =
    32.7 -          Output.protocol_message Isabelle_Markup.assign_execs
    32.8 +          Output.protocol_message Markup.assign_execs
    32.9              ((new_id, assignment) |>
   32.10                let open XML.Encode
   32.11                in pair int (list (pair int (option int))) end
   32.12 @@ -72,7 +72,7 @@
   32.13            YXML.parse_body versions_yxml |>
   32.14              let open XML.Decode in list int end;
   32.15          val state1 = Document.remove_versions versions state;
   32.16 -        val _ = Output.protocol_message Isabelle_Markup.removed_versions versions_yxml;
   32.17 +        val _ = Output.protocol_message Markup.removed_versions versions_yxml;
   32.18        in state1 end));
   32.19  
   32.20  val _ =
    33.1 --- a/src/Pure/PIDE/protocol.scala	Sun Nov 25 18:50:13 2012 +0100
    33.2 +++ b/src/Pure/PIDE/protocol.scala	Sun Nov 25 19:49:24 2012 +0100
    33.3 @@ -66,17 +66,17 @@
    33.4    }
    33.5  
    33.6    val command_status_markup: Set[String] =
    33.7 -    Set(Isabelle_Markup.ACCEPTED, Isabelle_Markup.FORKED, Isabelle_Markup.JOINED,
    33.8 -      Isabelle_Markup.RUNNING, Isabelle_Markup.FINISHED, Isabelle_Markup.FAILED)
    33.9 +    Set(Markup.ACCEPTED, Markup.FORKED, Markup.JOINED, Markup.RUNNING,
   33.10 +      Markup.FINISHED, Markup.FAILED)
   33.11  
   33.12    def command_status(status: Status, markup: Markup): Status =
   33.13      markup match {
   33.14 -      case Markup(Isabelle_Markup.ACCEPTED, _) => status.copy(accepted = true)
   33.15 -      case Markup(Isabelle_Markup.FORKED, _) => status.copy(touched = true, forks = status.forks + 1)
   33.16 -      case Markup(Isabelle_Markup.JOINED, _) => status.copy(forks = status.forks - 1)
   33.17 -      case Markup(Isabelle_Markup.RUNNING, _) => status.copy(touched = true, runs = status.runs + 1)
   33.18 -      case Markup(Isabelle_Markup.FINISHED, _) => status.copy(runs = status.runs - 1)
   33.19 -      case Markup(Isabelle_Markup.FAILED, _) => status.copy(failed = true)
   33.20 +      case Markup(Markup.ACCEPTED, _) => status.copy(accepted = true)
   33.21 +      case Markup(Markup.FORKED, _) => status.copy(touched = true, forks = status.forks + 1)
   33.22 +      case Markup(Markup.JOINED, _) => status.copy(forks = status.forks - 1)
   33.23 +      case Markup(Markup.RUNNING, _) => status.copy(touched = true, runs = status.runs + 1)
   33.24 +      case Markup(Markup.FINISHED, _) => status.copy(runs = status.runs - 1)
   33.25 +      case Markup(Markup.FAILED, _) => status.copy(failed = true)
   33.26        case _ => status
   33.27      }
   33.28  
   33.29 @@ -120,8 +120,8 @@
   33.30  
   33.31    def clean_message(body: XML.Body): XML.Body =
   33.32      body filter {
   33.33 -      case XML.Elem(Markup(Isabelle_Markup.REPORT, _), _) => false
   33.34 -      case XML.Elem(Markup(Isabelle_Markup.NO_REPORT, _), _) => false
   33.35 +      case XML.Elem(Markup(Markup.REPORT, _), _) => false
   33.36 +      case XML.Elem(Markup(Markup.NO_REPORT, _), _) => false
   33.37        case _ => true
   33.38      } map {
   33.39        case XML.Wrapped_Elem(markup, body, ts) => XML.Wrapped_Elem(markup, body, clean_message(ts))
   33.40 @@ -131,8 +131,8 @@
   33.41  
   33.42    def message_reports(props: Properties.T, body: XML.Body): List[XML.Elem] =
   33.43      body flatMap {
   33.44 -      case XML.Elem(Markup(Isabelle_Markup.REPORT, ps), ts) =>
   33.45 -        List(XML.Elem(Markup(Isabelle_Markup.REPORT, props ::: ps), ts))
   33.46 +      case XML.Elem(Markup(Markup.REPORT, ps), ts) =>
   33.47 +        List(XML.Elem(Markup(Markup.REPORT, props ::: ps), ts))
   33.48        case XML.Wrapped_Elem(_, _, ts) => message_reports(props, ts)
   33.49        case XML.Elem(_, ts) => message_reports(props, ts)
   33.50        case XML.Text(_) => Nil
   33.51 @@ -143,40 +143,38 @@
   33.52  
   33.53    def is_tracing(msg: XML.Tree): Boolean =
   33.54      msg match {
   33.55 -      case XML.Elem(Markup(Isabelle_Markup.TRACING, _), _) => true
   33.56 -      case XML.Elem(Markup(Isabelle_Markup.TRACING_MESSAGE, _), _) => true
   33.57 +      case XML.Elem(Markup(Markup.TRACING, _), _) => true
   33.58 +      case XML.Elem(Markup(Markup.TRACING_MESSAGE, _), _) => true
   33.59        case _ => false
   33.60      }
   33.61  
   33.62    def is_warning(msg: XML.Tree): Boolean =
   33.63      msg match {
   33.64 -      case XML.Elem(Markup(Isabelle_Markup.WARNING, _), _) => true
   33.65 -      case XML.Elem(Markup(Isabelle_Markup.WARNING_MESSAGE, _), _) => true
   33.66 +      case XML.Elem(Markup(Markup.WARNING, _), _) => true
   33.67 +      case XML.Elem(Markup(Markup.WARNING_MESSAGE, _), _) => true
   33.68        case _ => false
   33.69      }
   33.70  
   33.71    def is_error(msg: XML.Tree): Boolean =
   33.72      msg match {
   33.73 -      case XML.Elem(Markup(Isabelle_Markup.ERROR, _), _) => true
   33.74 -      case XML.Elem(Markup(Isabelle_Markup.ERROR_MESSAGE, _), _) => true
   33.75 +      case XML.Elem(Markup(Markup.ERROR, _), _) => true
   33.76 +      case XML.Elem(Markup(Markup.ERROR_MESSAGE, _), _) => true
   33.77        case _ => false
   33.78      }
   33.79  
   33.80    def is_state(msg: XML.Tree): Boolean =
   33.81      msg match {
   33.82 -      case XML.Elem(Markup(Isabelle_Markup.WRITELN, _),
   33.83 -        List(XML.Elem(Markup(Isabelle_Markup.STATE, _), _))) => true
   33.84 -      case XML.Elem(Markup(Isabelle_Markup.WRITELN_MESSAGE, _),
   33.85 -        List(XML.Elem(Markup(Isabelle_Markup.STATE, _), _))) => true
   33.86 +      case XML.Elem(Markup(Markup.WRITELN, _),
   33.87 +        List(XML.Elem(Markup(Markup.STATE, _), _))) => true
   33.88 +      case XML.Elem(Markup(Markup.WRITELN_MESSAGE, _),
   33.89 +        List(XML.Elem(Markup(Markup.STATE, _), _))) => true
   33.90        case _ => false
   33.91      }
   33.92  
   33.93  
   33.94    /* reported positions */
   33.95  
   33.96 -  private val include_pos =
   33.97 -    Set(Isabelle_Markup.BINDING, Isabelle_Markup.ENTITY, Isabelle_Markup.REPORT,
   33.98 -      Isabelle_Markup.POSITION)
   33.99 +  private val include_pos = Set(Markup.BINDING, Markup.ENTITY, Markup.REPORT, Markup.POSITION)
  33.100  
  33.101    def message_positions(command: Command, message: XML.Elem): Set[Text.Range] =
  33.102    {
    34.1 --- a/src/Pure/PIDE/sendback.ML	Sun Nov 25 18:50:13 2012 +0100
    34.2 +++ b/src/Pure/PIDE/sendback.ML	Sun Nov 25 19:49:24 2012 +0100
    34.3 @@ -19,13 +19,13 @@
    34.4    let
    34.5      val props =
    34.6        (case Position.get_id (Position.thread_data ()) of
    34.7 -        SOME id => [(Isabelle_Markup.idN, id)]
    34.8 +        SOME id => [(Markup.idN, id)]
    34.9        | NONE => []);
   34.10 -  in Markup.properties props Isabelle_Markup.sendback end;
   34.11 +  in Markup.properties props Markup.sendback end;
   34.12  
   34.13  fun markup s = Markup.markup (make_markup ()) s;
   34.14  
   34.15 -fun markup_implicit s = Markup.markup Isabelle_Markup.sendback s;
   34.16 +fun markup_implicit s = Markup.markup Markup.sendback s;
   34.17  
   34.18  end;
   34.19  
    35.1 --- a/src/Pure/ProofGeneral/proof_general_emacs.ML	Sun Nov 25 18:50:13 2012 +0100
    35.2 +++ b/src/Pure/ProofGeneral/proof_general_emacs.ML	Sun Nov 25 19:49:24 2012 +0100
    35.3 @@ -39,24 +39,24 @@
    35.4        | XML.Elem ((name, props), ts) =>
    35.5            let
    35.6              val (bg1, en1) =
    35.7 -              if name <> Isabelle_Markup.promptN andalso print_mode_active test_markupN
    35.8 +              if name <> Markup.promptN andalso print_mode_active test_markupN
    35.9                then XML.output_markup (name, props)
   35.10                else Markup.no_output;
   35.11              val (bg2, en2) =
   35.12                if null ts then Markup.no_output
   35.13 -              else if name = Isabelle_Markup.stateN then (special "O" ^ "\n", "\n" ^ special "P")
   35.14 -              else if name = Isabelle_Markup.sendbackN then (special "W", special "X")
   35.15 -              else if name = Isabelle_Markup.intensifyN then (special "0", special "1")
   35.16 -              else if name = Isabelle_Markup.tfreeN then (special "C", special "A")
   35.17 -              else if name = Isabelle_Markup.tvarN then (special "D", special "A")
   35.18 -              else if name = Isabelle_Markup.freeN then (special "E", special "A")
   35.19 -              else if name = Isabelle_Markup.boundN then (special "F", special "A")
   35.20 -              else if name = Isabelle_Markup.varN then (special "G", special "A")
   35.21 -              else if name = Isabelle_Markup.skolemN then (special "H", special "A")
   35.22 +              else if name = Markup.stateN then (special "O" ^ "\n", "\n" ^ special "P")
   35.23 +              else if name = Markup.sendbackN then (special "W", special "X")
   35.24 +              else if name = Markup.intensifyN then (special "0", special "1")
   35.25 +              else if name = Markup.tfreeN then (special "C", special "A")
   35.26 +              else if name = Markup.tvarN then (special "D", special "A")
   35.27 +              else if name = Markup.freeN then (special "E", special "A")
   35.28 +              else if name = Markup.boundN then (special "F", special "A")
   35.29 +              else if name = Markup.varN then (special "G", special "A")
   35.30 +              else if name = Markup.skolemN then (special "H", special "A")
   35.31                else
   35.32 -                (case Isabelle_Markup.get_entity_kind (name, props) of
   35.33 +                (case Markup.get_entity_kind (name, props) of
   35.34                    SOME kind =>
   35.35 -                    if kind = Isabelle_Markup.classN then (special "B", special "A")
   35.36 +                    if kind = Markup.classN then (special "B", special "A")
   35.37                      else Markup.no_output
   35.38                  | NONE => Markup.no_output);
   35.39            in
    36.1 --- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Sun Nov 25 18:50:13 2012 +0100
    36.2 +++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Sun Nov 25 19:49:24 2012 +0100
    36.3 @@ -101,8 +101,7 @@
    36.4  val pgml_syms = map pgml_sym o Symbol.explode;
    36.5  
    36.6  val token_markups =
    36.7 - [Isabelle_Markup.tfreeN, Isabelle_Markup.tvarN, Isabelle_Markup.freeN,
    36.8 -  Isabelle_Markup.boundN, Isabelle_Markup.varN, Isabelle_Markup.skolemN];
    36.9 +  [Markup.tfreeN, Markup.tvarN, Markup.freeN, Markup.boundN, Markup.varN, Markup.skolemN];
   36.10  
   36.11  fun get_int props name =
   36.12    (case Properties.get props name of NONE => NONE | SOME s => Int.fromString s);
   36.13 @@ -115,11 +114,10 @@
   36.14          in [Pgml.Atoms {kind = SOME name, content = content}] end
   36.15        else
   36.16          let val content = maps pgml_terms body in
   36.17 -          if name = Isabelle_Markup.blockN then
   36.18 -            [Pgml.Box {orient = NONE,
   36.19 -              indent = get_int atts Isabelle_Markup.indentN, content = content}]
   36.20 -          else if name = Isabelle_Markup.breakN then
   36.21 -            [Pgml.Break {mandatory = NONE, indent = get_int atts Isabelle_Markup.widthN}]
   36.22 +          if name = Markup.blockN then
   36.23 +            [Pgml.Box {orient = NONE, indent = get_int atts Markup.indentN, content = content}]
   36.24 +          else if name = Markup.breakN then
   36.25 +            [Pgml.Break {mandatory = NONE, indent = get_int atts Markup.widthN}]
   36.26            else content
   36.27          end
   36.28    | pgml_terms (XML.Text text) = map (Pgml.Raw o Pgml.atom_to_xml) (pgml_syms text);
   36.29 @@ -138,7 +136,7 @@
   36.30      val area =
   36.31        (case body of
   36.32          [XML.Elem ((name, _), _)] =>
   36.33 -          if name = Isabelle_Markup.stateN then PgipTypes.Display else default_area
   36.34 +          if name = Markup.stateN then PgipTypes.Display else default_area
   36.35        | _ => default_area);
   36.36    in Pgml.pgml_to_xml (pgml area (maps pgml_terms body)) end;
   36.37  
    37.1 --- a/src/Pure/ROOT	Sun Nov 25 18:50:13 2012 +0100
    37.2 +++ b/src/Pure/ROOT	Sun Nov 25 19:49:24 2012 +0100
    37.3 @@ -144,7 +144,6 @@
    37.4      "ML/ml_thms.ML"
    37.5      "PIDE/command.ML"
    37.6      "PIDE/document.ML"
    37.7 -    "PIDE/isabelle_markup.ML"
    37.8      "PIDE/markup.ML"
    37.9      "PIDE/protocol.ML"
   37.10      "PIDE/sendback.ML"
    38.1 --- a/src/Pure/ROOT.ML	Sun Nov 25 18:50:13 2012 +0100
    38.2 +++ b/src/Pure/ROOT.ML	Sun Nov 25 19:49:24 2012 +0100
    38.3 @@ -30,8 +30,7 @@
    38.4  use "General/output.ML";
    38.5  use "General/timing.ML";
    38.6  use "PIDE/markup.ML";
    38.7 -use "PIDE/isabelle_markup.ML";
    38.8 -fun legacy_feature s = warning (Markup.markup Isabelle_Markup.legacy ("Legacy feature! " ^ s));
    38.9 +fun legacy_feature s = warning (Markup.markup Markup.legacy ("Legacy feature! " ^ s));
   38.10  use "General/scan.ML";
   38.11  use "General/source.ML";
   38.12  use "General/symbol.ML";
    39.1 --- a/src/Pure/Syntax/lexicon.ML	Sun Nov 25 18:50:13 2012 +0100
    39.2 +++ b/src/Pure/Syntax/lexicon.ML	Sun Nov 25 19:49:24 2012 +0100
    39.3 @@ -190,19 +190,17 @@
    39.4  (* markup *)
    39.5  
    39.6  fun literal_markup s =
    39.7 -  if is_ascii_identifier s
    39.8 -  then Isabelle_Markup.literal
    39.9 -  else Isabelle_Markup.delimiter;
   39.10 +  if is_ascii_identifier s then Markup.literal else Markup.delimiter;
   39.11  
   39.12  val token_kind_markup =
   39.13 - fn VarSy   => Isabelle_Markup.var
   39.14 -  | TFreeSy => Isabelle_Markup.tfree
   39.15 -  | TVarSy  => Isabelle_Markup.tvar
   39.16 -  | NumSy   => Isabelle_Markup.numeral
   39.17 -  | FloatSy => Isabelle_Markup.numeral
   39.18 -  | XNumSy  => Isabelle_Markup.numeral
   39.19 -  | StrSy   => Isabelle_Markup.inner_string
   39.20 -  | Comment => Isabelle_Markup.inner_comment
   39.21 + fn VarSy   => Markup.var
   39.22 +  | TFreeSy => Markup.tfree
   39.23 +  | TVarSy  => Markup.tvar
   39.24 +  | NumSy   => Markup.numeral
   39.25 +  | FloatSy => Markup.numeral
   39.26 +  | XNumSy  => Markup.numeral
   39.27 +  | StrSy   => Markup.inner_string
   39.28 +  | Comment => Markup.inner_comment
   39.29    | _       => Markup.empty;
   39.30  
   39.31  fun report_of_token (Token (kind, s, (pos, _))) =
   39.32 @@ -211,7 +209,7 @@
   39.33  
   39.34  fun reported_token_range ctxt tok =
   39.35    if is_proper tok
   39.36 -  then Context_Position.reported_text ctxt (pos_of_token tok) Isabelle_Markup.token_range ""
   39.37 +  then Context_Position.reported_text ctxt (pos_of_token tok) Markup.token_range ""
   39.38    else "";
   39.39  
   39.40  
    40.1 --- a/src/Pure/Syntax/syntax.ML	Sun Nov 25 18:50:13 2012 +0100
    40.2 +++ b/src/Pure/Syntax/syntax.ML	Sun Nov 25 19:49:24 2012 +0100
    40.3 @@ -167,7 +167,7 @@
    40.4  (* outer syntax token -- with optional YXML content *)
    40.5  
    40.6  fun token_position (XML.Elem ((name, props), _)) =
    40.7 -      if name = Isabelle_Markup.tokenN then Position.of_properties props
    40.8 +      if name = Markup.tokenN then Position.of_properties props
    40.9        else Position.none
   40.10    | token_position (XML.Text _) = Position.none;
   40.11  
   40.12 @@ -190,7 +190,7 @@
   40.13    in
   40.14      (case YXML.parse_body str handle Fail msg => error msg of
   40.15        body as [tree as XML.Elem ((name, _), _)] =>
   40.16 -        if name = Isabelle_Markup.tokenN then parse_tree tree else decode body
   40.17 +        if name = Markup.tokenN then parse_tree tree else decode body
   40.18      | [tree as XML.Text _] => parse_tree tree
   40.19      | body => decode body)
   40.20    end;
    41.1 --- a/src/Pure/Syntax/syntax_phases.ML	Sun Nov 25 18:50:13 2012 +0100
    41.2 +++ b/src/Pure/Syntax/syntax_phases.ML	Sun Nov 25 19:49:24 2012 +0100
    41.3 @@ -51,16 +51,16 @@
    41.4    [Name_Space.markup (Consts.space_of (Proof_Context.consts_of ctxt)) c];
    41.5  
    41.6  fun markup_free ctxt x =
    41.7 -  [if can Name.dest_skolem x then Isabelle_Markup.skolem else Isabelle_Markup.free] @
    41.8 +  [if can Name.dest_skolem x then Markup.skolem else Markup.free] @
    41.9    (if Variable.is_body ctxt orelse Variable.is_fixed ctxt x
   41.10     then [Variable.markup_fixed ctxt x]
   41.11     else []);
   41.12  
   41.13 -fun markup_var xi = [Markup.name (Term.string_of_vname xi) Isabelle_Markup.var];
   41.14 +fun markup_var xi = [Markup.name (Term.string_of_vname xi) Markup.var];
   41.15  
   41.16  fun markup_bound def ps (name, id) =
   41.17 -  let val entity = Isabelle_Markup.entity Isabelle_Markup.boundN name in
   41.18 -    Isabelle_Markup.bound ::
   41.19 +  let val entity = Markup.entity Markup.boundN name in
   41.20 +    Markup.bound ::
   41.21        map (fn pos => Markup.properties (Position.entity_properties_of def id pos) entity) ps
   41.22    end;
   41.23  
   41.24 @@ -298,8 +298,7 @@
   41.25      val pts = Syntax.parse syn root (filter Lexicon.is_proper toks)
   41.26        handle ERROR msg =>
   41.27          error (msg ^
   41.28 -          implode
   41.29 -            (map (Markup.markup Isabelle_Markup.report o Lexicon.reported_token_range ctxt) toks));
   41.30 +          implode (map (Markup.markup Markup.report o Lexicon.reported_token_range ctxt) toks));
   41.31      val len = length pts;
   41.32  
   41.33      val limit = Config.get ctxt Syntax.ambiguity_limit;
   41.34 @@ -330,11 +329,10 @@
   41.35  
   41.36  fun parse_failed ctxt pos msg kind =
   41.37    cat_error msg ("Failed to parse " ^ kind ^
   41.38 -    Markup.markup Isabelle_Markup.report
   41.39 -      (Context_Position.reported_text ctxt pos Isabelle_Markup.bad ""));
   41.40 +    Markup.markup Markup.report (Context_Position.reported_text ctxt pos Markup.bad ""));
   41.41  
   41.42  fun parse_sort ctxt =
   41.43 -  Syntax.parse_token ctxt Term_XML.Decode.sort Isabelle_Markup.sort
   41.44 +  Syntax.parse_token ctxt Term_XML.Decode.sort Markup.sort
   41.45      (fn (syms, pos) =>
   41.46        parse_tree ctxt "sort" (syms, pos)
   41.47        |> uncurry (report_result ctxt pos)
   41.48 @@ -343,7 +341,7 @@
   41.49        handle ERROR msg => parse_failed ctxt pos msg "sort");
   41.50  
   41.51  fun parse_typ ctxt =
   41.52 -  Syntax.parse_token ctxt Term_XML.Decode.typ Isabelle_Markup.typ
   41.53 +  Syntax.parse_token ctxt Term_XML.Decode.typ Markup.typ
   41.54      (fn (syms, pos) =>
   41.55        parse_tree ctxt "type" (syms, pos)
   41.56        |> uncurry (report_result ctxt pos)
   41.57 @@ -354,8 +352,8 @@
   41.58    let
   41.59      val (markup, kind, root, constrain) =
   41.60        if is_prop
   41.61 -      then (Isabelle_Markup.prop, "proposition", "prop", Type.constraint propT)
   41.62 -      else (Isabelle_Markup.term, "term", Config.get ctxt Syntax.root, I);
   41.63 +      then (Markup.prop, "proposition", "prop", Type.constraint propT)
   41.64 +      else (Markup.term, "term", Config.get ctxt Syntax.root, I);
   41.65      val decode = constrain o Term_XML.Decode.term;
   41.66    in
   41.67      Syntax.parse_token ctxt decode markup
   41.68 @@ -605,24 +603,23 @@
   41.69    let
   41.70      val m =
   41.71        if Variable.is_fixed ctxt x orelse Syntax.is_pretty_global ctxt
   41.72 -      then Isabelle_Markup.fixed x
   41.73 -      else Isabelle_Markup.intensify;
   41.74 +      then Markup.fixed x else Markup.intensify;
   41.75    in
   41.76      if can Name.dest_skolem x
   41.77 -    then ([m, Isabelle_Markup.skolem], Variable.revert_fixed ctxt x)
   41.78 -    else ([m, Isabelle_Markup.free], x)
   41.79 +    then ([m, Markup.skolem], Variable.revert_fixed ctxt x)
   41.80 +    else ([m, Markup.free], x)
   41.81    end;
   41.82  
   41.83  fun var_or_skolem s =
   41.84    (case Lexicon.read_variable s of
   41.85      SOME (x, i) =>
   41.86        (case try Name.dest_skolem x of
   41.87 -        NONE => (Isabelle_Markup.var, s)
   41.88 -      | SOME x' => (Isabelle_Markup.skolem, Term.string_of_vname (x', i)))
   41.89 -  | NONE => (Isabelle_Markup.var, s));
   41.90 +        NONE => (Markup.var, s)
   41.91 +      | SOME x' => (Markup.skolem, Term.string_of_vname (x', i)))
   41.92 +  | NONE => (Markup.var, s));
   41.93  
   41.94 -val typing_elem = YXML.output_markup_elem Isabelle_Markup.typing;
   41.95 -val sorting_elem = YXML.output_markup_elem Isabelle_Markup.sorting;
   41.96 +val typing_elem = YXML.output_markup_elem Markup.typing;
   41.97 +val sorting_elem = YXML.output_markup_elem Markup.sorting;
   41.98  
   41.99  fun unparse_t t_to_ast prt_t markup ctxt t =
  41.100    let
  41.101 @@ -647,14 +644,14 @@
  41.102            case_fixed = fn x => free_or_skolem ctxt x,
  41.103            case_default = fn x => ([], x)});
  41.104  
  41.105 -    fun token_trans "_tfree" x = SOME (Pretty.mark_str (Isabelle_Markup.tfree, x))
  41.106 -      | token_trans "_tvar" x = SOME (Pretty.mark_str (Isabelle_Markup.tvar, x))
  41.107 +    fun token_trans "_tfree" x = SOME (Pretty.mark_str (Markup.tfree, x))
  41.108 +      | token_trans "_tvar" x = SOME (Pretty.mark_str (Markup.tvar, x))
  41.109        | token_trans "_free" x = SOME (Pretty.marks_str (free_or_skolem ctxt x))
  41.110 -      | token_trans "_bound" x = SOME (Pretty.mark_str (Isabelle_Markup.bound, x))
  41.111 -      | token_trans "_loose" x = SOME (Pretty.mark_str (Isabelle_Markup.bad, x))
  41.112 +      | token_trans "_bound" x = SOME (Pretty.mark_str (Markup.bound, x))
  41.113 +      | token_trans "_loose" x = SOME (Pretty.mark_str (Markup.bad, x))
  41.114        | token_trans "_var" x = SOME (Pretty.mark_str (var_or_skolem x))
  41.115 -      | token_trans "_numeral" x = SOME (Pretty.mark_str (Isabelle_Markup.numeral, x))
  41.116 -      | token_trans "_inner_string" x = SOME (Pretty.mark_str (Isabelle_Markup.inner_string, x))
  41.117 +      | token_trans "_numeral" x = SOME (Pretty.mark_str (Markup.numeral, x))
  41.118 +      | token_trans "_inner_string" x = SOME (Pretty.mark_str (Markup.inner_string, x))
  41.119        | token_trans _ _ = NONE;
  41.120  
  41.121      fun markup_trans a [Ast.Variable x] = token_trans a x
  41.122 @@ -694,8 +691,8 @@
  41.123  
  41.124  in
  41.125  
  41.126 -val unparse_sort = unparse_t sort_to_ast Printer.pretty_typ_ast Isabelle_Markup.sort;
  41.127 -val unparse_typ = unparse_t typ_to_ast Printer.pretty_typ_ast Isabelle_Markup.typ;
  41.128 +val unparse_sort = unparse_t sort_to_ast Printer.pretty_typ_ast Markup.sort;
  41.129 +val unparse_typ = unparse_t typ_to_ast Printer.pretty_typ_ast Markup.typ;
  41.130  
  41.131  fun unparse_term ctxt =
  41.132    let
  41.133 @@ -705,7 +702,7 @@
  41.134    in
  41.135      unparse_t (term_to_ast idents (is_some o Syntax.lookup_const syn))
  41.136        (Printer.pretty_term_ast (not (Pure_Thy.old_appl_syntax thy)))
  41.137 -      Isabelle_Markup.term ctxt
  41.138 +      Markup.term ctxt
  41.139    end;
  41.140  
  41.141  end;
  41.142 @@ -871,7 +868,7 @@
  41.143      val typing_report =
  41.144        fold2 (fn (pos, _) => fn ty =>
  41.145          if Position.is_reported pos then
  41.146 -          cons (Position.reported_text pos Isabelle_Markup.typing
  41.147 +          cons (Position.reported_text pos Markup.typing
  41.148              (Syntax.string_of_typ ctxt (Logic.dest_type ty)))
  41.149          else I) ps tys' []
  41.150        |> implode;
    42.1 --- a/src/Pure/Syntax/term_position.ML	Sun Nov 25 18:50:13 2012 +0100
    42.2 +++ b/src/Pure/Syntax/term_position.ML	Sun Nov 25 19:49:24 2012 +0100
    42.3 @@ -26,15 +26,15 @@
    42.4  val position_text = XML.Text position_dummy;
    42.5  
    42.6  fun pretty pos =
    42.7 -  Pretty.markup (Position.markup pos Isabelle_Markup.position) [Pretty.str position_dummy];
    42.8 +  Pretty.markup (Position.markup pos Markup.position) [Pretty.str position_dummy];
    42.9  
   42.10  fun encode pos =
   42.11 -  YXML.string_of (XML.Elem (Position.markup pos Isabelle_Markup.position, [position_text]));
   42.12 +  YXML.string_of (XML.Elem (Position.markup pos Markup.position, [position_text]));
   42.13  
   42.14  fun decode str =
   42.15    (case YXML.parse_body str handle Fail msg => error msg of
   42.16      [XML.Elem ((name, props), [arg])] =>
   42.17 -      if name = Isabelle_Markup.positionN andalso arg = position_text
   42.18 +      if name = Markup.positionN andalso arg = position_text
   42.19        then SOME (Position.of_properties props)
   42.20        else NONE
   42.21    | _ => NONE);
    43.1 --- a/src/Pure/System/invoke_scala.ML	Sun Nov 25 18:50:13 2012 +0100
    43.2 +++ b/src/Pure/System/invoke_scala.ML	Sun Nov 25 19:49:24 2012 +0100
    43.3 @@ -33,10 +33,10 @@
    43.4  fun promise_method name arg =
    43.5    let
    43.6      val id = new_id ();
    43.7 -    fun abort () = Output.protocol_message (Isabelle_Markup.cancel_scala id) "";
    43.8 +    fun abort () = Output.protocol_message (Markup.cancel_scala id) "";
    43.9      val promise = Future.promise abort : string future;
   43.10      val _ = Synchronized.change promises (Symtab.update (id, promise));
   43.11 -    val _ = Output.protocol_message (Isabelle_Markup.invoke_scala name id) arg;
   43.12 +    val _ = Output.protocol_message (Markup.invoke_scala name id) arg;
   43.13    in promise end;
   43.14  
   43.15  fun method name arg = Future.join (promise_method name arg);
    44.1 --- a/src/Pure/System/isabelle_process.ML	Sun Nov 25 18:50:13 2012 +0100
    44.2 +++ b/src/Pure/System/isabelle_process.ML	Sun Nov 25 19:49:24 2012 +0100
    44.3 @@ -99,7 +99,7 @@
    44.4    if body = "" then ()
    44.5    else
    44.6      message false mbox name
    44.7 -      ((case opt_serial of SOME i => cons (Isabelle_Markup.serialN, string_of_int i) | _ => I)
    44.8 +      ((case opt_serial of SOME i => cons (Markup.serialN, string_of_int i) | _ => I)
    44.9          (Position.properties_of (Position.thread_data ()))) body;
   44.10  
   44.11  fun message_output mbox channel =
   44.12 @@ -124,22 +124,20 @@
   44.13      val mbox = Mailbox.create () : (string list * bool) Mailbox.T;
   44.14      val _ = Simple_Thread.fork false (message_output mbox channel);
   44.15    in
   44.16 -    Output.Private_Hooks.status_fn := standard_message mbox NONE Isabelle_Markup.statusN;
   44.17 -    Output.Private_Hooks.report_fn := standard_message mbox NONE Isabelle_Markup.reportN;
   44.18 +    Output.Private_Hooks.status_fn := standard_message mbox NONE Markup.statusN;
   44.19 +    Output.Private_Hooks.report_fn := standard_message mbox NONE Markup.reportN;
   44.20      Output.Private_Hooks.writeln_fn :=
   44.21 -      (fn s => standard_message mbox (SOME (serial ())) Isabelle_Markup.writelnN s);
   44.22 +      (fn s => standard_message mbox (SOME (serial ())) Markup.writelnN s);
   44.23      Output.Private_Hooks.tracing_fn :=
   44.24 -      (fn s =>
   44.25 -        (update_tracing_limits s;
   44.26 -          standard_message mbox (SOME (serial ())) Isabelle_Markup.tracingN s));
   44.27 +      (fn s => (update_tracing_limits s; standard_message mbox (SOME (serial ())) Markup.tracingN s));
   44.28      Output.Private_Hooks.warning_fn :=
   44.29 -      (fn s => standard_message mbox (SOME (serial ())) Isabelle_Markup.warningN s);
   44.30 +      (fn s => standard_message mbox (SOME (serial ())) Markup.warningN s);
   44.31      Output.Private_Hooks.error_fn :=
   44.32 -      (fn (i, s) => standard_message mbox (SOME i) Isabelle_Markup.errorN s);
   44.33 -    Output.Private_Hooks.protocol_message_fn := message true mbox Isabelle_Markup.protocolN;
   44.34 +      (fn (i, s) => standard_message mbox (SOME i) Markup.errorN s);
   44.35 +    Output.Private_Hooks.protocol_message_fn := message true mbox Markup.protocolN;
   44.36      Output.Private_Hooks.urgent_message_fn := ! Output.Private_Hooks.writeln_fn;
   44.37      Output.Private_Hooks.prompt_fn := ignore;
   44.38 -    message true mbox Isabelle_Markup.initN [] (Session.welcome ())
   44.39 +    message true mbox Markup.initN [] (Session.welcome ())
   44.40    end;
   44.41  
   44.42  end;
    45.1 --- a/src/Pure/System/isabelle_process.scala	Sun Nov 25 18:50:13 2012 +0100
    45.2 +++ b/src/Pure/System/isabelle_process.scala	Sun Nov 25 19:49:24 2012 +0100
    45.3 @@ -25,10 +25,9 @@
    45.4    class Input(name: String, args: List[String]) extends Message
    45.5    {
    45.6      override def toString: String =
    45.7 -      XML.Elem(Markup(Isabelle_Markup.PROVER_COMMAND, List((Markup.NAME, name))),
    45.8 +      XML.Elem(Markup(Markup.PROVER_COMMAND, List((Markup.NAME, name))),
    45.9          args.map(s =>
   45.10 -          List(XML.Text("\n"),
   45.11 -            XML.elem(Isabelle_Markup.PROVER_ARG, YXML.parse_body(s)))).flatten).toString
   45.12 +          List(XML.Text("\n"), XML.elem(Markup.PROVER_ARG, YXML.parse_body(s)))).flatten).toString
   45.13    }
   45.14  
   45.15    class Output(val message: XML.Elem) extends Message
   45.16 @@ -37,14 +36,14 @@
   45.17      def properties: Properties.T = message.markup.properties
   45.18      def body: XML.Body = message.body
   45.19  
   45.20 -    def is_init = kind == Isabelle_Markup.INIT
   45.21 -    def is_exit = kind == Isabelle_Markup.EXIT
   45.22 -    def is_stdout = kind == Isabelle_Markup.STDOUT
   45.23 -    def is_stderr = kind == Isabelle_Markup.STDERR
   45.24 -    def is_system = kind == Isabelle_Markup.SYSTEM
   45.25 -    def is_status = kind == Isabelle_Markup.STATUS
   45.26 -    def is_report = kind == Isabelle_Markup.REPORT
   45.27 -    def is_protocol = kind == Isabelle_Markup.PROTOCOL
   45.28 +    def is_init = kind == Markup.INIT
   45.29 +    def is_exit = kind == Markup.EXIT
   45.30 +    def is_stdout = kind == Markup.STDOUT
   45.31 +    def is_stderr = kind == Markup.STDERR
   45.32 +    def is_system = kind == Markup.SYSTEM
   45.33 +    def is_status = kind == Markup.STATUS
   45.34 +    def is_report = kind == Markup.REPORT
   45.35 +    def is_protocol = kind == Markup.PROTOCOL
   45.36      def is_syslog = is_init || is_exit || is_system || is_stderr
   45.37  
   45.38      override def toString: String =
   45.39 @@ -85,15 +84,15 @@
   45.40  
   45.41    private def system_output(text: String)
   45.42    {
   45.43 -    receiver(new Output(XML.Elem(Markup(Isabelle_Markup.SYSTEM, Nil), List(XML.Text(text)))))
   45.44 +    receiver(new Output(XML.Elem(Markup(Markup.SYSTEM, Nil), List(XML.Text(text)))))
   45.45    }
   45.46  
   45.47    private val xml_cache = new XML.Cache()
   45.48  
   45.49    private def output_message(kind: String, props: Properties.T, body: XML.Body)
   45.50    {
   45.51 -    if (kind == Isabelle_Markup.INIT) system_channel.accepted()
   45.52 -    if (kind == Isabelle_Markup.PROTOCOL)
   45.53 +    if (kind == Markup.INIT) system_channel.accepted()
   45.54 +    if (kind == Markup.PROTOCOL)
   45.55        receiver(new Output(XML.Elem(Markup(kind, props), body)))
   45.56      else {
   45.57        val main = XML.Elem(Markup(kind, props), Protocol.clean_message(body))
   45.58 @@ -105,7 +104,7 @@
   45.59  
   45.60    private def exit_message(rc: Int)
   45.61    {
   45.62 -    output_message(Isabelle_Markup.EXIT, Isabelle_Markup.Return_Code(rc),
   45.63 +    output_message(Markup.EXIT, Markup.Return_Code(rc),
   45.64        List(XML.Text("Return code: " + rc.toString)))
   45.65    }
   45.66  
   45.67 @@ -247,8 +246,8 @@
   45.68    private def physical_output_actor(err: Boolean): (Thread, Actor) =
   45.69    {
   45.70      val (name, reader, markup) =
   45.71 -      if (err) ("standard_error", process.stderr, Isabelle_Markup.STDERR)
   45.72 -      else ("standard_output", process.stdout, Isabelle_Markup.STDOUT)
   45.73 +      if (err) ("standard_error", process.stderr, Markup.STDERR)
   45.74 +      else ("standard_output", process.stdout, Markup.STDOUT)
   45.75  
   45.76      Simple_Thread.actor(name) {
   45.77        try {
   45.78 @@ -364,7 +363,7 @@
   45.79              header match {
   45.80                case List(XML.Elem(Markup(name, props), Nil)) =>
   45.81                  val kind = name.intern
   45.82 -                val body = read_chunk(kind != Isabelle_Markup.PROTOCOL)
   45.83 +                val body = read_chunk(kind != Markup.PROTOCOL)
   45.84                  output_message(kind, props, body)
   45.85                case _ =>
   45.86                  read_chunk(false)
    46.1 --- a/src/Pure/System/session.scala	Sun Nov 25 18:50:13 2012 +0100
    46.2 +++ b/src/Pure/System/session.scala	Sun Nov 25 19:49:24 2012 +0100
    46.3 @@ -314,7 +314,7 @@
    46.4              case _: Document.State.Fail => bad_output(output)
    46.5            }
    46.6  
    46.7 -        case Isabelle_Markup.Assign_Execs if output.is_protocol =>
    46.8 +        case Markup.Assign_Execs if output.is_protocol =>
    46.9            XML.content(output.body) match {
   46.10              case Protocol.Assign(id, assign) =>
   46.11                try {
   46.12 @@ -331,7 +331,7 @@
   46.13              prune_next = System.currentTimeMillis() + prune_delay.ms
   46.14            }
   46.15  
   46.16 -        case Isabelle_Markup.Removed_Versions if output.is_protocol =>
   46.17 +        case Markup.Removed_Versions if output.is_protocol =>
   46.18            XML.content(output.body) match {
   46.19              case Protocol.Removed(removed) =>
   46.20                try {
   46.21 @@ -341,7 +341,7 @@
   46.22              case _ => bad_output(output)
   46.23            }
   46.24  
   46.25 -        case Isabelle_Markup.Invoke_Scala(name, id) if output.is_protocol =>
   46.26 +        case Markup.Invoke_Scala(name, id) if output.is_protocol =>
   46.27            futures += (id ->
   46.28              default_thread_pool.submit(() =>
   46.29                {
   46.30 @@ -350,7 +350,7 @@
   46.31                  this_actor ! Finished_Scala(id, tag, result)
   46.32                }))
   46.33  
   46.34 -        case Isabelle_Markup.Cancel_Scala(id) if output.is_protocol =>
   46.35 +        case Markup.Cancel_Scala(id) if output.is_protocol =>
   46.36            futures.get(id) match {
   46.37              case Some(future) =>
   46.38                future.cancel(true)
   46.39 @@ -361,7 +361,7 @@
   46.40          case _ if output.is_init =>
   46.41              phase = Session.Ready
   46.42  
   46.43 -        case Isabelle_Markup.Return_Code(rc) if output.is_exit =>
   46.44 +        case Markup.Return_Code(rc) if output.is_exit =>
   46.45            if (rc == 0) phase = Session.Inactive
   46.46            else phase = Session.Failed
   46.47  
    47.1 --- a/src/Pure/Thy/html.ML	Sun Nov 25 18:50:13 2012 +0100
    47.2 +++ b/src/Pure/Thy/html.ML	Sun Nov 25 19:49:24 2012 +0100
    47.3 @@ -54,7 +54,7 @@
    47.4  (* symbol output *)
    47.5  
    47.6  local
    47.7 -  val hidden = span Isabelle_Markup.hiddenN |-> enclose;
    47.8 +  val hidden = span Markup.hiddenN |-> enclose;
    47.9  
   47.10    (* FIXME proper unicode -- produced on Scala side *)
   47.11    val html_syms = Symtab.make
    48.1 --- a/src/Pure/Thy/html.scala	Sun Nov 25 18:50:13 2012 +0100
    48.2 +++ b/src/Pure/Thy/html.scala	Sun Nov 25 19:49:24 2012 +0100
    48.3 @@ -51,7 +51,7 @@
    48.4      XML.Elem(Markup(SPAN, List((STYLE, "font-family: " + font))), List(XML.Text(txt)))
    48.5  
    48.6    def hidden(txt: String): XML.Elem =
    48.7 -    span(Isabelle_Markup.HIDDEN, List(XML.Text(txt)))
    48.8 +    span(Markup.HIDDEN, List(XML.Text(txt)))
    48.9  
   48.10    def sub(txt: String): XML.Elem = XML.elem("sub", List(XML.Text(txt)))
   48.11    def sup(txt: String): XML.Elem = XML.elem("sup", List(XML.Text(txt)))
    49.1 --- a/src/Pure/Thy/latex.ML	Sun Nov 25 18:50:13 2012 +0100
    49.2 +++ b/src/Pure/Thy/latex.ML	Sun Nov 25 19:49:24 2012 +0100
    49.3 @@ -178,9 +178,9 @@
    49.4    in (output_symbols syms, Symbol.length syms) end;
    49.5  
    49.6  fun latex_markup (s, _) =
    49.7 -  if s = Isabelle_Markup.commandN orelse s = Isabelle_Markup.keyword1N
    49.8 +  if s = Markup.commandN orelse s = Markup.keyword1N
    49.9      then ("\\isacommand{", "}")
   49.10 -  else if s = Isabelle_Markup.keywordN orelse s = Isabelle_Markup.keyword2N
   49.11 +  else if s = Markup.keywordN orelse s = Markup.keyword2N
   49.12      then ("\\isakeyword{", "}")
   49.13    else Markup.no_output;
   49.14  
    50.1 --- a/src/Pure/Thy/thy_load.ML	Sun Nov 25 18:50:13 2012 +0100
    50.2 +++ b/src/Pure/Thy/thy_load.ML	Sun Nov 25 19:49:24 2012 +0100
    50.3 @@ -68,7 +68,7 @@
    50.4    let
    50.5      fun make_file file =
    50.6        let
    50.7 -        val _ = Position.report pos (Isabelle_Markup.path (Path.implode file));
    50.8 +        val _ = Position.report pos (Markup.path (Path.implode file));
    50.9          val full_path = check_file dir file;
   50.10        in {src_path = file, text = File.read full_path, pos = Path.position full_path} end;
   50.11      val paths =
   50.12 @@ -285,7 +285,7 @@
   50.13          val _ =
   50.14            if File.exists path then ()
   50.15            else error ("Bad file: " ^ Path.print (Path.expand path) ^ Position.here pos);
   50.16 -        val _ = Position.report pos (Isabelle_Markup.path name);
   50.17 +        val _ = Position.report pos (Markup.path name);
   50.18        in Thy_Output.verb_text name end)));
   50.19  
   50.20  
    51.1 --- a/src/Pure/Thy/thy_output.ML	Sun Nov 25 18:50:13 2012 +0100
    51.2 +++ b/src/Pure/Thy/thy_output.ML	Sun Nov 25 19:49:24 2012 +0100
    51.3 @@ -83,8 +83,8 @@
    51.4      (Args.src -> Toplevel.state -> Proof.context -> string) Name_Space.table *
    51.5        (string -> Proof.context -> Proof.context) Name_Space.table;
    51.6    val empty : T =
    51.7 -    (Name_Space.empty_table Isabelle_Markup.document_antiquotationN,
    51.8 -      Name_Space.empty_table Isabelle_Markup.document_antiquotation_optionN);
    51.9 +    (Name_Space.empty_table Markup.document_antiquotationN,
   51.10 +      Name_Space.empty_table Markup.document_antiquotation_optionN);
   51.11    val extend = I;
   51.12    fun merge ((commands1, options1), (commands2, options2)) : T =
   51.13      (Name_Space.merge_tables (commands1, commands2),
   51.14 @@ -205,7 +205,7 @@
   51.15  
   51.16  
   51.17  fun check_text (txt, pos) state =
   51.18 - (Position.report pos Isabelle_Markup.doc_source;
   51.19 + (Position.report pos Markup.doc_source;
   51.20    ignore (eval_antiquote (#1 (Keyword.get_lexicons ())) state (txt, pos)));
   51.21  
   51.22  
    52.1 --- a/src/Pure/Thy/thy_syntax.ML	Sun Nov 25 18:50:13 2012 +0100
    52.2 +++ b/src/Pure/Thy/thy_syntax.ML	Sun Nov 25 19:49:24 2012 +0100
    52.3 @@ -38,29 +38,29 @@
    52.4  local
    52.5  
    52.6  val token_kind_markup =
    52.7 - fn Token.Command       => (Isabelle_Markup.command, "")
    52.8 -  | Token.Keyword       => (Isabelle_Markup.keyword, "")
    52.9 + fn Token.Command       => (Markup.command, "")
   52.10 +  | Token.Keyword       => (Markup.keyword, "")
   52.11    | Token.Ident         => (Markup.empty, "")
   52.12    | Token.LongIdent     => (Markup.empty, "")
   52.13    | Token.SymIdent      => (Markup.empty, "")
   52.14 -  | Token.Var           => (Isabelle_Markup.var, "")
   52.15 -  | Token.TypeIdent     => (Isabelle_Markup.tfree, "")
   52.16 -  | Token.TypeVar       => (Isabelle_Markup.tvar, "")
   52.17 +  | Token.Var           => (Markup.var, "")
   52.18 +  | Token.TypeIdent     => (Markup.tfree, "")
   52.19 +  | Token.TypeVar       => (Markup.tvar, "")
   52.20    | Token.Nat           => (Markup.empty, "")
   52.21    | Token.Float         => (Markup.empty, "")
   52.22 -  | Token.String        => (Isabelle_Markup.string, "")
   52.23 -  | Token.AltString     => (Isabelle_Markup.altstring, "")
   52.24 -  | Token.Verbatim      => (Isabelle_Markup.verbatim, "")
   52.25 +  | Token.String        => (Markup.string, "")
   52.26 +  | Token.AltString     => (Markup.altstring, "")
   52.27 +  | Token.Verbatim      => (Markup.verbatim, "")
   52.28    | Token.Space         => (Markup.empty, "")
   52.29 -  | Token.Comment       => (Isabelle_Markup.comment, "")
   52.30 +  | Token.Comment       => (Markup.comment, "")
   52.31    | Token.InternalValue => (Markup.empty, "")
   52.32 -  | Token.Error msg     => (Isabelle_Markup.bad, msg)
   52.33 -  | Token.Sync          => (Isabelle_Markup.control, "")
   52.34 -  | Token.EOF           => (Isabelle_Markup.control, "");
   52.35 +  | Token.Error msg     => (Markup.bad, msg)
   52.36 +  | Token.Sync          => (Markup.control, "")
   52.37 +  | Token.EOF           => (Markup.control, "");
   52.38  
   52.39  fun token_markup tok =
   52.40    if Token.keyword_with (not o Lexicon.is_ascii_identifier) tok
   52.41 -  then (Isabelle_Markup.operator, "")
   52.42 +  then (Markup.operator, "")
   52.43    else
   52.44      let
   52.45        val kind = Token.kind_of tok;
   52.46 @@ -77,7 +77,7 @@
   52.47        Symbol_Pos.explode (Token.source_position_of tok)
   52.48        |> map_filter (fn (sym, pos) =>
   52.49            if Symbol.is_malformed sym
   52.50 -          then SOME ((pos, Isabelle_Markup.bad), "Malformed symbolic character") else NONE);
   52.51 +          then SOME ((pos, Markup.bad), "Malformed symbolic character") else NONE);
   52.52      val is_malformed = Token.is_error tok orelse not (null malformed_symbols);
   52.53      val (markup, txt) = token_markup tok;
   52.54      val reports = ((Token.position_of tok, markup), txt) :: malformed_symbols;
    53.1 --- a/src/Pure/build-jars	Sun Nov 25 18:50:13 2012 +0100
    53.2 +++ b/src/Pure/build-jars	Sun Nov 25 19:49:24 2012 +0100
    53.3 @@ -32,7 +32,6 @@
    53.4    Isar/token.scala
    53.5    PIDE/command.scala
    53.6    PIDE/document.scala
    53.7 -  PIDE/isabelle_markup.scala
    53.8    PIDE/markup.scala
    53.9    PIDE/markup_tree.scala
   53.10    PIDE/protocol.scala
    54.1 --- a/src/Pure/consts.ML	Sun Nov 25 18:50:13 2012 +0100
    54.2 +++ b/src/Pure/consts.ML	Sun Nov 25 19:49:24 2012 +0100
    54.3 @@ -311,7 +311,7 @@
    54.4  (* empty and merge *)
    54.5  
    54.6  val empty =
    54.7 -  make_consts (Name_Space.empty_table Isabelle_Markup.constantN, Symtab.empty, Symtab.empty);
    54.8 +  make_consts (Name_Space.empty_table Markup.constantN, Symtab.empty, Symtab.empty);
    54.9  
   54.10  fun merge
   54.11     (Consts {decls = decls1, constraints = constraints1, rev_abbrevs = rev_abbrevs1},
    55.1 --- a/src/Pure/global_theory.ML	Sun Nov 25 18:50:13 2012 +0100
    55.2 +++ b/src/Pure/global_theory.ML	Sun Nov 25 19:49:24 2012 +0100
    55.3 @@ -82,7 +82,7 @@
    55.4      | SOME (static, ths) =>
    55.5          (Context_Position.report_generic context pos (Name_Space.markup (Facts.space_of facts) name);
    55.6           if static then ()
    55.7 -         else Context_Position.report_generic context pos (Isabelle_Markup.dynamic_fact name);
    55.8 +         else Context_Position.report_generic context pos (Markup.dynamic_fact name);
    55.9           Facts.select xthmref (map (Thm.transfer thy) ths)))
   55.10    end;
   55.11  
    56.1 --- a/src/Pure/goal.ML	Sun Nov 25 18:50:13 2012 +0100
    56.2 +++ b/src/Pure/goal.ML	Sun Nov 25 19:49:24 2012 +0100
    56.3 @@ -129,7 +129,7 @@
    56.4      in (m, groups', tab') end);
    56.5  
    56.6  fun status task markups =
    56.7 -  let val props = Markup.properties [(Isabelle_Markup.taskN, Task_Queue.str_of_task task)]
    56.8 +  let val props = Markup.properties [(Markup.taskN, Task_Queue.str_of_task task)]
    56.9    in Output.status (implode (map (Markup.markup_only o props) markups)) end;
   56.10  
   56.11  in
   56.12 @@ -148,21 +148,21 @@
   56.13            (fn () =>
   56.14              let
   56.15                val task = the (Future.worker_task ());
   56.16 -              val _ = status task [Isabelle_Markup.running];
   56.17 +              val _ = status task [Markup.running];
   56.18                val result = Exn.capture (Future.interruptible_task e) ();
   56.19 -              val _ = status task [Isabelle_Markup.finished, Isabelle_Markup.joined];
   56.20 +              val _ = status task [Markup.finished, Markup.joined];
   56.21                val _ =
   56.22                  (case result of
   56.23                    Exn.Res _ => ()
   56.24                  | Exn.Exn exn =>
   56.25                      if id = 0 orelse Exn.is_interrupt exn then ()
   56.26                      else
   56.27 -                      (status task [Isabelle_Markup.failed];
   56.28 -                       Output.report (Markup.markup_only Isabelle_Markup.bad);
   56.29 +                      (status task [Markup.failed];
   56.30 +                       Output.report (Markup.markup_only Markup.bad);
   56.31                         Output.error_msg (ML_Compiler.exn_message exn)));
   56.32                val _ = count_forked ~1;
   56.33              in Exn.release result end);
   56.34 -      val _ = status (Future.task_of future) [Isabelle_Markup.forked];
   56.35 +      val _ = status (Future.task_of future) [Markup.forked];
   56.36        val _ = register_forked id future;
   56.37      in future end) ();
   56.38  
    57.1 --- a/src/Pure/goal_display.ML	Sun Nov 25 18:50:13 2012 +0100
    57.2 +++ b/src/Pure/goal_display.ML	Sun Nov 25 19:49:24 2012 +0100
    57.3 @@ -116,8 +116,7 @@
    57.4        | pretty_list name prt lst = [Pretty.big_list name (map prt lst)];
    57.5  
    57.6      fun pretty_subgoal (n, A) =
    57.7 -      Pretty.markup Isabelle_Markup.subgoal
    57.8 -        [Pretty.str (" " ^ string_of_int n ^ ". "), prt_term A];
    57.9 +      Pretty.markup Markup.subgoal [Pretty.str (" " ^ string_of_int n ^ ". "), prt_term A];
   57.10      fun pretty_subgoals As = map pretty_subgoal (1 upto length As ~~ As);
   57.11  
   57.12      val pretty_ffpairs = pretty_list "flex-flex pairs:" (pretty_flexpair ctxt);
    58.1 --- a/src/Pure/theory.ML	Sun Nov 25 18:50:13 2012 +0100
    58.2 +++ b/src/Pure/theory.ML	Sun Nov 25 19:49:24 2012 +0100
    58.3 @@ -133,7 +133,7 @@
    58.4    if id = 0 then Markup.empty
    58.5    else
    58.6      Markup.properties (Position.entity_properties_of def id pos)
    58.7 -      (Isabelle_Markup.entity Isabelle_Markup.theoryN name);
    58.8 +      (Markup.entity Markup.theoryN name);
    58.9  
   58.10  fun init_markup (name, pos) thy =
   58.11    let
    59.1 --- a/src/Pure/type.ML	Sun Nov 25 18:50:13 2012 +0100
    59.2 +++ b/src/Pure/type.ML	Sun Nov 25 19:49:24 2012 +0100
    59.3 @@ -187,8 +187,8 @@
    59.4    build_tsig (f (classes, default, types));
    59.5  
    59.6  val empty_tsig =
    59.7 -  build_tsig ((Name_Space.empty Isabelle_Markup.classN, Sorts.empty_algebra), [],
    59.8 -    Name_Space.empty_table Isabelle_Markup.type_nameN);
    59.9 +  build_tsig ((Name_Space.empty Markup.classN, Sorts.empty_algebra), [],
   59.10 +    Name_Space.empty_table Markup.type_nameN);
   59.11  
   59.12  
   59.13  (* classes and sorts *)
    60.1 --- a/src/Pure/variable.ML	Sun Nov 25 18:50:13 2012 +0100
    60.2 +++ b/src/Pure/variable.ML	Sun Nov 25 19:49:24 2012 +0100
    60.3 @@ -81,7 +81,7 @@
    60.4  (** local context data **)
    60.5  
    60.6  type fixes = string Name_Space.table;
    60.7 -val empty_fixes: fixes = Name_Space.empty_table Isabelle_Markup.fixedN;
    60.8 +val empty_fixes: fixes = Name_Space.empty_table Markup.fixedN;
    60.9  
   60.10  datatype data = Data of
   60.11   {is_body: bool,                        (*inner body mode*)
    61.1 --- a/src/Tools/jEdit/src/graphview_dockable.scala	Sun Nov 25 18:50:13 2012 +0100
    61.2 +++ b/src/Tools/jEdit/src/graphview_dockable.scala	Sun Nov 25 19:49:24 2012 +0100
    61.3 @@ -81,9 +81,9 @@
    61.4      val new_graph =
    61.5        if (!restriction.isDefined || restriction.get.contains(new_state.command)) {
    61.6          new_state.markup.cumulate[Option[XML.Body]](
    61.7 -          new_state.command.range, None, Some(Set(Isabelle_Markup.GRAPHVIEW)),
    61.8 +          new_state.command.range, None, Some(Set(Markup.GRAPHVIEW)),
    61.9          {
   61.10 -          case (_, Text.Info(_, XML.Elem(Markup(Isabelle_Markup.GRAPHVIEW, _), graph))) =>
   61.11 +          case (_, Text.Info(_, XML.Elem(Markup(Markup.GRAPHVIEW, _), graph))) =>
   61.12              Some(graph)
   61.13          }).filter(_.info.isDefined) match {
   61.14            case Text.Info(_, Some(graph)) #:: _ => graph
    62.1 --- a/src/Tools/jEdit/src/isabelle_rendering.scala	Sun Nov 25 18:50:13 2012 +0100
    62.2 +++ b/src/Tools/jEdit/src/isabelle_rendering.scala	Sun Nov 25 19:49:24 2012 +0100
    62.3 @@ -34,10 +34,10 @@
    62.4    private val error_pri = 5
    62.5  
    62.6    private val message_pri = Map(
    62.7 -    Isabelle_Markup.WRITELN -> writeln_pri, Isabelle_Markup.WRITELN_MESSAGE -> writeln_pri,
    62.8 -    Isabelle_Markup.TRACING -> tracing_pri, Isabelle_Markup.TRACING_MESSAGE -> tracing_pri,
    62.9 -    Isabelle_Markup.WARNING -> warning_pri, Isabelle_Markup.WARNING_MESSAGE -> warning_pri,
   62.10 -    Isabelle_Markup.ERROR -> error_pri, Isabelle_Markup.ERROR_MESSAGE -> error_pri)
   62.11 +    Markup.WRITELN -> writeln_pri, Markup.WRITELN_MESSAGE -> writeln_pri,
   62.12 +    Markup.TRACING -> tracing_pri, Markup.TRACING_MESSAGE -> tracing_pri,
   62.13 +    Markup.WARNING -> warning_pri, Markup.WARNING_MESSAGE -> warning_pri,
   62.14 +    Markup.ERROR -> error_pri, Markup.ERROR_MESSAGE -> error_pri)
   62.15  
   62.16  
   62.17    /* icons */
   62.18 @@ -156,10 +156,10 @@
   62.19        val results =
   62.20          snapshot.cumulate_markup[(Protocol.Status, Int)](
   62.21            range, (Protocol.Status.init, 0),
   62.22 -          Some(Protocol.command_status_markup + Isabelle_Markup.WARNING + Isabelle_Markup.ERROR),
   62.23 +          Some(Protocol.command_status_markup + Markup.WARNING + Markup.ERROR),
   62.24            {
   62.25              case ((status, pri), Text.Info(_, XML.Elem(markup, _))) =>
   62.26 -              if (markup.name == Isabelle_Markup.WARNING || markup.name == Isabelle_Markup.ERROR)
   62.27 +              if (markup.name == Markup.WARNING || markup.name == Markup.ERROR)
   62.28                  (status, pri max Rendering.message_pri(markup.name))
   62.29                else (Protocol.command_status(status, markup), pri)
   62.30            })
   62.31 @@ -183,11 +183,9 @@
   62.32    /* markup selectors */
   62.33  
   62.34    private val highlight_include =
   62.35 -    Set(Isabelle_Markup.SORT, Isabelle_Markup.TYP, Isabelle_Markup.TERM, Isabelle_Markup.PROP,
   62.36 -      Isabelle_Markup.ML_TYPING, Isabelle_Markup.TOKEN_RANGE, Isabelle_Markup.ENTITY,
   62.37 -      Isabelle_Markup.PATH, Isabelle_Markup.SORTING, Isabelle_Markup.TYPING, Isabelle_Markup.FREE,
   62.38 -      Isabelle_Markup.SKOLEM, Isabelle_Markup.BOUND, Isabelle_Markup.VAR, Isabelle_Markup.TFREE,
   62.39 -      Isabelle_Markup.TVAR, Isabelle_Markup.ML_SOURCE, Isabelle_Markup.DOCUMENT_SOURCE)
   62.40 +    Set(Markup.SORT, Markup.TYP, Markup.TERM, Markup.PROP, Markup.ML_TYPING, Markup.TOKEN_RANGE,
   62.41 +      Markup.ENTITY, Markup.PATH, Markup.SORTING, Markup.TYPING, Markup.FREE, Markup.SKOLEM,
   62.42 +      Markup.BOUND, Markup.VAR, Markup.TFREE, Markup.TVAR, Markup.ML_SOURCE, Markup.DOCUMENT_SOURCE)
   62.43  
   62.44    def highlight(range: Text.Range): Option[Text.Info[Color]] =
   62.45    {
   62.46 @@ -199,21 +197,21 @@
   62.47    }
   62.48  
   62.49  
   62.50 -  private val hyperlink_include = Set(Isabelle_Markup.ENTITY, Isabelle_Markup.PATH)
   62.51 +  private val hyperlink_include = Set(Markup.ENTITY, Markup.PATH)
   62.52  
   62.53    def hyperlink(range: Text.Range): Option[Text.Info[Hyperlink]] =
   62.54    {
   62.55      snapshot.cumulate_markup[List[Text.Info[Hyperlink]]](range, Nil, Some(hyperlink_include),
   62.56          {
   62.57 -          case (links, Text.Info(info_range, XML.Elem(Isabelle_Markup.Path(name), _)))
   62.58 +          case (links, Text.Info(info_range, XML.Elem(Markup.Path(name), _)))
   62.59            if Path.is_ok(name) =>
   62.60              val jedit_file = Isabelle.thy_load.append(snapshot.node_name.dir, Path.explode(name))
   62.61              Text.Info(snapshot.convert(info_range), Hyperlink(jedit_file, 0, 0)) :: links
   62.62  
   62.63 -          case (links, Text.Info(info_range, XML.Elem(Markup(Isabelle_Markup.ENTITY, props), _)))
   62.64 +          case (links, Text.Info(info_range, XML.Elem(Markup(Markup.ENTITY, props), _)))
   62.65            if !props.exists(
   62.66 -            { case (Markup.KIND, Isabelle_Markup.ML_OPEN) => true
   62.67 -              case (Markup.KIND, Isabelle_Markup.ML_STRUCT) => true
   62.68 +            { case (Markup.KIND, Markup.ML_OPEN) => true
   62.69 +              case (Markup.KIND, Markup.ML_STRUCT) => true
   62.70                case _ => false }) =>
   62.71  
   62.72              props match {
   62.73 @@ -244,9 +242,9 @@
   62.74  
   62.75  
   62.76    def sendback(range: Text.Range): Option[Text.Info[Option[Document.Exec_ID]]] =
   62.77 -    snapshot.select_markup(range, Some(Set(Isabelle_Markup.SENDBACK)),
   62.78 +    snapshot.select_markup(range, Some(Set(Markup.SENDBACK)),
   62.79          {
   62.80 -          case Text.Info(info_range, XML.Elem(Markup(Isabelle_Markup.SENDBACK, props), _)) =>
   62.81 +          case Text.Info(info_range, XML.Elem(Markup(Markup.SENDBACK, props), _)) =>
   62.82              Text.Info(snapshot.convert(info_range), Position.Id.unapply(props))
   62.83          }) match { case Text.Info(_, info) #:: _ => Some(info) case _ => None }
   62.84  
   62.85 @@ -255,16 +253,14 @@
   62.86    {
   62.87      val msgs =
   62.88        snapshot.cumulate_markup[SortedMap[Long, XML.Tree]](range, SortedMap.empty,
   62.89 -        Some(Set(Isabelle_Markup.WRITELN, Isabelle_Markup.WARNING, Isabelle_Markup.ERROR,
   62.90 -          Isabelle_Markup.BAD)),
   62.91 +        Some(Set(Markup.WRITELN, Markup.WARNING, Markup.ERROR, Markup.BAD)),
   62.92          {
   62.93 -          case (msgs, Text.Info(_,
   62.94 -            XML.Elem(Markup(name, props @ Isabelle_Markup.Serial(serial)), body)))
   62.95 -          if name == Isabelle_Markup.WRITELN ||
   62.96 -              name == Isabelle_Markup.WARNING ||
   62.97 -              name == Isabelle_Markup.ERROR =>
   62.98 -            msgs + (serial -> XML.Elem(Markup(Isabelle_Markup.message(name), props), body))
   62.99 -          case (msgs, Text.Info(_, msg @ XML.Elem(Markup(Isabelle_Markup.BAD, _), body)))
  62.100 +          case (msgs, Text.Info(_, XML.Elem(Markup(name, props @ Markup.Serial(serial)), body)))
  62.101 +          if name == Markup.WRITELN ||
  62.102 +              name == Markup.WARNING ||
  62.103 +              name == Markup.ERROR =>
  62.104 +            msgs + (serial -> XML.Elem(Markup(Markup.message(name), props), body))
  62.105 +          case (msgs, Text.Info(_, msg @ XML.Elem(Markup(Markup.BAD, _), body)))
  62.106            if !body.isEmpty => msgs + (Document.new_id() -> msg)
  62.107          }).toList.flatMap(_.info)
  62.108      Pretty.separate(msgs.iterator.map(_._2).toList)
  62.109 @@ -273,23 +269,23 @@
  62.110  
  62.111    private val tooltips: Map[String, String] =
  62.112      Map(
  62.113 -      Isabelle_Markup.SORT -> "sort",
  62.114 -      Isabelle_Markup.TYP -> "type",
  62.115 -      Isabelle_Markup.TERM -> "term",
  62.116 -      Isabelle_Markup.PROP -> "proposition",
  62.117 -      Isabelle_Markup.TOKEN_RANGE -> "inner syntax token",
  62.118 -      Isabelle_Markup.FREE -> "free variable",
  62.119 -      Isabelle_Markup.SKOLEM -> "skolem variable",
  62.120 -      Isabelle_Markup.BOUND -> "bound variable",
  62.121 -      Isabelle_Markup.VAR -> "schematic variable",
  62.122 -      Isabelle_Markup.TFREE -> "free type variable",
  62.123 -      Isabelle_Markup.TVAR -> "schematic type variable",
  62.124 -      Isabelle_Markup.ML_SOURCE -> "ML source",
  62.125 -      Isabelle_Markup.DOCUMENT_SOURCE -> "document source")
  62.126 +      Markup.SORT -> "sort",
  62.127 +      Markup.TYP -> "type",
  62.128 +      Markup.TERM -> "term",
  62.129 +      Markup.PROP -> "proposition",
  62.130 +      Markup.TOKEN_RANGE -> "inner syntax token",
  62.131 +      Markup.FREE -> "free variable",
  62.132 +      Markup.SKOLEM -> "skolem variable",
  62.133 +      Markup.BOUND -> "bound variable",
  62.134 +      Markup.VAR -> "schematic variable",
  62.135 +      Markup.TFREE -> "free type variable",
  62.136 +      Markup.TVAR -> "schematic type variable",
  62.137 +      Markup.ML_SOURCE -> "ML source",
  62.138 +      Markup.DOCUMENT_SOURCE -> "document source")
  62.139  
  62.140    private val tooltip_elements =
  62.141 -    Set(Isabelle_Markup.ENTITY, Isabelle_Markup.SORTING, Isabelle_Markup.TYPING,
  62.142 -      Isabelle_Markup.ML_TYPING, Isabelle_Markup.PATH) ++ tooltips.keys
  62.143 +    Set(Markup.ENTITY, Markup.SORTING, Markup.TYPING, Markup.ML_TYPING, Markup.PATH) ++
  62.144 +      tooltips.keys
  62.145  
  62.146    private def pretty_typing(kind: String, body: XML.Body): XML.Tree =
  62.147      Pretty.block(XML.Text(kind) :: Pretty.Break(1) :: body)
  62.148 @@ -303,17 +299,17 @@
  62.149        snapshot.cumulate_markup[Text.Info[(List[(Boolean, XML.Tree)])]](
  62.150          range, Text.Info(range, Nil), Some(tooltip_elements),
  62.151          {
  62.152 -          case (prev, Text.Info(r, XML.Elem(Isabelle_Markup.Entity(kind, name), _))) =>
  62.153 +          case (prev, Text.Info(r, XML.Elem(Markup.Entity(kind, name), _))) =>
  62.154              val kind1 = space_explode('_', kind).mkString(" ")
  62.155              add(prev, r, (true, XML.Text(kind1 + " " + quote(name))))
  62.156 -          case (prev, Text.Info(r, XML.Elem(Isabelle_Markup.Path(name), _)))
  62.157 +          case (prev, Text.Info(r, XML.Elem(Markup.Path(name), _)))
  62.158            if Path.is_ok(name) =>
  62.159              val jedit_file = Isabelle.thy_load.append(snapshot.node_name.dir, Path.explode(name))
  62.160              add(prev, r, (true, XML.Text("file " + quote(jedit_file))))
  62.161            case (prev, Text.Info(r, XML.Elem(Markup(name, _), body)))
  62.162 -          if name == Isabelle_Markup.SORTING || name == Isabelle_Markup.TYPING =>
  62.163 +          if name == Markup.SORTING || name == Markup.TYPING =>
  62.164              add(prev, r, (true, pretty_typing("::", body)))
  62.165 -          case (prev, Text.Info(r, XML.Elem(Markup(Isabelle_Markup.ML_TYPING, _), body))) =>
  62.166 +          case (prev, Text.Info(r, XML.Elem(Markup(Markup.ML_TYPING, _), body))) =>
  62.167              add(prev, r, (false, pretty_typing("ML:", body)))
  62.168            case (prev, Text.Info(r, XML.Elem(Markup(name, _), _)))
  62.169            if tooltips.isDefinedAt(name) => add(prev, r, (true, XML.Text(tooltips(name))))
  62.170 @@ -328,16 +324,15 @@
  62.171    def gutter_message(range: Text.Range): Option[Icon] =
  62.172    {
  62.173      val results =
  62.174 -      snapshot.cumulate_markup[Int](range, 0,
  62.175 -        Some(Set(Isabelle_Markup.WARNING, Isabelle_Markup.ERROR)),
  62.176 +      snapshot.cumulate_markup[Int](range, 0, Some(Set(Markup.WARNING, Markup.ERROR)),
  62.177          {
  62.178 -          case (pri, Text.Info(_, XML.Elem(Markup(Isabelle_Markup.WARNING, _), body))) =>
  62.179 +          case (pri, Text.Info(_, XML.Elem(Markup(Markup.WARNING, _), body))) =>
  62.180              body match {
  62.181 -              case List(XML.Elem(Markup(Isabelle_Markup.LEGACY, _), _)) =>
  62.182 +              case List(XML.Elem(Markup(Markup.LEGACY, _), _)) =>
  62.183                  pri max Rendering.legacy_pri
  62.184                case _ => pri max Rendering.warning_pri
  62.185              }
  62.186 -          case (pri, Text.Info(_, XML.Elem(Markup(Isabelle_Markup.ERROR, _), _))) =>
  62.187 +          case (pri, Text.Info(_, XML.Elem(Markup(Markup.ERROR, _), _))) =>
  62.188              pri max Rendering.error_pri
  62.189          })
  62.190      val pri = (0 /: results) { case (p1, Text.Info(_, p2)) => p1 max p2 }
  62.191 @@ -354,12 +349,12 @@
  62.192    {
  62.193      val results =
  62.194        snapshot.cumulate_markup[Int](range, 0,
  62.195 -        Some(Set(Isabelle_Markup.WRITELN, Isabelle_Markup.WARNING, Isabelle_Markup.ERROR)),
  62.196 +        Some(Set(Markup.WRITELN, Markup.WARNING, Markup.ERROR)),
  62.197          {
  62.198            case (pri, Text.Info(_, XML.Elem(Markup(name, _), _)))
  62.199 -          if name == Isabelle_Markup.WRITELN ||
  62.200 -            name == Isabelle_Markup.WARNING ||
  62.201 -            name == Isabelle_Markup.ERROR => pri max Rendering.message_pri(name)
  62.202 +          if name == Markup.WRITELN ||
  62.203 +            name == Markup.WARNING ||
  62.204 +            name == Markup.ERROR => pri max Rendering.message_pri(name)
  62.205          })
  62.206      for {
  62.207        Text.Info(r, pri) <- results
  62.208 @@ -369,8 +364,7 @@
  62.209  
  62.210  
  62.211    private val messages_include =
  62.212 -    Set(Isabelle_Markup.WRITELN_MESSAGE, Isabelle_Markup.TRACING_MESSAGE,
  62.213 -      Isabelle_Markup.WARNING_MESSAGE, Isabelle_Markup.ERROR_MESSAGE)
  62.214 +    Set(Markup.WRITELN_MESSAGE, Markup.TRACING_MESSAGE, Markup.WARNING_MESSAGE, Markup.ERROR_MESSAGE)
  62.215  
  62.216    private val message_colors = Map(
  62.217      Rendering.writeln_pri -> writeln_message_color,
  62.218 @@ -384,17 +378,17 @@
  62.219        snapshot.cumulate_markup[Int](range, 0, Some(messages_include),
  62.220          {
  62.221            case (pri, Text.Info(_, XML.Elem(Markup(name, _), _)))
  62.222 -          if name == Isabelle_Markup.WRITELN_MESSAGE ||
  62.223 -            name == Isabelle_Markup.TRACING_MESSAGE ||
  62.224 -            name == Isabelle_Markup.WARNING_MESSAGE ||
  62.225 -            name == Isabelle_Markup.ERROR_MESSAGE => pri max Rendering.message_pri(name)
  62.226 +          if name == Markup.WRITELN_MESSAGE ||
  62.227 +            name == Markup.TRACING_MESSAGE ||
  62.228 +            name == Markup.WARNING_MESSAGE ||
  62.229 +            name == Markup.ERROR_MESSAGE => pri max Rendering.message_pri(name)
  62.230          })
  62.231      val pri = (0 /: results) { case (p1, Text.Info(_, p2)) => p1 max p2 }
  62.232  
  62.233      val is_separator = pri > 0 &&
  62.234 -      snapshot.cumulate_markup[Boolean](range, false, Some(Set(Isabelle_Markup.SEPARATOR)),
  62.235 +      snapshot.cumulate_markup[Boolean](range, false, Some(Set(Markup.SEPARATOR)),
  62.236          {
  62.237 -          case (_, Text.Info(_, XML.Elem(Markup(Isabelle_Markup.SEPARATOR, _), _))) => true
  62.238 +          case (_, Text.Info(_, XML.Elem(Markup(Markup.SEPARATOR, _), _))) => true
  62.239          }).exists(_.info)
  62.240  
  62.241      message_colors.get(pri).map((_, is_separator))
  62.242 @@ -402,10 +396,9 @@
  62.243  
  62.244  
  62.245    private val background1_include =
  62.246 -    Protocol.command_status_markup + Isabelle_Markup.WRITELN_MESSAGE +
  62.247 -      Isabelle_Markup.TRACING_MESSAGE + Isabelle_Markup.WARNING_MESSAGE +
  62.248 -      Isabelle_Markup.ERROR_MESSAGE + Isabelle_Markup.BAD + Isabelle_Markup.INTENSIFY +
  62.249 -      Isabelle_Markup.SENDBACK
  62.250 +    Protocol.command_status_markup + Markup.WRITELN_MESSAGE + Markup.TRACING_MESSAGE +
  62.251 +      Markup.WARNING_MESSAGE + Markup.ERROR_MESSAGE + Markup.BAD + Markup.INTENSIFY +
  62.252 +      Markup.SENDBACK
  62.253  
  62.254    def background1(range: Text.Range): Stream[Text.Info[Color]] =
  62.255    {
  62.256 @@ -419,11 +412,11 @@
  62.257                case (((Some(status), color), Text.Info(_, XML.Elem(markup, _))))
  62.258                if (Protocol.command_status_markup(markup.name)) =>
  62.259                  (Some(Protocol.command_status(status, markup)), color)
  62.260 -              case (_, Text.Info(_, XML.Elem(Markup(Isabelle_Markup.BAD, _), _))) =>
  62.261 +              case (_, Text.Info(_, XML.Elem(Markup(Markup.BAD, _), _))) =>
  62.262                  (None, Some(bad_color))
  62.263 -              case (_, Text.Info(_, XML.Elem(Markup(Isabelle_Markup.INTENSIFY, _), _))) =>
  62.264 +              case (_, Text.Info(_, XML.Elem(Markup(Markup.INTENSIFY, _), _))) =>
  62.265                  (None, Some(intensify_color))
  62.266 -              case (_, Text.Info(_, XML.Elem(Markup(Isabelle_Markup.SENDBACK, _), _))) =>
  62.267 +              case (_, Text.Info(_, XML.Elem(Markup(Markup.SENDBACK, _), _))) =>
  62.268                  (None, Some(sendback_color))
  62.269              })
  62.270          color <-
  62.271 @@ -439,47 +432,45 @@
  62.272  
  62.273  
  62.274    def background2(range: Text.Range): Stream[Text.Info[Color]] =
  62.275 -    snapshot.select_markup(range,
  62.276 -      Some(Set(Isabelle_Markup.TOKEN_RANGE)),
  62.277 +    snapshot.select_markup(range, Some(Set(Markup.TOKEN_RANGE)),
  62.278        {
  62.279 -        case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.TOKEN_RANGE, _), _)) => light_color
  62.280 +        case Text.Info(_, XML.Elem(Markup(Markup.TOKEN_RANGE, _), _)) => light_color
  62.281        })
  62.282  
  62.283  
  62.284    def foreground(range: Text.Range): Stream[Text.Info[Color]] =
  62.285 -    snapshot.select_markup(range,
  62.286 -      Some(Set(Isabelle_Markup.STRING, Isabelle_Markup.ALTSTRING, Isabelle_Markup.VERBATIM)),
  62.287 +    snapshot.select_markup(range, Some(Set(Markup.STRING, Markup.ALTSTRING, Markup.VERBATIM)),
  62.288        {
  62.289 -        case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.STRING, _), _)) => quoted_color
  62.290 -        case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.ALTSTRING, _), _)) => quoted_color
  62.291 -        case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.VERBATIM, _), _)) => quoted_color
  62.292 +        case Text.Info(_, XML.Elem(Markup(Markup.STRING, _), _)) => quoted_color
  62.293 +        case Text.Info(_, XML.Elem(Markup(Markup.ALTSTRING, _), _)) => quoted_color
  62.294 +        case Text.Info(_, XML.Elem(Markup(Markup.VERBATIM, _), _)) => quoted_color
  62.295        })
  62.296  
  62.297  
  62.298    private val text_colors: Map[String, Color] = Map(
  62.299 -      Isabelle_Markup.KEYWORD1 -> keyword1_color,
  62.300 -      Isabelle_Markup.KEYWORD2 -> keyword2_color,
  62.301 -      Isabelle_Markup.STRING -> Color.BLACK,
  62.302 -      Isabelle_Markup.ALTSTRING -> Color.BLACK,
  62.303 -      Isabelle_Markup.VERBATIM -> Color.BLACK,
  62.304 -      Isabelle_Markup.LITERAL -> keyword1_color,
  62.305 -      Isabelle_Markup.DELIMITER -> Color.BLACK,
  62.306 -      Isabelle_Markup.TFREE -> tfree_color,
  62.307 -      Isabelle_Markup.TVAR -> tvar_color,
  62.308 -      Isabelle_Markup.FREE -> free_color,
  62.309 -      Isabelle_Markup.SKOLEM -> skolem_color,
  62.310 -      Isabelle_Markup.BOUND -> bound_color,
  62.311 -      Isabelle_Markup.VAR -> var_color,
  62.312 -      Isabelle_Markup.INNER_STRING -> inner_quoted_color,
  62.313 -      Isabelle_Markup.INNER_COMMENT -> inner_comment_color,
  62.314 -      Isabelle_Markup.DYNAMIC_FACT -> dynamic_color,
  62.315 -      Isabelle_Markup.ML_KEYWORD -> keyword1_color,
  62.316 -      Isabelle_Markup.ML_DELIMITER -> Color.BLACK,
  62.317 -      Isabelle_Markup.ML_NUMERAL -> inner_numeral_color,
  62.318 -      Isabelle_Markup.ML_CHAR -> inner_quoted_color,
  62.319 -      Isabelle_Markup.ML_STRING -> inner_quoted_color,
  62.320 -      Isabelle_Markup.ML_COMMENT -> inner_comment_color,
  62.321 -      Isabelle_Markup.ANTIQ -> antiquotation_color)
  62.322 +      Markup.KEYWORD1 -> keyword1_color,
  62.323 +      Markup.KEYWORD2 -> keyword2_color,
  62.324 +      Markup.STRING -> Color.BLACK,
  62.325 +      Markup.ALTSTRING -> Color.BLACK,
  62.326 +      Markup.VERBATIM -> Color.BLACK,
  62.327 +      Markup.LITERAL -> keyword1_color,
  62.328 +      Markup.DELIMITER -> Color.BLACK,
  62.329 +      Markup.TFREE -> tfree_color,
  62.330 +      Markup.TVAR -> tvar_color,
  62.331 +      Markup.FREE -> free_color,
  62.332 +      Markup.SKOLEM -> skolem_color,
  62.333 +      Markup.BOUND -> bound_color,
  62.334 +      Markup.VAR -> var_color,
  62.335 +      Markup.INNER_STRING -> inner_quoted_color,
  62.336 +      Markup.INNER_COMMENT -> inner_comment_color,
  62.337 +      Markup.DYNAMIC_FACT -> dynamic_color,
  62.338 +      Markup.ML_KEYWORD -> keyword1_color,
  62.339 +      Markup.ML_DELIMITER -> Color.BLACK,
  62.340 +      Markup.ML_NUMERAL -> inner_numeral_color,
  62.341 +      Markup.ML_CHAR -> inner_quoted_color,
  62.342 +      Markup.ML_STRING -> inner_quoted_color,
  62.343 +      Markup.ML_COMMENT -> inner_comment_color,
  62.344 +      Markup.ANTIQ -> antiquotation_color)
  62.345  
  62.346    private val text_color_elements = Set.empty[String] ++ text_colors.keys
  62.347  
    63.1 --- a/src/Tools/quickcheck.ML	Sun Nov 25 18:50:13 2012 +0100
    63.2 +++ b/src/Tools/quickcheck.ML	Sun Nov 25 19:49:24 2012 +0100
    63.3 @@ -529,7 +529,7 @@
    63.4               state
    63.5               |> (if auto then
    63.6                     Proof.goal_message (K (Pretty.chunks [Pretty.str "",
    63.7 -                       Pretty.mark Isabelle_Markup.intensify msg]))
    63.8 +                       Pretty.mark Markup.intensify msg]))
    63.9                   else
   63.10                     tap (fn _ => Output.urgent_message (Pretty.string_of msg))))
   63.11            else
    64.1 --- a/src/Tools/solve_direct.ML	Sun Nov 25 18:50:13 2012 +0100
    64.2 +++ b/src/Tools/solve_direct.ML	Sun Nov 25 19:49:24 2012 +0100
    64.3 @@ -89,7 +89,7 @@
    64.4                 Proof.goal_message
    64.5                   (fn () =>
    64.6                     Pretty.chunks
    64.7 -                    [Pretty.str "", Pretty.markup Isabelle_Markup.intensify (message results)])
    64.8 +                    [Pretty.str "", Pretty.markup Markup.intensify (message results)])
    64.9               else
   64.10                 tap (fn _ =>
   64.11                   Output.urgent_message (Pretty.string_of (Pretty.chunks (message results))))))