separate module for concrete Isabelle markup;
authorwenzelm
Mon Nov 28 22:05:32 2011 +0100 (2011-11-28 ago)
changeset 45666d83797ef0d2d
parent 45665 129db1416717
child 45667 546d78f0d81f
separate module for concrete Isabelle markup;
src/HOL/Library/Sum_of_Squares/sos_wrapper.ML
src/HOL/Statespace/StateSpaceEx.thy
src/HOL/Tools/ATP/atp_reconstruct.ML
src/HOL/Tools/Nitpick/nitpick.ML
src/HOL/Tools/Sledgehammer/sledgehammer_run.ML
src/HOL/Tools/try_methods.ML
src/Pure/Concurrent/future.ML
src/Pure/General/antiquote.ML
src/Pure/General/binding.ML
src/Pure/General/isabelle_markup.ML
src/Pure/General/isabelle_markup.scala
src/Pure/General/markup.ML
src/Pure/General/markup.scala
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/IsaMakefile
src/Pure/Isar/isar_cmd.ML
src/Pure/Isar/keyword.ML
src/Pure/Isar/keyword.scala
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-5.3.ML
src/Pure/ML/ml_context.ML
src/Pure/ML/ml_lex.ML
src/Pure/PIDE/command.scala
src/Pure/PIDE/document.ML
src/Pure/PIDE/isar_document.ML
src/Pure/PIDE/isar_document.scala
src/Pure/PIDE/yxml.scala
src/Pure/ProofGeneral/proof_general_emacs.ML
src/Pure/ProofGeneral/proof_general_pgip.ML
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_info.ML
src/Pure/Thy/thy_info.scala
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_display.ML
src/Pure/type.ML
src/Pure/variable.ML
src/Tools/jEdit/src/html_panel.scala
src/Tools/jEdit/src/isabelle_hyperlinks.scala
src/Tools/jEdit/src/isabelle_rendering.scala
src/Tools/jEdit/src/output_dockable.scala
src/Tools/quickcheck.ML
src/Tools/solve_direct.ML
     1.1 --- a/src/HOL/Library/Sum_of_Squares/sos_wrapper.ML	Mon Nov 28 20:39:08 2011 +0100
     1.2 +++ b/src/HOL/Library/Sum_of_Squares/sos_wrapper.ML	Mon Nov 28 22:05:32 2011 +0100
     1.3 @@ -130,7 +130,7 @@
     1.4  
     1.5  fun output_line cert =
     1.6    "To repeat this proof with a certifiate use this command:\n" ^
     1.7 -    Markup.markup Markup.sendback ("by (sos_cert \"" ^ cert ^ "\")")
     1.8 +    Markup.markup Isabelle_Markup.sendback ("by (sos_cert \"" ^ cert ^ "\")")
     1.9  
    1.10  val print_cert = warning o output_line o PositivstellensatzTools.pss_tree_to_cert
    1.11  
     2.1 --- a/src/HOL/Statespace/StateSpaceEx.thy	Mon Nov 28 20:39:08 2011 +0100
     2.2 +++ b/src/HOL/Statespace/StateSpaceEx.thy	Mon Nov 28 22:05:32 2011 +0100
     2.3 @@ -235,7 +235,7 @@
     2.4  
     2.5  ML {*
     2.6    fun make_benchmark n =
     2.7 -    writeln (Markup.markup Markup.sendback
     2.8 +    writeln (Markup.markup Isabelle_Markup.sendback
     2.9        ("statespace benchmark" ^ string_of_int n ^ " =\n" ^
    2.10          (cat_lines (map (fn i => "A" ^ string_of_int i ^ "::nat") (1 upto n)))));
    2.11  *}
     3.1 --- a/src/HOL/Tools/ATP/atp_reconstruct.ML	Mon Nov 28 20:39:08 2011 +0100
     3.2 +++ b/src/HOL/Tools/ATP/atp_reconstruct.ML	Mon Nov 28 22:05:32 2011 +0100
     3.3 @@ -233,7 +233,7 @@
     3.4      name |> not (Lexicon.is_identifier name) ? enclose "(" ")"
     3.5    | command_call name args = "(" ^ name ^ " " ^ space_implode " " args ^ ")"
     3.6  fun try_command_line banner time command =
     3.7 -  banner ^ ": " ^ Markup.markup Markup.sendback command ^ show_time time ^ "."
     3.8 +  banner ^ ": " ^ Markup.markup Isabelle_Markup.sendback command ^ show_time time ^ "."
     3.9  fun using_labels [] = ""
    3.10    | using_labels ls =
    3.11      "using " ^ space_implode " " (map string_for_label ls) ^ " "
    3.12 @@ -244,7 +244,7 @@
    3.13    | minimize_line minimize_command ss =
    3.14      case minimize_command ss of
    3.15        "" => ""
    3.16 -    | command => "\nTo minimize: " ^ Markup.markup Markup.sendback command ^ "."
    3.17 +    | command => "\nTo minimize: " ^ Markup.markup Isabelle_Markup.sendback command ^ "."
    3.18  
    3.19  val split_used_facts =
    3.20    List.partition (curry (op =) Chained o snd)
    3.21 @@ -1048,7 +1048,7 @@
    3.22        | proof =>
    3.23          "\n\n" ^ (if isar_proof_requested then "Structured proof"
    3.24                    else "Perhaps this will work") ^
    3.25 -        ":\n" ^ Markup.markup Markup.sendback proof
    3.26 +        ":\n" ^ Markup.markup Isabelle_Markup.sendback proof
    3.27      val isar_proof =
    3.28        if debug then
    3.29          isar_proof_for ()
     4.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML	Mon Nov 28 20:39:08 2011 +0100
     4.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML	Mon Nov 28 22:05:32 2011 +0100
     4.3 @@ -239,7 +239,7 @@
     4.4        if mode = Auto_Try then
     4.5          Unsynchronized.change state_ref o Proof.goal_message o K
     4.6          o Pretty.chunks o cons (Pretty.str "") o single
     4.7 -        o Pretty.mark Markup.hilite
     4.8 +        o Pretty.mark Isabelle_Markup.hilite
     4.9        else
    4.10          (fn s => (Output.urgent_message s; if debug then tracing s else ()))
    4.11          o Pretty.string_of
    4.12 @@ -459,7 +459,7 @@
    4.13                pprint_n (fn () => Pretty.blk (0,
    4.14                    pstrs "Hint: To check that the induction hypothesis is \
    4.15                          \general enough, try this command: " @
    4.16 -                  [Pretty.mark Markup.sendback (Pretty.blk (0,
    4.17 +                  [Pretty.mark Isabelle_Markup.sendback (Pretty.blk (0,
    4.18                         pstrs ("nitpick [non_std, show_all]")))] @ pstrs "."))
    4.19              else
    4.20                ()
     5.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Mon Nov 28 20:39:08 2011 +0100
     5.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Mon Nov 28 22:05:32 2011 +0100
     5.3 @@ -238,7 +238,7 @@
     5.4           |> outcome_code = someN
     5.5              ? Proof.goal_message (fn () =>
     5.6                    [Pretty.str "",
     5.7 -                   Pretty.mark Markup.hilite (Pretty.str (message ()))]
     5.8 +                   Pretty.mark Isabelle_Markup.hilite (Pretty.str (message ()))]
     5.9                    |> Pretty.chunks))
    5.10        end
    5.11      else if blocking then
     6.1 --- a/src/HOL/Tools/try_methods.ML	Mon Nov 28 20:39:08 2011 +0100
     6.2 +++ b/src/HOL/Tools/try_methods.ML	Mon Nov 28 22:05:32 2011 +0100
     6.3 @@ -138,7 +138,7 @@
     6.4               Auto_Try => "Auto Try Methods found a proof"
     6.5             | Try => "Try Methods found a proof"
     6.6             | Normal => "Try this") ^ ": " ^
     6.7 -          Markup.markup Markup.sendback
     6.8 +          Markup.markup Isabelle_Markup.sendback
     6.9                ((if nprems_of (#goal (Proof.goal st)) = 1 then "by"
    6.10                  else "apply") ^ " " ^ (s |> need_parens ? enclose "(" ")")) ^
    6.11            "\n(" ^ space_implode "; " (map time_string xs) ^ ").\n"
    6.12 @@ -146,7 +146,7 @@
    6.13          (true, (s, st |> (if mode = Auto_Try then
    6.14                              Proof.goal_message
    6.15                                  (fn () => Pretty.chunks [Pretty.str "",
    6.16 -                                          Pretty.markup Markup.hilite
    6.17 +                                          Pretty.markup Isabelle_Markup.hilite
    6.18                                                          [Pretty.str message]])
    6.19                            else
    6.20                              tap (fn _ => Output.urgent_message message))))
     7.1 --- a/src/Pure/Concurrent/future.ML	Mon Nov 28 20:39:08 2011 +0100
     7.2 +++ b/src/Pure/Concurrent/future.ML	Mon Nov 28 22:05:32 2011 +0100
     7.3 @@ -643,10 +643,10 @@
     7.4      val task_props =
     7.5        (case worker_task () of
     7.6          NONE => I
     7.7 -      | SOME task => Markup.properties [(Markup.taskN, Task_Queue.str_of_task task)]);
     7.8 -    val _ = Output.status (Markup.markup_only (task_props Markup.forked));
     7.9 +      | SOME task => Markup.properties [(Isabelle_Markup.taskN, Task_Queue.str_of_task task)]);
    7.10 +    val _ = Output.status (Markup.markup_only (task_props Isabelle_Markup.forked));
    7.11      val x = e ();  (*sic -- report "joined" only for success*)
    7.12 -    val _ = Output.status (Markup.markup_only (task_props Markup.joined));
    7.13 +    val _ = Output.status (Markup.markup_only (task_props Isabelle_Markup.joined));
    7.14    in x end;
    7.15  
    7.16  
     8.1 --- a/src/Pure/General/antiquote.ML	Mon Nov 28 20:39:08 2011 +0100
     8.2 +++ b/src/Pure/General/antiquote.ML	Mon Nov 28 22:05:32 2011 +0100
     8.3 @@ -40,9 +40,9 @@
     8.4  fun reports_of text =
     8.5    maps
     8.6      (fn Text x => text x
     8.7 -      | Antiq (_, (pos, _)) => [(pos, Markup.antiq)]
     8.8 -      | Open pos => [(pos, Markup.antiq)]
     8.9 -      | Close pos => [(pos, Markup.antiq)]);
    8.10 +      | Antiq (_, (pos, _)) => [(pos, Isabelle_Markup.antiq)]
    8.11 +      | Open pos => [(pos, Isabelle_Markup.antiq)]
    8.12 +      | Close pos => [(pos, Isabelle_Markup.antiq)]);
    8.13  
    8.14  
    8.15  (* check_nesting *)
     9.1 --- a/src/Pure/General/binding.ML	Mon Nov 28 20:39:08 2011 +0100
     9.2 +++ b/src/Pure/General/binding.ML	Mon Nov 28 22:05:32 2011 +0100
     9.3 @@ -122,7 +122,7 @@
     9.4  (* print *)
     9.5  
     9.6  fun pretty (Binding {prefix, qualifier, name, pos, ...}) =
     9.7 -  Pretty.markup (Position.markup pos Markup.binding)
     9.8 +  Pretty.markup (Position.markup pos Isabelle_Markup.binding)
     9.9      [Pretty.str (Long_Name.implode (map #1 (prefix @ qualifier) @ [name]))]
    9.10    |> Pretty.quote;
    9.11  
    10.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    10.2 +++ b/src/Pure/General/isabelle_markup.ML	Mon Nov 28 22:05:32 2011 +0100
    10.3 @@ -0,0 +1,310 @@
    10.4 +(*  Title:      Pure/General/isabelle_markup.ML
    10.5 +    Author:     Makarius
    10.6 +
    10.7 +Isabelle markup elements.
    10.8 +*)
    10.9 +
   10.10 +signature ISABELLE_MARKUP =
   10.11 +sig
   10.12 +  val bindingN: string val binding: Markup.T
   10.13 +  val entityN: string val entity: string -> string -> Markup.T
   10.14 +  val get_entity_kind: Markup.T -> string option
   10.15 +  val defN: string
   10.16 +  val refN: string
   10.17 +  val lineN: string
   10.18 +  val offsetN: string
   10.19 +  val end_offsetN: string
   10.20 +  val fileN: string
   10.21 +  val idN: string
   10.22 +  val position_properties': string list
   10.23 +  val position_properties: string list
   10.24 +  val positionN: string val position: Markup.T
   10.25 +  val pathN: string val path: string -> Markup.T
   10.26 +  val indentN: string
   10.27 +  val blockN: string val block: int -> Markup.T
   10.28 +  val widthN: string
   10.29 +  val breakN: string val break: int -> Markup.T
   10.30 +  val fbreakN: string val fbreak: Markup.T
   10.31 +  val hiddenN: string val hidden: Markup.T
   10.32 +  val classN: string
   10.33 +  val typeN: string
   10.34 +  val constantN: string
   10.35 +  val fixedN: string val fixed: string -> Markup.T
   10.36 +  val dynamic_factN: string val dynamic_fact: string -> Markup.T
   10.37 +  val tfreeN: string val tfree: Markup.T
   10.38 +  val tvarN: string val tvar: Markup.T
   10.39 +  val freeN: string val free: Markup.T
   10.40 +  val skolemN: string val skolem: Markup.T
   10.41 +  val boundN: string val bound: Markup.T
   10.42 +  val varN: string val var: Markup.T
   10.43 +  val numeralN: string val numeral: Markup.T
   10.44 +  val literalN: string val literal: Markup.T
   10.45 +  val delimiterN: string val delimiter: Markup.T
   10.46 +  val inner_stringN: string val inner_string: Markup.T
   10.47 +  val inner_commentN: string val inner_comment: Markup.T
   10.48 +  val token_rangeN: string val token_range: Markup.T
   10.49 +  val sortN: string val sort: Markup.T
   10.50 +  val typN: string val typ: Markup.T
   10.51 +  val termN: string val term: Markup.T
   10.52 +  val propN: string val prop: Markup.T
   10.53 +  val typingN: string val typing: Markup.T
   10.54 +  val ML_keywordN: string val ML_keyword: Markup.T
   10.55 +  val ML_delimiterN: string val ML_delimiter: Markup.T
   10.56 +  val ML_tvarN: string val ML_tvar: Markup.T
   10.57 +  val ML_numeralN: string val ML_numeral: Markup.T
   10.58 +  val ML_charN: string val ML_char: Markup.T
   10.59 +  val ML_stringN: string val ML_string: Markup.T
   10.60 +  val ML_commentN: string val ML_comment: Markup.T
   10.61 +  val ML_malformedN: string val ML_malformed: Markup.T
   10.62 +  val ML_defN: string
   10.63 +  val ML_openN: string
   10.64 +  val ML_structN: string
   10.65 +  val ML_typingN: string val ML_typing: Markup.T
   10.66 +  val ML_sourceN: string val ML_source: Markup.T
   10.67 +  val doc_sourceN: string val doc_source: Markup.T
   10.68 +  val antiqN: string val antiq: Markup.T
   10.69 +  val ML_antiquotationN: string
   10.70 +  val doc_antiquotationN: string
   10.71 +  val doc_antiquotation_optionN: string
   10.72 +  val keyword_declN: string val keyword_decl: string -> Markup.T
   10.73 +  val command_declN: string val command_decl: string -> string -> Markup.T
   10.74 +  val keywordN: string val keyword: Markup.T
   10.75 +  val operatorN: string val operator: Markup.T
   10.76 +  val commandN: string val command: Markup.T
   10.77 +  val stringN: string val string: Markup.T
   10.78 +  val altstringN: string val altstring: Markup.T
   10.79 +  val verbatimN: string val verbatim: Markup.T
   10.80 +  val commentN: string val comment: Markup.T
   10.81 +  val controlN: string val control: Markup.T
   10.82 +  val malformedN: string val malformed: Markup.T
   10.83 +  val tokenN: string val token: Properties.T -> Markup.T
   10.84 +  val command_spanN: string val command_span: string -> Markup.T
   10.85 +  val ignored_spanN: string val ignored_span: Markup.T
   10.86 +  val malformed_spanN: string val malformed_span: Markup.T
   10.87 +  val loaded_theoryN: string val loaded_theory: string -> Markup.T
   10.88 +  val subgoalsN: string
   10.89 +  val proof_stateN: string val proof_state: int -> Markup.T
   10.90 +  val stateN: string val state: Markup.T
   10.91 +  val subgoalN: string val subgoal: Markup.T
   10.92 +  val sendbackN: string val sendback: Markup.T
   10.93 +  val hiliteN: string val hilite: Markup.T
   10.94 +  val taskN: string
   10.95 +  val forkedN: string val forked: Markup.T
   10.96 +  val joinedN: string val joined: Markup.T
   10.97 +  val failedN: string val failed: Markup.T
   10.98 +  val finishedN: string val finished: Markup.T
   10.99 +  val serialN: string
  10.100 +  val legacyN: string val legacy: Markup.T
  10.101 +  val promptN: string val prompt: Markup.T
  10.102 +  val readyN: string val ready: Markup.T
  10.103 +  val reportN: string val report: Markup.T
  10.104 +  val no_reportN: string val no_report: Markup.T
  10.105 +  val badN: string val bad: Markup.T
  10.106 +  val functionN: string
  10.107 +  val assign_execs: Properties.T
  10.108 +  val removed_versions: Properties.T
  10.109 +  val invoke_scala: string -> string -> Properties.T
  10.110 +  val cancel_scala: string -> Properties.T
  10.111 +end;
  10.112 +
  10.113 +structure Isabelle_Markup: ISABELLE_MARKUP =
  10.114 +struct
  10.115 +
  10.116 +(** markup elements **)
  10.117 +
  10.118 +fun markup_elem elem = (elem, (elem, []): Markup.T);
  10.119 +fun markup_string elem prop = (elem, fn s => (elem, [(prop, s)]): Markup.T);
  10.120 +fun markup_int elem prop = (elem, fn i => (elem, [(prop, Markup.print_int i)]): Markup.T);
  10.121 +
  10.122 +
  10.123 +(* formal entities *)
  10.124 +
  10.125 +val (bindingN, binding) = markup_elem "binding";
  10.126 +
  10.127 +val entityN = "entity";
  10.128 +fun entity kind name = (entityN, [(Markup.nameN, name), (Markup.kindN, kind)]);
  10.129 +
  10.130 +fun get_entity_kind (name, props) =
  10.131 +  if name = entityN then AList.lookup (op =) props Markup.kindN
  10.132 +  else NONE;
  10.133 +
  10.134 +val defN = "def";
  10.135 +val refN = "ref";
  10.136 +
  10.137 +
  10.138 +(* position *)
  10.139 +
  10.140 +val lineN = "line";
  10.141 +val offsetN = "offset";
  10.142 +val end_offsetN = "end_offset";
  10.143 +val fileN = "file";
  10.144 +val idN = "id";
  10.145 +
  10.146 +val position_properties' = [fileN, idN];
  10.147 +val position_properties = [lineN, offsetN, end_offsetN] @ position_properties';
  10.148 +
  10.149 +val (positionN, position) = markup_elem "position";
  10.150 +
  10.151 +
  10.152 +(* path *)
  10.153 +
  10.154 +val (pathN, path) = markup_string "path" Markup.nameN;
  10.155 +
  10.156 +
  10.157 +(* pretty printing *)
  10.158 +
  10.159 +val indentN = "indent";
  10.160 +val (blockN, block) = markup_int "block" indentN;
  10.161 +
  10.162 +val widthN = "width";
  10.163 +val (breakN, break) = markup_int "break" widthN;
  10.164 +
  10.165 +val (fbreakN, fbreak) = markup_elem "fbreak";
  10.166 +
  10.167 +
  10.168 +(* hidden text *)
  10.169 +
  10.170 +val (hiddenN, hidden) = markup_elem "hidden";
  10.171 +
  10.172 +
  10.173 +(* logical entities *)
  10.174 +
  10.175 +val classN = "class";
  10.176 +val typeN = "type";
  10.177 +val constantN = "constant";
  10.178 +
  10.179 +val (fixedN, fixed) = markup_string "fixed" Markup.nameN;
  10.180 +val (dynamic_factN, dynamic_fact) = markup_string "dynamic_fact" Markup.nameN;
  10.181 +
  10.182 +
  10.183 +(* inner syntax *)
  10.184 +
  10.185 +val (tfreeN, tfree) = markup_elem "tfree";
  10.186 +val (tvarN, tvar) = markup_elem "tvar";
  10.187 +val (freeN, free) = markup_elem "free";
  10.188 +val (skolemN, skolem) = markup_elem "skolem";
  10.189 +val (boundN, bound) = markup_elem "bound";
  10.190 +val (varN, var) = markup_elem "var";
  10.191 +val (numeralN, numeral) = markup_elem "numeral";
  10.192 +val (literalN, literal) = markup_elem "literal";
  10.193 +val (delimiterN, delimiter) = markup_elem "delimiter";
  10.194 +val (inner_stringN, inner_string) = markup_elem "inner_string";
  10.195 +val (inner_commentN, inner_comment) = markup_elem "inner_comment";
  10.196 +
  10.197 +val (token_rangeN, token_range) = markup_elem "token_range";
  10.198 +
  10.199 +val (sortN, sort) = markup_elem "sort";
  10.200 +val (typN, typ) = markup_elem "typ";
  10.201 +val (termN, term) = markup_elem "term";
  10.202 +val (propN, prop) = markup_elem "prop";
  10.203 +
  10.204 +val (typingN, typing) = markup_elem "typing";
  10.205 +
  10.206 +
  10.207 +(* ML syntax *)
  10.208 +
  10.209 +val (ML_keywordN, ML_keyword) = markup_elem "ML_keyword";
  10.210 +val (ML_delimiterN, ML_delimiter) = markup_elem "ML_delimiter";
  10.211 +val (ML_tvarN, ML_tvar) = markup_elem "ML_tvar";
  10.212 +val (ML_numeralN, ML_numeral) = markup_elem "ML_numeral";
  10.213 +val (ML_charN, ML_char) = markup_elem "ML_char";
  10.214 +val (ML_stringN, ML_string) = markup_elem "ML_string";
  10.215 +val (ML_commentN, ML_comment) = markup_elem "ML_comment";
  10.216 +val (ML_malformedN, ML_malformed) = markup_elem "ML_malformed";
  10.217 +
  10.218 +val ML_defN = "ML_def";
  10.219 +val ML_openN = "ML_open";
  10.220 +val ML_structN = "ML_struct";
  10.221 +val (ML_typingN, ML_typing) = markup_elem "ML_typing";
  10.222 +
  10.223 +
  10.224 +(* embedded source text *)
  10.225 +
  10.226 +val (ML_sourceN, ML_source) = markup_elem "ML_source";
  10.227 +val (doc_sourceN, doc_source) = markup_elem "doc_source";
  10.228 +
  10.229 +val (antiqN, antiq) = markup_elem "antiq";
  10.230 +val ML_antiquotationN = "ML antiquotation";
  10.231 +val doc_antiquotationN = "document antiquotation";
  10.232 +val doc_antiquotation_optionN = "document antiquotation option";
  10.233 +
  10.234 +
  10.235 +(* outer syntax *)
  10.236 +
  10.237 +val (keyword_declN, keyword_decl) = markup_string "keyword_decl" Markup.nameN;
  10.238 +
  10.239 +val command_declN = "command_decl";
  10.240 +
  10.241 +fun command_decl name kind : Markup.T =
  10.242 +  (command_declN, [(Markup.nameN, name), (Markup.kindN, kind)]);
  10.243 +
  10.244 +val (keywordN, keyword) = markup_elem "keyword";
  10.245 +val (operatorN, operator) = markup_elem "operator";
  10.246 +val (commandN, command) = markup_elem "command";
  10.247 +val (stringN, string) = markup_elem "string";
  10.248 +val (altstringN, altstring) = markup_elem "altstring";
  10.249 +val (verbatimN, verbatim) = markup_elem "verbatim";
  10.250 +val (commentN, comment) = markup_elem "comment";
  10.251 +val (controlN, control) = markup_elem "control";
  10.252 +val (malformedN, malformed) = markup_elem "malformed";
  10.253 +
  10.254 +val tokenN = "token";
  10.255 +fun token props = (tokenN, props);
  10.256 +
  10.257 +val (command_spanN, command_span) = markup_string "command_span" Markup.nameN;
  10.258 +val (ignored_spanN, ignored_span) = markup_elem "ignored_span";
  10.259 +val (malformed_spanN, malformed_span) = markup_elem "malformed_span";
  10.260 +
  10.261 +
  10.262 +(* theory loader *)
  10.263 +
  10.264 +val (loaded_theoryN, loaded_theory) = markup_string "loaded_theory" Markup.nameN;
  10.265 +
  10.266 +
  10.267 +(* toplevel *)
  10.268 +
  10.269 +val subgoalsN = "subgoals";
  10.270 +val (proof_stateN, proof_state) = markup_int "proof_state" subgoalsN;
  10.271 +
  10.272 +val (stateN, state) = markup_elem "state";
  10.273 +val (subgoalN, subgoal) = markup_elem "subgoal";
  10.274 +val (sendbackN, sendback) = markup_elem "sendback";
  10.275 +val (hiliteN, hilite) = markup_elem "hilite";
  10.276 +
  10.277 +
  10.278 +(* command status *)
  10.279 +
  10.280 +val taskN = "task";
  10.281 +
  10.282 +val (forkedN, forked) = markup_elem "forked";
  10.283 +val (joinedN, joined) = markup_elem "joined";
  10.284 +
  10.285 +val (failedN, failed) = markup_elem "failed";
  10.286 +val (finishedN, finished) = markup_elem "finished";
  10.287 +
  10.288 +
  10.289 +(* messages *)
  10.290 +
  10.291 +val serialN = "serial";
  10.292 +
  10.293 +val (legacyN, legacy) = markup_elem "legacy";
  10.294 +val (promptN, prompt) = markup_elem "prompt";
  10.295 +val (readyN, ready) = markup_elem "ready";
  10.296 +
  10.297 +val (reportN, report) = markup_elem "report";
  10.298 +val (no_reportN, no_report) = markup_elem "no_report";
  10.299 +
  10.300 +val (badN, bad) = markup_elem "bad";
  10.301 +
  10.302 +
  10.303 +(* raw message functions *)
  10.304 +
  10.305 +val functionN = "function"
  10.306 +
  10.307 +val assign_execs = [(functionN, "assign_execs")];
  10.308 +val removed_versions = [(functionN, "removed_versions")];
  10.309 +
  10.310 +fun invoke_scala name id = [(functionN, "invoke_scala"), (Markup.nameN, name), (idN, id)];
  10.311 +fun cancel_scala id = [(functionN, "cancel_scala"), (idN, id)];
  10.312 +
  10.313 +end;
    11.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    11.2 +++ b/src/Pure/General/isabelle_markup.scala	Mon Nov 28 22:05:32 2011 +0100
    11.3 @@ -0,0 +1,260 @@
    11.4 +/*  Title:      Pure/General/isabelle_markup.scala
    11.5 +    Author:     Makarius
    11.6 +
    11.7 +Isabelle markup elements.
    11.8 +*/
    11.9 +
   11.10 +package isabelle
   11.11 +
   11.12 +
   11.13 +object Isabelle_Markup
   11.14 +{
   11.15 +  /* formal entities */
   11.16 +
   11.17 +  val BINDING = "binding"
   11.18 +  val ENTITY = "entity"
   11.19 +  val DEF = "def"
   11.20 +  val REF = "ref"
   11.21 +
   11.22 +  object Entity
   11.23 +  {
   11.24 +    def unapply(markup: Markup): Option[(String, String)] =
   11.25 +      markup match {
   11.26 +        case Markup(ENTITY, props @ Markup.Kind(kind)) =>
   11.27 +          props match {
   11.28 +            case Markup.Name(name) => Some(kind, name)
   11.29 +            case _ => None
   11.30 +          }
   11.31 +        case _ => None
   11.32 +      }
   11.33 +  }
   11.34 +
   11.35 +
   11.36 +  /* position */
   11.37 +
   11.38 +  val LINE = "line"
   11.39 +  val OFFSET = "offset"
   11.40 +  val END_OFFSET = "end_offset"
   11.41 +  val FILE = "file"
   11.42 +  val ID = "id"
   11.43 +
   11.44 +  val DEF_LINE = "def_line"
   11.45 +  val DEF_OFFSET = "def_offset"
   11.46 +  val DEF_END_OFFSET = "def_end_offset"
   11.47 +  val DEF_FILE = "def_file"
   11.48 +  val DEF_ID = "def_id"
   11.49 +
   11.50 +  val POSITION_PROPERTIES = Set(LINE, OFFSET, END_OFFSET, FILE, ID)
   11.51 +  val POSITION = "position"
   11.52 +
   11.53 +
   11.54 +  /* path */
   11.55 +
   11.56 +  val PATH = "path"
   11.57 +
   11.58 +  object Path
   11.59 +  {
   11.60 +    def unapply(markup: Markup): Option[String] =
   11.61 +      markup match {
   11.62 +        case Markup(PATH, Markup.Name(name)) => Some(name)
   11.63 +        case _ => None
   11.64 +      }
   11.65 +  }
   11.66 +
   11.67 +
   11.68 +  /* pretty printing */
   11.69 +
   11.70 +  val Indent = new Properties.Int("indent")
   11.71 +  val BLOCK = "block"
   11.72 +  val Width = new Properties.Int("width")
   11.73 +  val BREAK = "break"
   11.74 +
   11.75 +
   11.76 +  /* hidden text */
   11.77 +
   11.78 +  val HIDDEN = "hidden"
   11.79 +
   11.80 +
   11.81 +  /* logical entities */
   11.82 +
   11.83 +  val CLASS = "class"
   11.84 +  val TYPE = "type"
   11.85 +  val FIXED = "fixed"
   11.86 +  val CONSTANT = "constant"
   11.87 +
   11.88 +  val DYNAMIC_FACT = "dynamic_fact"
   11.89 +
   11.90 +
   11.91 +  /* inner syntax */
   11.92 +
   11.93 +  val TFREE = "tfree"
   11.94 +  val TVAR = "tvar"
   11.95 +  val FREE = "free"
   11.96 +  val SKOLEM = "skolem"
   11.97 +  val BOUND = "bound"
   11.98 +  val VAR = "var"
   11.99 +  val NUM = "num"
  11.100 +  val FLOAT = "float"
  11.101 +  val XNUM = "xnum"
  11.102 +  val XSTR = "xstr"
  11.103 +  val LITERAL = "literal"
  11.104 +  val DELIMITER = "delimiter"
  11.105 +  val INNER_STRING = "inner_string"
  11.106 +  val INNER_COMMENT = "inner_comment"
  11.107 +
  11.108 +  val TOKEN_RANGE = "token_range"
  11.109 +
  11.110 +  val SORT = "sort"
  11.111 +  val TYP = "typ"
  11.112 +  val TERM = "term"
  11.113 +  val PROP = "prop"
  11.114 +
  11.115 +  val TYPING = "typing"
  11.116 +
  11.117 +  val ATTRIBUTE = "attribute"
  11.118 +  val METHOD = "method"
  11.119 +
  11.120 +
  11.121 +  /* embedded source text */
  11.122 +
  11.123 +  val ML_SOURCE = "ML_source"
  11.124 +  val DOC_SOURCE = "doc_source"
  11.125 +
  11.126 +  val ANTIQ = "antiq"
  11.127 +  val ML_ANTIQUOTATION = "ML antiquotation"
  11.128 +  val DOCUMENT_ANTIQUOTATION = "document antiquotation"
  11.129 +  val DOCUMENT_ANTIQUOTATION_OPTION = "document antiquotation option"
  11.130 +
  11.131 +
  11.132 +  /* ML syntax */
  11.133 +
  11.134 +  val ML_KEYWORD = "ML_keyword"
  11.135 +  val ML_DELIMITER = "ML_delimiter"
  11.136 +  val ML_TVAR = "ML_tvar"
  11.137 +  val ML_NUMERAL = "ML_numeral"
  11.138 +  val ML_CHAR = "ML_char"
  11.139 +  val ML_STRING = "ML_string"
  11.140 +  val ML_COMMENT = "ML_comment"
  11.141 +  val ML_MALFORMED = "ML_malformed"
  11.142 +
  11.143 +  val ML_DEF = "ML_def"
  11.144 +  val ML_OPEN = "ML_open"
  11.145 +  val ML_STRUCT = "ML_struct"
  11.146 +  val ML_TYPING = "ML_typing"
  11.147 +
  11.148 +
  11.149 +  /* outer syntax */
  11.150 +
  11.151 +  val KEYWORD_DECL = "keyword_decl"
  11.152 +  val COMMAND_DECL = "command_decl"
  11.153 +
  11.154 +  val KEYWORD = "keyword"
  11.155 +  val OPERATOR = "operator"
  11.156 +  val COMMAND = "command"
  11.157 +  val STRING = "string"
  11.158 +  val ALTSTRING = "altstring"
  11.159 +  val VERBATIM = "verbatim"
  11.160 +  val COMMENT = "comment"
  11.161 +  val CONTROL = "control"
  11.162 +  val MALFORMED = "malformed"
  11.163 +
  11.164 +  val COMMAND_SPAN = "command_span"
  11.165 +  val IGNORED_SPAN = "ignored_span"
  11.166 +  val MALFORMED_SPAN = "malformed_span"
  11.167 +
  11.168 +
  11.169 +  /* theory loader */
  11.170 +
  11.171 +  val LOADED_THEORY = "loaded_theory"
  11.172 +
  11.173 +
  11.174 +  /* toplevel */
  11.175 +
  11.176 +  val SUBGOALS = "subgoals"
  11.177 +  val PROOF_STATE = "proof_state"
  11.178 +
  11.179 +  val STATE = "state"
  11.180 +  val SUBGOAL = "subgoal"
  11.181 +  val SENDBACK = "sendback"
  11.182 +  val HILITE = "hilite"
  11.183 +
  11.184 +
  11.185 +  /* command status */
  11.186 +
  11.187 +  val TASK = "task"
  11.188 +
  11.189 +  val FORKED = "forked"
  11.190 +  val JOINED = "joined"
  11.191 +  val FAILED = "failed"
  11.192 +  val FINISHED = "finished"
  11.193 +
  11.194 +
  11.195 +  /* interactive documents */
  11.196 +
  11.197 +  val VERSION = "version"
  11.198 +  val ASSIGN = "assign"
  11.199 +
  11.200 +
  11.201 +  /* prover process */
  11.202 +
  11.203 +  val PROVER_COMMAND = "prover_command"
  11.204 +  val PROVER_ARG = "prover_arg"
  11.205 +
  11.206 +
  11.207 +  /* messages */
  11.208 +
  11.209 +  val Serial = new Properties.Long("serial")
  11.210 +
  11.211 +  val MESSAGE = "message"
  11.212 +
  11.213 +  val INIT = "init"
  11.214 +  val STATUS = "status"
  11.215 +  val REPORT = "report"
  11.216 +  val WRITELN = "writeln"
  11.217 +  val TRACING = "tracing"
  11.218 +  val WARNING = "warning"
  11.219 +  val ERROR = "error"
  11.220 +  val RAW = "raw"
  11.221 +  val SYSTEM = "system"
  11.222 +  val STDOUT = "stdout"
  11.223 +  val STDERR = "stderr"
  11.224 +  val EXIT = "exit"
  11.225 +
  11.226 +  val LEGACY = "legacy"
  11.227 +
  11.228 +  val NO_REPORT = "no_report"
  11.229 +
  11.230 +  val BAD = "bad"
  11.231 +
  11.232 +  val READY = "ready"
  11.233 +
  11.234 +
  11.235 +  /* raw message functions */
  11.236 +
  11.237 +  val FUNCTION = "function"
  11.238 +  val Function = new Properties.String(FUNCTION)
  11.239 +
  11.240 +  val Assign_Execs: Properties.T = List((FUNCTION, "assign_execs"))
  11.241 +  val Removed_Versions: Properties.T = List((FUNCTION, "removed_versions"))
  11.242 +
  11.243 +  val INVOKE_SCALA = "invoke_scala"
  11.244 +  object Invoke_Scala
  11.245 +  {
  11.246 +    def unapply(props: Properties.T): Option[(String, String)] =
  11.247 +      props match {
  11.248 +        case List((FUNCTION, INVOKE_SCALA), (Markup.NAME, name), (ID, id)) => Some((name, id))
  11.249 +        case _ => None
  11.250 +      }
  11.251 +  }
  11.252 +
  11.253 +  val CANCEL_SCALA = "cancel_scala"
  11.254 +  object Cancel_Scala
  11.255 +  {
  11.256 +    def unapply(props: Properties.T): Option[String] =
  11.257 +      props match {
  11.258 +        case List((FUNCTION, CANCEL_SCALA), (ID, id)) => Some(id)
  11.259 +        case _ => None
  11.260 +      }
  11.261 +  }
  11.262 +}
  11.263 +
    12.1 --- a/src/Pure/General/markup.ML	Mon Nov 28 20:39:08 2011 +0100
    12.2 +++ b/src/Pure/General/markup.ML	Mon Nov 28 22:05:32 2011 +0100
    12.3 @@ -1,7 +1,7 @@
    12.4  (*  Title:      Pure/General/markup.ML
    12.5      Author:     Makarius
    12.6  
    12.7 -Common markup elements.
    12.8 +Generic markup elements.
    12.9  *)
   12.10  
   12.11  signature MARKUP =
   12.12 @@ -15,109 +15,10 @@
   12.13    val nameN: string
   12.14    val name: string -> T -> T
   12.15    val kindN: string
   12.16 -  val bindingN: string val binding: T
   12.17 -  val entityN: string val entity: string -> string -> T
   12.18 -  val get_entity_kind: T -> string option
   12.19 -  val defN: string
   12.20 -  val refN: string
   12.21 -  val lineN: string
   12.22 -  val offsetN: string
   12.23 -  val end_offsetN: string
   12.24 -  val fileN: string
   12.25 -  val idN: string
   12.26 -  val position_properties': string list
   12.27 -  val position_properties: string list
   12.28 -  val positionN: string val position: T
   12.29 -  val pathN: string val path: string -> T
   12.30 -  val indentN: string
   12.31 -  val blockN: string val block: int -> T
   12.32 -  val widthN: string
   12.33 -  val breakN: string val break: int -> T
   12.34 -  val fbreakN: string val fbreak: T
   12.35 -  val hiddenN: string val hidden: T
   12.36 -  val classN: string
   12.37 -  val typeN: string
   12.38 -  val constantN: string
   12.39 -  val fixedN: string val fixed: string -> T
   12.40 -  val dynamic_factN: string val dynamic_fact: string -> T
   12.41 -  val tfreeN: string val tfree: T
   12.42 -  val tvarN: string val tvar: T
   12.43 -  val freeN: string val free: T
   12.44 -  val skolemN: string val skolem: T
   12.45 -  val boundN: string val bound: T
   12.46 -  val varN: string val var: T
   12.47 -  val numeralN: string val numeral: T
   12.48 -  val literalN: string val literal: T
   12.49 -  val delimiterN: string val delimiter: T
   12.50 -  val inner_stringN: string val inner_string: T
   12.51 -  val inner_commentN: string val inner_comment: T
   12.52 -  val token_rangeN: string val token_range: T
   12.53 -  val sortN: string val sort: T
   12.54 -  val typN: string val typ: T
   12.55 -  val termN: string val term: T
   12.56 -  val propN: string val prop: T
   12.57 -  val typingN: string val typing: T
   12.58 -  val ML_keywordN: string val ML_keyword: T
   12.59 -  val ML_delimiterN: string val ML_delimiter: T
   12.60 -  val ML_tvarN: string val ML_tvar: T
   12.61 -  val ML_numeralN: string val ML_numeral: T
   12.62 -  val ML_charN: string val ML_char: T
   12.63 -  val ML_stringN: string val ML_string: T
   12.64 -  val ML_commentN: string val ML_comment: T
   12.65 -  val ML_malformedN: string val ML_malformed: T
   12.66 -  val ML_defN: string
   12.67 -  val ML_openN: string
   12.68 -  val ML_structN: string
   12.69 -  val ML_typingN: string val ML_typing: T
   12.70 -  val ML_sourceN: string val ML_source: T
   12.71 -  val doc_sourceN: string val doc_source: T
   12.72 -  val antiqN: string val antiq: T
   12.73 -  val ML_antiquotationN: string
   12.74 -  val doc_antiquotationN: string
   12.75 -  val doc_antiquotation_optionN: string
   12.76 -  val keyword_declN: string val keyword_decl: string -> T
   12.77 -  val command_declN: string val command_decl: string -> string -> T
   12.78 -  val keywordN: string val keyword: T
   12.79 -  val operatorN: string val operator: T
   12.80 -  val commandN: string val command: T
   12.81 -  val stringN: string val string: T
   12.82 -  val altstringN: string val altstring: T
   12.83 -  val verbatimN: string val verbatim: T
   12.84 -  val commentN: string val comment: T
   12.85 -  val controlN: string val control: T
   12.86 -  val malformedN: string val malformed: T
   12.87 -  val tokenN: string val token: Properties.T -> T
   12.88 -  val command_spanN: string val command_span: string -> T
   12.89 -  val ignored_spanN: string val ignored_span: T
   12.90 -  val malformed_spanN: string val malformed_span: T
   12.91 -  val loaded_theoryN: string val loaded_theory: string -> T
   12.92    val elapsedN: string
   12.93    val cpuN: string
   12.94    val gcN: string
   12.95    val timingN: string val timing: Timing.timing -> T
   12.96 -  val subgoalsN: string
   12.97 -  val proof_stateN: string val proof_state: int -> T
   12.98 -  val stateN: string val state: T
   12.99 -  val subgoalN: string val subgoal: T
  12.100 -  val sendbackN: string val sendback: T
  12.101 -  val hiliteN: string val hilite: T
  12.102 -  val taskN: string
  12.103 -  val forkedN: string val forked: T
  12.104 -  val joinedN: string val joined: T
  12.105 -  val failedN: string val failed: T
  12.106 -  val finishedN: string val finished: T
  12.107 -  val serialN: string
  12.108 -  val legacyN: string val legacy: T
  12.109 -  val promptN: string val prompt: T
  12.110 -  val readyN: string val ready: T
  12.111 -  val reportN: string val report: T
  12.112 -  val no_reportN: string val no_report: T
  12.113 -  val badN: string val bad: T
  12.114 -  val functionN: string
  12.115 -  val assign_execs: Properties.T
  12.116 -  val removed_versions: Properties.T
  12.117 -  val invoke_scala: string -> string -> Properties.T
  12.118 -  val cancel_scala: string -> Properties.T
  12.119    val no_output: Output.output * Output.output
  12.120    val default_output: T -> Output.output * Output.output
  12.121    val add_mode: string -> (T -> Output.output * Output.output) -> unit
  12.122 @@ -157,10 +58,6 @@
  12.123  fun properties more_props ((elem, props): T) =
  12.124    (elem, fold_rev Properties.put more_props props);
  12.125  
  12.126 -fun markup_elem elem = (elem, (elem, []): T);
  12.127 -fun markup_string elem prop = (elem, fn s => (elem, [(prop, s)]): T);
  12.128 -fun markup_int elem prop = (elem, fn i => (elem, [(prop, print_int i)]): T);
  12.129 -
  12.130  
  12.131  (* misc properties *)
  12.132  
  12.133 @@ -170,148 +67,6 @@
  12.134  val kindN = "kind";
  12.135  
  12.136  
  12.137 -(* formal entities *)
  12.138 -
  12.139 -val (bindingN, binding) = markup_elem "binding";
  12.140 -
  12.141 -val entityN = "entity";
  12.142 -fun entity kind name = (entityN, [(nameN, name), (kindN, kind)]);
  12.143 -
  12.144 -fun get_entity_kind (name, props) =
  12.145 -  if name = entityN then AList.lookup (op =) props kindN
  12.146 -  else NONE;
  12.147 -
  12.148 -val defN = "def";
  12.149 -val refN = "ref";
  12.150 -
  12.151 -
  12.152 -(* position *)
  12.153 -
  12.154 -val lineN = "line";
  12.155 -val offsetN = "offset";
  12.156 -val end_offsetN = "end_offset";
  12.157 -val fileN = "file";
  12.158 -val idN = "id";
  12.159 -
  12.160 -val position_properties' = [fileN, idN];
  12.161 -val position_properties = [lineN, offsetN, end_offsetN] @ position_properties';
  12.162 -
  12.163 -val (positionN, position) = markup_elem "position";
  12.164 -
  12.165 -
  12.166 -(* path *)
  12.167 -
  12.168 -val (pathN, path) = markup_string "path" nameN;
  12.169 -
  12.170 -
  12.171 -(* pretty printing *)
  12.172 -
  12.173 -val indentN = "indent";
  12.174 -val (blockN, block) = markup_int "block" indentN;
  12.175 -
  12.176 -val widthN = "width";
  12.177 -val (breakN, break) = markup_int "break" widthN;
  12.178 -
  12.179 -val (fbreakN, fbreak) = markup_elem "fbreak";
  12.180 -
  12.181 -
  12.182 -(* hidden text *)
  12.183 -
  12.184 -val (hiddenN, hidden) = markup_elem "hidden";
  12.185 -
  12.186 -
  12.187 -(* logical entities *)
  12.188 -
  12.189 -val classN = "class";
  12.190 -val typeN = "type";
  12.191 -val constantN = "constant";
  12.192 -
  12.193 -val (fixedN, fixed) = markup_string "fixed" nameN;
  12.194 -val (dynamic_factN, dynamic_fact) = markup_string "dynamic_fact" nameN;
  12.195 -
  12.196 -
  12.197 -(* inner syntax *)
  12.198 -
  12.199 -val (tfreeN, tfree) = markup_elem "tfree";
  12.200 -val (tvarN, tvar) = markup_elem "tvar";
  12.201 -val (freeN, free) = markup_elem "free";
  12.202 -val (skolemN, skolem) = markup_elem "skolem";
  12.203 -val (boundN, bound) = markup_elem "bound";
  12.204 -val (varN, var) = markup_elem "var";
  12.205 -val (numeralN, numeral) = markup_elem "numeral";
  12.206 -val (literalN, literal) = markup_elem "literal";
  12.207 -val (delimiterN, delimiter) = markup_elem "delimiter";
  12.208 -val (inner_stringN, inner_string) = markup_elem "inner_string";
  12.209 -val (inner_commentN, inner_comment) = markup_elem "inner_comment";
  12.210 -
  12.211 -val (token_rangeN, token_range) = markup_elem "token_range";
  12.212 -
  12.213 -val (sortN, sort) = markup_elem "sort";
  12.214 -val (typN, typ) = markup_elem "typ";
  12.215 -val (termN, term) = markup_elem "term";
  12.216 -val (propN, prop) = markup_elem "prop";
  12.217 -
  12.218 -val (typingN, typing) = markup_elem "typing";
  12.219 -
  12.220 -
  12.221 -(* ML syntax *)
  12.222 -
  12.223 -val (ML_keywordN, ML_keyword) = markup_elem "ML_keyword";
  12.224 -val (ML_delimiterN, ML_delimiter) = markup_elem "ML_delimiter";
  12.225 -val (ML_tvarN, ML_tvar) = markup_elem "ML_tvar";
  12.226 -val (ML_numeralN, ML_numeral) = markup_elem "ML_numeral";
  12.227 -val (ML_charN, ML_char) = markup_elem "ML_char";
  12.228 -val (ML_stringN, ML_string) = markup_elem "ML_string";
  12.229 -val (ML_commentN, ML_comment) = markup_elem "ML_comment";
  12.230 -val (ML_malformedN, ML_malformed) = markup_elem "ML_malformed";
  12.231 -
  12.232 -val ML_defN = "ML_def";
  12.233 -val ML_openN = "ML_open";
  12.234 -val ML_structN = "ML_struct";
  12.235 -val (ML_typingN, ML_typing) = markup_elem "ML_typing";
  12.236 -
  12.237 -
  12.238 -(* embedded source text *)
  12.239 -
  12.240 -val (ML_sourceN, ML_source) = markup_elem "ML_source";
  12.241 -val (doc_sourceN, doc_source) = markup_elem "doc_source";
  12.242 -
  12.243 -val (antiqN, antiq) = markup_elem "antiq";
  12.244 -val ML_antiquotationN = "ML antiquotation";
  12.245 -val doc_antiquotationN = "document antiquotation";
  12.246 -val doc_antiquotation_optionN = "document antiquotation option";
  12.247 -
  12.248 -
  12.249 -(* outer syntax *)
  12.250 -
  12.251 -val (keyword_declN, keyword_decl) = markup_string "keyword_decl" nameN;
  12.252 -
  12.253 -val command_declN = "command_decl";
  12.254 -fun command_decl name kind : T = (command_declN, [(nameN, name), (kindN, kind)]);
  12.255 -
  12.256 -val (keywordN, keyword) = markup_elem "keyword";
  12.257 -val (operatorN, operator) = markup_elem "operator";
  12.258 -val (commandN, command) = markup_elem "command";
  12.259 -val (stringN, string) = markup_elem "string";
  12.260 -val (altstringN, altstring) = markup_elem "altstring";
  12.261 -val (verbatimN, verbatim) = markup_elem "verbatim";
  12.262 -val (commentN, comment) = markup_elem "comment";
  12.263 -val (controlN, control) = markup_elem "control";
  12.264 -val (malformedN, malformed) = markup_elem "malformed";
  12.265 -
  12.266 -val tokenN = "token";
  12.267 -fun token props = (tokenN, props);
  12.268 -
  12.269 -val (command_spanN, command_span) = markup_string "command_span" nameN;
  12.270 -val (ignored_spanN, ignored_span) = markup_elem "ignored_span";
  12.271 -val (malformed_spanN, malformed_span) = markup_elem "malformed_span";
  12.272 -
  12.273 -
  12.274 -(* theory loader *)
  12.275 -
  12.276 -val (loaded_theoryN, loaded_theory) = markup_string "loaded_theory" nameN;
  12.277 -
  12.278 -
  12.279  (* timing *)
  12.280  
  12.281  val timingN = "timing";
  12.282 @@ -326,53 +81,6 @@
  12.283      (gcN, Time.toString gc)]);
  12.284  
  12.285  
  12.286 -(* toplevel *)
  12.287 -
  12.288 -val subgoalsN = "subgoals";
  12.289 -val (proof_stateN, proof_state) = markup_int "proof_state" subgoalsN;
  12.290 -
  12.291 -val (stateN, state) = markup_elem "state";
  12.292 -val (subgoalN, subgoal) = markup_elem "subgoal";
  12.293 -val (sendbackN, sendback) = markup_elem "sendback";
  12.294 -val (hiliteN, hilite) = markup_elem "hilite";
  12.295 -
  12.296 -
  12.297 -(* command status *)
  12.298 -
  12.299 -val taskN = "task";
  12.300 -
  12.301 -val (forkedN, forked) = markup_elem "forked";
  12.302 -val (joinedN, joined) = markup_elem "joined";
  12.303 -
  12.304 -val (failedN, failed) = markup_elem "failed";
  12.305 -val (finishedN, finished) = markup_elem "finished";
  12.306 -
  12.307 -
  12.308 -(* messages *)
  12.309 -
  12.310 -val serialN = "serial";
  12.311 -
  12.312 -val (legacyN, legacy) = markup_elem "legacy";
  12.313 -val (promptN, prompt) = markup_elem "prompt";
  12.314 -val (readyN, ready) = markup_elem "ready";
  12.315 -
  12.316 -val (reportN, report) = markup_elem "report";
  12.317 -val (no_reportN, no_report) = markup_elem "no_report";
  12.318 -
  12.319 -val (badN, bad) = markup_elem "bad";
  12.320 -
  12.321 -
  12.322 -(* raw message functions *)
  12.323 -
  12.324 -val functionN = "function"
  12.325 -
  12.326 -val assign_execs = [(functionN, "assign_execs")];
  12.327 -val removed_versions = [(functionN, "removed_versions")];
  12.328 -
  12.329 -fun invoke_scala name id = [(functionN, "invoke_scala"), (nameN, name), (idN, id)];
  12.330 -fun cancel_scala id = [(functionN, "cancel_scala"), (idN, id)];
  12.331 -
  12.332 -
  12.333  
  12.334  (** print mode operations **)
  12.335  
    13.1 --- a/src/Pure/General/markup.scala	Mon Nov 28 20:39:08 2011 +0100
    13.2 +++ b/src/Pure/General/markup.scala	Mon Nov 28 22:05:32 2011 +0100
    13.3 @@ -1,7 +1,7 @@
    13.4  /*  Title:      Pure/General/markup.scala
    13.5      Author:     Makarius
    13.6  
    13.7 -Common markup elements.
    13.8 +Generic markup elements.
    13.9  */
   13.10  
   13.11  package isabelle
   13.12 @@ -9,12 +9,7 @@
   13.13  
   13.14  object Markup
   13.15  {
   13.16 -  /* empty */
   13.17 -
   13.18 -  val Empty = Markup("", Nil)
   13.19 -
   13.20 -
   13.21 -  /* misc properties */
   13.22 +  /* properties */
   13.23  
   13.24    val NAME = "name"
   13.25    val Name = new Properties.String(NAME)
   13.26 @@ -23,163 +18,11 @@
   13.27    val Kind = new Properties.String(KIND)
   13.28  
   13.29  
   13.30 -  /* formal entities */
   13.31 -
   13.32 -  val BINDING = "binding"
   13.33 -  val ENTITY = "entity"
   13.34 -  val DEF = "def"
   13.35 -  val REF = "ref"
   13.36 -
   13.37 -  object Entity
   13.38 -  {
   13.39 -    def unapply(markup: Markup): Option[(String, String)] =
   13.40 -      markup match {
   13.41 -        case Markup(ENTITY, props @ Kind(kind)) =>
   13.42 -          props match {
   13.43 -            case Name(name) => Some(kind, name)
   13.44 -            case _ => None
   13.45 -          }
   13.46 -        case _ => None
   13.47 -      }
   13.48 -  }
   13.49 -
   13.50 -
   13.51 -  /* position */
   13.52 -
   13.53 -  val LINE = "line"
   13.54 -  val OFFSET = "offset"
   13.55 -  val END_OFFSET = "end_offset"
   13.56 -  val FILE = "file"
   13.57 -  val ID = "id"
   13.58 -
   13.59 -  val DEF_LINE = "def_line"
   13.60 -  val DEF_OFFSET = "def_offset"
   13.61 -  val DEF_END_OFFSET = "def_end_offset"
   13.62 -  val DEF_FILE = "def_file"
   13.63 -  val DEF_ID = "def_id"
   13.64 -
   13.65 -  val POSITION_PROPERTIES = Set(LINE, OFFSET, END_OFFSET, FILE, ID)
   13.66 -  val POSITION = "position"
   13.67 -
   13.68 -
   13.69 -  /* path */
   13.70 -
   13.71 -  val PATH = "path"
   13.72 -
   13.73 -  object Path
   13.74 -  {
   13.75 -    def unapply(markup: Markup): Option[String] =
   13.76 -      markup match {
   13.77 -        case Markup(PATH, Name(name)) => Some(name)
   13.78 -        case _ => None
   13.79 -      }
   13.80 -  }
   13.81 -
   13.82 -
   13.83 -  /* pretty printing */
   13.84 -
   13.85 -  val Indent = new Properties.Int("indent")
   13.86 -  val BLOCK = "block"
   13.87 -  val Width = new Properties.Int("width")
   13.88 -  val BREAK = "break"
   13.89 -
   13.90 -
   13.91 -  /* hidden text */
   13.92 -
   13.93 -  val HIDDEN = "hidden"
   13.94 -
   13.95 -
   13.96 -  /* logical entities */
   13.97 -
   13.98 -  val CLASS = "class"
   13.99 -  val TYPE = "type"
  13.100 -  val FIXED = "fixed"
  13.101 -  val CONSTANT = "constant"
  13.102 -
  13.103 -  val DYNAMIC_FACT = "dynamic_fact"
  13.104 -
  13.105 -
  13.106 -  /* inner syntax */
  13.107 +  /* elements */
  13.108  
  13.109 -  val TFREE = "tfree"
  13.110 -  val TVAR = "tvar"
  13.111 -  val FREE = "free"
  13.112 -  val SKOLEM = "skolem"
  13.113 -  val BOUND = "bound"
  13.114 -  val VAR = "var"
  13.115 -  val NUM = "num"
  13.116 -  val FLOAT = "float"
  13.117 -  val XNUM = "xnum"
  13.118 -  val XSTR = "xstr"
  13.119 -  val LITERAL = "literal"
  13.120 -  val DELIMITER = "delimiter"
  13.121 -  val INNER_STRING = "inner_string"
  13.122 -  val INNER_COMMENT = "inner_comment"
  13.123 -
  13.124 -  val TOKEN_RANGE = "token_range"
  13.125 -
  13.126 -  val SORT = "sort"
  13.127 -  val TYP = "typ"
  13.128 -  val TERM = "term"
  13.129 -  val PROP = "prop"
  13.130 -
  13.131 -  val TYPING = "typing"
  13.132 -
  13.133 -  val ATTRIBUTE = "attribute"
  13.134 -  val METHOD = "method"
  13.135 -
  13.136 -
  13.137 -  /* embedded source text */
  13.138 -
  13.139 -  val ML_SOURCE = "ML_source"
  13.140 -  val DOC_SOURCE = "doc_source"
  13.141 -
  13.142 -  val ANTIQ = "antiq"
  13.143 -  val ML_ANTIQUOTATION = "ML antiquotation"
  13.144 -  val DOCUMENT_ANTIQUOTATION = "document antiquotation"
  13.145 -  val DOCUMENT_ANTIQUOTATION_OPTION = "document antiquotation option"
  13.146 -
  13.147 -
  13.148 -  /* ML syntax */
  13.149 -
  13.150 -  val ML_KEYWORD = "ML_keyword"
  13.151 -  val ML_DELIMITER = "ML_delimiter"
  13.152 -  val ML_TVAR = "ML_tvar"
  13.153 -  val ML_NUMERAL = "ML_numeral"
  13.154 -  val ML_CHAR = "ML_char"
  13.155 -  val ML_STRING = "ML_string"
  13.156 -  val ML_COMMENT = "ML_comment"
  13.157 -  val ML_MALFORMED = "ML_malformed"
  13.158 -
  13.159 -  val ML_DEF = "ML_def"
  13.160 -  val ML_OPEN = "ML_open"
  13.161 -  val ML_STRUCT = "ML_struct"
  13.162 -  val ML_TYPING = "ML_typing"
  13.163 -
  13.164 -
  13.165 -  /* outer syntax */
  13.166 -
  13.167 -  val KEYWORD_DECL = "keyword_decl"
  13.168 -  val COMMAND_DECL = "command_decl"
  13.169 -
  13.170 -  val KEYWORD = "keyword"
  13.171 -  val OPERATOR = "operator"
  13.172 -  val COMMAND = "command"
  13.173 -  val STRING = "string"
  13.174 -  val ALTSTRING = "altstring"
  13.175 -  val VERBATIM = "verbatim"
  13.176 -  val COMMENT = "comment"
  13.177 -  val CONTROL = "control"
  13.178 -  val MALFORMED = "malformed"
  13.179 -
  13.180 -  val COMMAND_SPAN = "command_span"
  13.181 -  val IGNORED_SPAN = "ignored_span"
  13.182 -  val MALFORMED_SPAN = "malformed_span"
  13.183 -
  13.184 -
  13.185 -  /* theory loader */
  13.186 -
  13.187 -  val LOADED_THEORY = "loaded_theory"
  13.188 +  val Empty = Markup("", Nil)
  13.189 +  val Data = Markup("data", Nil)
  13.190 +  val Broken = Markup("broken", Nil)
  13.191  
  13.192  
  13.193    /* timing */
  13.194 @@ -206,101 +49,8 @@
  13.195          case _ => None
  13.196        }
  13.197    }
  13.198 -
  13.199 -
  13.200 -  /* toplevel */
  13.201 -
  13.202 -  val SUBGOALS = "subgoals"
  13.203 -  val PROOF_STATE = "proof_state"
  13.204 -
  13.205 -  val STATE = "state"
  13.206 -  val SUBGOAL = "subgoal"
  13.207 -  val SENDBACK = "sendback"
  13.208 -  val HILITE = "hilite"
  13.209 -
  13.210 -
  13.211 -  /* command status */
  13.212 -
  13.213 -  val TASK = "task"
  13.214 -
  13.215 -  val FORKED = "forked"
  13.216 -  val JOINED = "joined"
  13.217 -  val FAILED = "failed"
  13.218 -  val FINISHED = "finished"
  13.219 -
  13.220 -
  13.221 -  /* interactive documents */
  13.222 -
  13.223 -  val VERSION = "version"
  13.224 -  val ASSIGN = "assign"
  13.225 -
  13.226 -
  13.227 -  /* prover process */
  13.228 -
  13.229 -  val PROVER_COMMAND = "prover_command"
  13.230 -  val PROVER_ARG = "prover_arg"
  13.231 +}
  13.232  
  13.233  
  13.234 -  /* messages */
  13.235 -
  13.236 -  val Serial = new Properties.Long("serial")
  13.237 -
  13.238 -  val MESSAGE = "message"
  13.239 -
  13.240 -  val INIT = "init"
  13.241 -  val STATUS = "status"
  13.242 -  val REPORT = "report"
  13.243 -  val WRITELN = "writeln"
  13.244 -  val TRACING = "tracing"
  13.245 -  val WARNING = "warning"
  13.246 -  val ERROR = "error"
  13.247 -  val RAW = "raw"
  13.248 -  val SYSTEM = "system"
  13.249 -  val STDOUT = "stdout"
  13.250 -  val STDERR = "stderr"
  13.251 -  val EXIT = "exit"
  13.252 -
  13.253 -  val LEGACY = "legacy"
  13.254 -
  13.255 -  val NO_REPORT = "no_report"
  13.256 -
  13.257 -  val BAD = "bad"
  13.258 -
  13.259 -  val READY = "ready"
  13.260 -
  13.261 -
  13.262 -  /* raw message functions */
  13.263 +sealed case class Markup(name: String, properties: Properties.T)
  13.264  
  13.265 -  val FUNCTION = "function"
  13.266 -  val Function = new Properties.String(FUNCTION)
  13.267 -
  13.268 -  val Assign_Execs: Properties.T = List((FUNCTION, "assign_execs"))
  13.269 -  val Removed_Versions: Properties.T = List((FUNCTION, "removed_versions"))
  13.270 -
  13.271 -  val INVOKE_SCALA = "invoke_scala"
  13.272 -  object Invoke_Scala
  13.273 -  {
  13.274 -    def unapply(props: Properties.T): Option[(String, String)] =
  13.275 -      props match {
  13.276 -        case List((FUNCTION, INVOKE_SCALA), (NAME, name), (ID, id)) => Some((name, id))
  13.277 -        case _ => None
  13.278 -      }
  13.279 -  }
  13.280 -
  13.281 -  val CANCEL_SCALA = "cancel_scala"
  13.282 -  object Cancel_Scala
  13.283 -  {
  13.284 -    def unapply(props: Properties.T): Option[String] =
  13.285 -      props match {
  13.286 -        case List((FUNCTION, CANCEL_SCALA), (ID, id)) => Some(id)
  13.287 -        case _ => None
  13.288 -      }
  13.289 -  }
  13.290 -
  13.291 -
  13.292 -  /* system data */
  13.293 -
  13.294 -  val Data = Markup("data", Nil)
  13.295 -}
  13.296 -
  13.297 -sealed case class Markup(name: String, properties: Properties.T)
    14.1 --- a/src/Pure/General/name_space.ML	Mon Nov 28 20:39:08 2011 +0100
    14.2 +++ b/src/Pure/General/name_space.ML	Mon Nov 28 22:05:32 2011 +0100
    14.3 @@ -83,7 +83,7 @@
    14.4    id: serial};
    14.5  
    14.6  fun entry_markup def kind (name, {pos, id, ...}: entry) =
    14.7 -  Markup.properties (Position.entity_properties_of def id pos) (Markup.entity kind name);
    14.8 +  Markup.properties (Position.entity_properties_of def id pos) (Isabelle_Markup.entity kind name);
    14.9  
   14.10  fun print_entry def kind (name, entry) =
   14.11    quote (Markup.markup (entry_markup def kind (name, entry)) name);
   14.12 @@ -126,7 +126,7 @@
   14.13  
   14.14  fun markup (Name_Space {kind, entries, ...}) name =
   14.15    (case Symtab.lookup entries name of
   14.16 -    NONE => Markup.hilite
   14.17 +    NONE => Isabelle_Markup.hilite
   14.18    | SOME (_, entry) => entry_markup false kind (name, entry));
   14.19  
   14.20  fun is_concealed space name = #concealed (the_entry space name);
    15.1 --- a/src/Pure/General/path.ML	Mon Nov 28 20:39:08 2011 +0100
    15.2 +++ b/src/Pure/General/path.ML	Mon Nov 28 22:05:32 2011 +0100
    15.3 @@ -155,7 +155,7 @@
    15.4  
    15.5  fun pretty path =
    15.6    let val s = implode_path path
    15.7 -  in Pretty.mark (Markup.path s) (Pretty.str (quote s)) end;
    15.8 +  in Pretty.mark (Isabelle_Markup.path s) (Pretty.str (quote s)) end;
    15.9  
   15.10  val print = Pretty.str_of o pretty;
   15.11  
    16.1 --- a/src/Pure/General/position.ML	Mon Nov 28 20:39:08 2011 +0100
    16.2 +++ b/src/Pure/General/position.ML	Mon Nov 28 22:05:32 2011 +0100
    16.3 @@ -58,7 +58,8 @@
    16.4  datatype T = Pos of (int * int * int) * Properties.T;
    16.5  
    16.6  fun norm_props (props: Properties.T) =
    16.7 -  maps (fn a => the_list (find_first (fn (b, _) => a = b) props)) Markup.position_properties';
    16.8 +  maps (fn a => the_list (find_first (fn (b, _) => a = b) props))
    16.9 +    Isabelle_Markup.position_properties';
   16.10  
   16.11  fun make {line = i, offset = j, end_offset = k, props} = Pos ((i, j, k), norm_props props);
   16.12  fun dest (Pos ((i, j, k), props)) = {line = i, offset = j, end_offset = k, props = props};
   16.13 @@ -73,7 +74,7 @@
   16.14  fun offset_of (Pos ((_, j, _), _)) = if valid j then SOME j else NONE;
   16.15  fun end_offset_of (Pos ((_, _, k), _)) = if valid k then SOME k else NONE;
   16.16  
   16.17 -fun file_of (Pos (_, props)) = Properties.get props Markup.fileN;
   16.18 +fun file_of (Pos (_, props)) = Properties.get props Isabelle_Markup.fileN;
   16.19  
   16.20  
   16.21  (* advance *)
   16.22 @@ -105,7 +106,7 @@
   16.23  
   16.24  
   16.25  fun file_name "" = []
   16.26 -  | file_name name = [(Markup.fileN, name)];
   16.27 +  | file_name name = [(Isabelle_Markup.fileN, name)];
   16.28  
   16.29  fun file_only name = Pos ((0, 0, 0), file_name name);
   16.30  fun file name = Pos ((1, 1, 0), file_name name);
   16.31 @@ -113,11 +114,11 @@
   16.32  fun line_file i name = Pos ((i, 1, 0), file_name name);
   16.33  fun line i = line_file i "";
   16.34  
   16.35 -fun id id = Pos ((0, 1, 0), [(Markup.idN, id)]);
   16.36 -fun id_only id = Pos ((0, 0, 0), [(Markup.idN, id)]);
   16.37 +fun id id = Pos ((0, 1, 0), [(Isabelle_Markup.idN, id)]);
   16.38 +fun id_only id = Pos ((0, 0, 0), [(Isabelle_Markup.idN, id)]);
   16.39  
   16.40 -fun get_id (Pos (_, props)) = Properties.get props Markup.idN;
   16.41 -fun put_id id (Pos (count, props)) = Pos (count, Properties.put (Markup.idN, id) props);
   16.42 +fun get_id (Pos (_, props)) = Properties.get props Isabelle_Markup.idN;
   16.43 +fun put_id id (Pos (count, props)) = Pos (count, Properties.put (Isabelle_Markup.idN, id) props);
   16.44  
   16.45  
   16.46  (* markup properties *)
   16.47 @@ -129,24 +130,26 @@
   16.48          NONE => 0
   16.49        | SOME s => the_default 0 (Int.fromString s));
   16.50    in
   16.51 -    make {line = get Markup.lineN, offset = get Markup.offsetN,
   16.52 -      end_offset = get Markup.end_offsetN, props = props}
   16.53 +    make {line = get Isabelle_Markup.lineN, offset = get Isabelle_Markup.offsetN,
   16.54 +      end_offset = get Isabelle_Markup.end_offsetN, props = props}
   16.55    end;
   16.56  
   16.57  
   16.58  fun value k i = if valid i then [(k, string_of_int i)] else [];
   16.59  
   16.60  fun properties_of (Pos ((i, j, k), props)) =
   16.61 -  value Markup.lineN i @ value Markup.offsetN j @ value Markup.end_offsetN k @ props;
   16.62 +  value Isabelle_Markup.lineN i @
   16.63 +  value Isabelle_Markup.offsetN j @
   16.64 +  value Isabelle_Markup.end_offsetN k @ props;
   16.65  
   16.66  val def_properties_of = properties_of #> (map (fn (x, y) => ("def_" ^ x, y)));
   16.67  
   16.68  fun entity_properties_of def id pos =
   16.69 -  if def then (Markup.defN, string_of_int id) :: properties_of pos
   16.70 -  else (Markup.refN, string_of_int id) :: def_properties_of pos;
   16.71 +  if def then (Isabelle_Markup.defN, string_of_int id) :: properties_of pos
   16.72 +  else (Isabelle_Markup.refN, string_of_int id) :: def_properties_of pos;
   16.73  
   16.74  fun default_properties default props =
   16.75 -  if exists (member (op =) Markup.position_properties o #1) props then props
   16.76 +  if exists (member (op =) Isabelle_Markup.position_properties o #1) props then props
   16.77    else properties_of default @ props;
   16.78  
   16.79  val markup = Markup.properties o properties_of;
   16.80 @@ -185,7 +188,9 @@
   16.81        | _ => "");
   16.82    in
   16.83      if null props then ""
   16.84 -    else (if s = "" then "" else " ") ^ Markup.markup (Markup.properties props Markup.position) s
   16.85 +    else
   16.86 +      (if s = "" then "" else " ") ^
   16.87 +        Markup.markup (Markup.properties props Isabelle_Markup.position) s
   16.88    end;
   16.89  
   16.90  
    17.1 --- a/src/Pure/General/position.scala	Mon Nov 28 20:39:08 2011 +0100
    17.2 +++ b/src/Pure/General/position.scala	Mon Nov 28 22:05:32 2011 +0100
    17.3 @@ -11,11 +11,11 @@
    17.4  {
    17.5    type T = Properties.T
    17.6  
    17.7 -  val Line = new Properties.Int(Markup.LINE)
    17.8 -  val Offset = new Properties.Int(Markup.OFFSET)
    17.9 -  val End_Offset = new Properties.Int(Markup.END_OFFSET)
   17.10 -  val File = new Properties.String(Markup.FILE)
   17.11 -  val Id = new Properties.Long(Markup.ID)
   17.12 +  val Line = new Properties.Int(Isabelle_Markup.LINE)
   17.13 +  val Offset = new Properties.Int(Isabelle_Markup.OFFSET)
   17.14 +  val End_Offset = new Properties.Int(Isabelle_Markup.END_OFFSET)
   17.15 +  val File = new Properties.String(Isabelle_Markup.FILE)
   17.16 +  val Id = new Properties.Long(Isabelle_Markup.ID)
   17.17  
   17.18    object Range
   17.19    {
   17.20 @@ -38,13 +38,13 @@
   17.21    }
   17.22  
   17.23    private val purge_pos = Map(
   17.24 -    Markup.DEF_LINE -> Markup.LINE,
   17.25 -    Markup.DEF_OFFSET -> Markup.OFFSET,
   17.26 -    Markup.DEF_END_OFFSET -> Markup.END_OFFSET,
   17.27 -    Markup.DEF_FILE -> Markup.FILE,
   17.28 -    Markup.DEF_ID -> Markup.ID)
   17.29 +    Isabelle_Markup.DEF_LINE -> Isabelle_Markup.LINE,
   17.30 +    Isabelle_Markup.DEF_OFFSET -> Isabelle_Markup.OFFSET,
   17.31 +    Isabelle_Markup.DEF_END_OFFSET -> Isabelle_Markup.END_OFFSET,
   17.32 +    Isabelle_Markup.DEF_FILE -> Isabelle_Markup.FILE,
   17.33 +    Isabelle_Markup.DEF_ID -> Isabelle_Markup.ID)
   17.34  
   17.35    def purge(props: T): T =
   17.36 -    for ((x, y) <- props if !Markup.POSITION_PROPERTIES(x))
   17.37 +    for ((x, y) <- props if !Isabelle_Markup.POSITION_PROPERTIES(x))
   17.38        yield (if (purge_pos.isDefinedAt(x)) (purge_pos(x), y) else (x, y))
   17.39  }
    18.1 --- a/src/Pure/General/pretty.ML	Mon Nov 28 20:39:08 2011 +0100
    18.2 +++ b/src/Pure/General/pretty.ML	Mon Nov 28 22:05:32 2011 +0100
    18.3 @@ -133,8 +133,8 @@
    18.4  fun mark_str (m, s) = mark m (str s);
    18.5  fun marks_str (ms, s) = fold_rev mark ms (str s);
    18.6  
    18.7 -fun keyword name = mark_str (Markup.keyword, name);
    18.8 -fun command name = mark_str (Markup.command, name);
    18.9 +fun keyword name = mark_str (Isabelle_Markup.keyword, name);
   18.10 +fun command name = mark_str (Isabelle_Markup.command, name);
   18.11  
   18.12  fun markup_chunks m prts = markup m (fbreaks prts);
   18.13  val chunks = markup_chunks Markup.empty;
   18.14 @@ -276,9 +276,12 @@
   18.15    let
   18.16      fun out (Block ((bg, en), [], _, _)) = Buffer.add bg #> Buffer.add en
   18.17        | out (Block ((bg, en), prts, indent, _)) =
   18.18 -          Buffer.add bg #> Buffer.markup (Markup.block indent) (fold out prts) #> Buffer.add en
   18.19 +          Buffer.add bg #>
   18.20 +          Buffer.markup (Isabelle_Markup.block indent) (fold out prts) #>
   18.21 +          Buffer.add en
   18.22        | out (String (s, _)) = Buffer.add s
   18.23 -      | out (Break (false, wd)) = Buffer.markup (Markup.break wd) (Buffer.add (output_spaces wd))
   18.24 +      | out (Break (false, wd)) =
   18.25 +          Buffer.markup (Isabelle_Markup.break wd) (Buffer.add (output_spaces wd))
   18.26        | out (Break (true, _)) = Buffer.add (Output.output "\n");
   18.27    in out prt Buffer.empty end;
   18.28  
    19.1 --- a/src/Pure/General/pretty.scala	Mon Nov 28 20:39:08 2011 +0100
    19.2 +++ b/src/Pure/General/pretty.scala	Mon Nov 28 22:05:32 2011 +0100
    19.3 @@ -19,11 +19,12 @@
    19.4    object Block
    19.5    {
    19.6      def apply(i: Int, body: XML.Body): XML.Tree =
    19.7 -      XML.Elem(Markup(Markup.BLOCK, Markup.Indent(i)), body)
    19.8 +      XML.Elem(Markup(Isabelle_Markup.BLOCK, Isabelle_Markup.Indent(i)), body)
    19.9  
   19.10      def unapply(tree: XML.Tree): Option[(Int, XML.Body)] =
   19.11        tree match {
   19.12 -        case XML.Elem(Markup(Markup.BLOCK, Markup.Indent(i)), body) => Some((i, body))
   19.13 +        case XML.Elem(Markup(Isabelle_Markup.BLOCK, Isabelle_Markup.Indent(i)), body) =>
   19.14 +          Some((i, body))
   19.15          case _ => None
   19.16        }
   19.17    }
   19.18 @@ -31,11 +32,12 @@
   19.19    object Break
   19.20    {
   19.21      def apply(w: Int): XML.Tree =
   19.22 -      XML.Elem(Markup(Markup.BREAK, Markup.Width(w)), List(XML.Text(Symbol.spaces(w))))
   19.23 +      XML.Elem(Markup(Isabelle_Markup.BREAK, Isabelle_Markup.Width(w)),
   19.24 +        List(XML.Text(Symbol.spaces(w))))
   19.25  
   19.26      def unapply(tree: XML.Tree): Option[Int] =
   19.27        tree match {
   19.28 -        case XML.Elem(Markup(Markup.BREAK, Markup.Width(w)), _) => Some(w)
   19.29 +        case XML.Elem(Markup(Isabelle_Markup.BREAK, Isabelle_Markup.Width(w)), _) => Some(w)
   19.30          case _ => None
   19.31        }
   19.32    }
    20.1 --- a/src/Pure/IsaMakefile	Mon Nov 28 20:39:08 2011 +0100
    20.2 +++ b/src/Pure/IsaMakefile	Mon Nov 28 22:05:32 2011 +0100
    20.3 @@ -80,6 +80,7 @@
    20.4    General/graph.ML					\
    20.5    General/heap.ML					\
    20.6    General/integer.ML					\
    20.7 +  General/isabelle_markup.ML				\
    20.8    General/linear_set.ML					\
    20.9    General/long_name.ML					\
   20.10    General/markup.ML					\
    21.1 --- a/src/Pure/Isar/isar_cmd.ML	Mon Nov 28 20:39:08 2011 +0100
    21.2 +++ b/src/Pure/Isar/isar_cmd.ML	Mon Nov 28 22:05:32 2011 +0100
    21.3 @@ -515,7 +515,7 @@
    21.4  (* markup commands *)
    21.5  
    21.6  fun check_text (txt, pos) state =
    21.7 - (Position.report pos Markup.doc_source;
    21.8 + (Position.report pos Isabelle_Markup.doc_source;
    21.9    ignore (Thy_Output.eval_antiquote (#1 (Keyword.get_lexicons ())) state (txt, pos)));
   21.10  
   21.11  fun header_markup txt = Toplevel.keep (fn state =>
    22.1 --- a/src/Pure/Isar/keyword.ML	Mon Nov 28 20:39:08 2011 +0100
    22.2 +++ b/src/Pure/Isar/keyword.ML	Mon Nov 28 22:05:32 2011 +0100
    22.3 @@ -156,11 +156,11 @@
    22.4      (if print_mode_active keyword_statusN then Output.status else writeln) s;
    22.5  
    22.6  fun keyword_status name =
    22.7 -  status_message (Markup.markup (Markup.keyword_decl name)
    22.8 +  status_message (Markup.markup (Isabelle_Markup.keyword_decl name)
    22.9      ("Outer syntax keyword: " ^ quote name));
   22.10  
   22.11  fun command_status (name, kind) =
   22.12 -  status_message (Markup.markup (Markup.command_decl name (kind_of kind))
   22.13 +  status_message (Markup.markup (Isabelle_Markup.command_decl name (kind_of kind))
   22.14      ("Outer syntax command: " ^ quote name ^ " (" ^ kind_of kind ^ ")"));
   22.15  
   22.16  fun status () =
    23.1 --- a/src/Pure/Isar/keyword.scala	Mon Nov 28 20:39:08 2011 +0100
    23.2 +++ b/src/Pure/Isar/keyword.scala	Mon Nov 28 22:05:32 2011 +0100
    23.3 @@ -61,7 +61,8 @@
    23.4    object Keyword_Decl {
    23.5      def unapply(msg: XML.Tree): Option[String] =
    23.6        msg match {
    23.7 -        case XML.Elem(Markup(Markup.KEYWORD_DECL, List((Markup.NAME, name))), _) => Some(name)
    23.8 +        case XML.Elem(Markup(Isabelle_Markup.KEYWORD_DECL, List((Markup.NAME, name))), _) =>
    23.9 +          Some(name)
   23.10          case _ => None
   23.11        }
   23.12    }
   23.13 @@ -69,8 +70,8 @@
   23.14    object Command_Decl {
   23.15      def unapply(msg: XML.Tree): Option[(String, String)] =
   23.16        msg match {
   23.17 -        case XML.Elem(Markup(Markup.COMMAND_DECL, List((Markup.NAME, name), (Markup.KIND, kind))), _) =>
   23.18 -          Some((name, kind))
   23.19 +        case XML.Elem(Markup(Isabelle_Markup.COMMAND_DECL,
   23.20 +            List((Markup.NAME, name), (Markup.KIND, kind))), _) => Some((name, kind))
   23.21          case _ => None
   23.22        }
   23.23    }
    24.1 --- a/src/Pure/Isar/proof.ML	Mon Nov 28 20:39:08 2011 +0100
    24.2 +++ b/src/Pure/Isar/proof.ML	Mon Nov 28 22:05:32 2011 +0100
    24.3 @@ -522,7 +522,7 @@
    24.4  
    24.5  fun status_markup state =
    24.6    (case try goal state of
    24.7 -    SOME {goal, ...} => Markup.proof_state (Thm.nprems_of goal)
    24.8 +    SOME {goal, ...} => Isabelle_Markup.proof_state (Thm.nprems_of goal)
    24.9    | NONE => Markup.empty);
   24.10  
   24.11  
   24.12 @@ -998,7 +998,8 @@
   24.13      fun print_rule ctxt th =
   24.14        if ! testing then rule := SOME th
   24.15        else if int then
   24.16 -        writeln (Markup.markup Markup.state (Proof_Display.string_of_rule ctxt "Successful" th))
   24.17 +        writeln
   24.18 +          (Markup.markup Isabelle_Markup.state (Proof_Display.string_of_rule ctxt "Successful" th))
   24.19        else ();
   24.20      val test_proof =
   24.21        try (local_skip_proof true)
    25.1 --- a/src/Pure/Isar/proof_context.ML	Mon Nov 28 20:39:08 2011 +0100
    25.2 +++ b/src/Pure/Isar/proof_context.ML	Mon Nov 28 22:05:32 2011 +0100
    25.3 @@ -463,7 +463,7 @@
    25.4      val (c, pos) = token_content text;
    25.5    in
    25.6      if Lexicon.is_tid c then
    25.7 -     (Context_Position.report ctxt pos Markup.tfree;
    25.8 +     (Context_Position.report ctxt pos Isabelle_Markup.tfree;
    25.9        TFree (c, default_sort ctxt (c, ~1)))
   25.10      else
   25.11        let
   25.12 @@ -495,7 +495,8 @@
   25.13      (case (Variable.lookup_fixed ctxt c, Variable.is_const ctxt c) of
   25.14        (SOME x, false) =>
   25.15          (Context_Position.report ctxt pos
   25.16 -            (Markup.name x (if can Name.dest_skolem x then Markup.skolem else Markup.free));
   25.17 +            (Markup.name x
   25.18 +              (if can Name.dest_skolem x then Isabelle_Markup.skolem else Isabelle_Markup.free));
   25.19            Free (x, infer_type ctxt (x, ty)))
   25.20      | _ => prep_const_proper ctxt strict (c, pos))
   25.21    end;
    26.1 --- a/src/Pure/Isar/runtime.ML	Mon Nov 28 20:39:08 2011 +0100
    26.2 +++ b/src/Pure/Isar/runtime.ML	Mon Nov 28 22:05:32 2011 +0100
    26.3 @@ -65,7 +65,7 @@
    26.4      fun exn_msgs (context, (i, exn)) =
    26.5        (case exn of
    26.6          EXCURSION_FAIL (exn, loc) =>
    26.7 -          map (apsnd (fn msg => msg ^ Markup.markup Markup.no_report ("\n" ^ loc)))
    26.8 +          map (apsnd (fn msg => msg ^ Markup.markup Isabelle_Markup.no_report ("\n" ^ loc)))
    26.9              (sorted_msgs context exn)
   26.10        | _ =>
   26.11          let
    27.1 --- a/src/Pure/Isar/token.ML	Mon Nov 28 20:39:08 2011 +0100
    27.2 +++ b/src/Pure/Isar/token.ML	Mon Nov 28 22:05:32 2011 +0100
    27.3 @@ -189,7 +189,9 @@
    27.4  
    27.5  fun source_of (Token ((source, (pos, _)), (_, x), _)) =
    27.6    if YXML.detect x then x
    27.7 -  else YXML.string_of (XML.Elem (Markup.token (Position.properties_of pos), [XML.Text source]));
    27.8 +  else
    27.9 +    YXML.string_of
   27.10 +      (XML.Elem (Isabelle_Markup.token (Position.properties_of pos), [XML.Text source]));
   27.11  
   27.12  fun source_position_of (Token ((source, (pos, _)), _, _)) = (source, pos);
   27.13  
    28.1 --- a/src/Pure/Isar/toplevel.ML	Mon Nov 28 20:39:08 2011 +0100
    28.2 +++ b/src/Pure/Isar/toplevel.ML	Mon Nov 28 22:05:32 2011 +0100
    28.3 @@ -210,7 +210,7 @@
    28.4    | SOME (Proof (prf, _)) =>
    28.5        Proof.pretty_state (Proof_Node.position prf) (Proof_Node.current prf)
    28.6    | SOME (SkipProof (d, _)) => [Pretty.str ("skipped proof: depth " ^ string_of_int d)])
    28.7 -  |> Pretty.markup_chunks Markup.state |> Pretty.writeln;
    28.8 +  |> Pretty.markup_chunks Isabelle_Markup.state |> Pretty.writeln;
    28.9  
   28.10  fun pretty_abstract state = Pretty.str ("<Isar " ^ str_of_state state ^ ">");
   28.11  
    29.1 --- a/src/Pure/ML/ml_compiler_polyml-5.3.ML	Mon Nov 28 20:39:08 2011 +0100
    29.2 +++ b/src/Pure/ML/ml_compiler_polyml-5.3.ML	Mon Nov 28 22:05:32 2011 +0100
    29.3 @@ -15,7 +15,7 @@
    29.4        endLine = _, endPosition = end_offset} = loc;
    29.5      val props =
    29.6        (case YXML.parse text of
    29.7 -        XML.Elem ((e, atts), _) => if e = Markup.positionN then atts else []
    29.8 +        XML.Elem ((e, atts), _) => if e = Isabelle_Markup.positionN then atts else []
    29.9        | XML.Text s => Position.file_name s);
   29.10    in
   29.11      Position.make {line = line, offset = offset, end_offset = end_offset, props = props}
   29.12 @@ -41,19 +41,20 @@
   29.13  
   29.14      fun reported_entity kind loc decl =
   29.15        reported_text (position_of loc)
   29.16 -        (Markup.entityN, (Markup.kindN, kind) :: Position.def_properties_of (position_of decl)) "";
   29.17 +        (Isabelle_Markup.entityN,
   29.18 +          (Markup.kindN, kind) :: Position.def_properties_of (position_of decl)) "";
   29.19  
   29.20      fun reported loc (PolyML.PTtype types) =
   29.21            cons
   29.22              (PolyML.NameSpace.displayTypeExpression (types, depth, space)
   29.23                |> pretty_ml |> Pretty.from_ML |> Pretty.string_of
   29.24 -              |> reported_text (position_of loc) Markup.ML_typing)
   29.25 +              |> reported_text (position_of loc) Isabelle_Markup.ML_typing)
   29.26        | reported loc (PolyML.PTdeclaredAt decl) =
   29.27 -          cons (reported_entity Markup.ML_defN loc decl)
   29.28 +          cons (reported_entity Isabelle_Markup.ML_defN loc decl)
   29.29        | reported loc (PolyML.PTopenedAt decl) =
   29.30 -          cons (reported_entity Markup.ML_openN loc decl)
   29.31 +          cons (reported_entity Isabelle_Markup.ML_openN loc decl)
   29.32        | reported loc (PolyML.PTstructureAt decl) =
   29.33 -          cons (reported_entity Markup.ML_structN loc decl)
   29.34 +          cons (reported_entity Isabelle_Markup.ML_structN loc decl)
   29.35        | reported _ (PolyML.PTnextSibling tree) = reported_tree (tree ())
   29.36        | reported _ (PolyML.PTfirstChild tree) = reported_tree (tree ())
   29.37        | reported _ _ = I
   29.38 @@ -72,8 +73,9 @@
   29.39      (* input *)
   29.40  
   29.41      val location_props =
   29.42 -      op ^ (YXML.output_markup (Markup.position |> Markup.properties
   29.43 -            (filter (member (op =) [Markup.idN, Markup.fileN] o #1) (Position.properties_of pos))));
   29.44 +      op ^ (YXML.output_markup (Isabelle_Markup.position |> Markup.properties
   29.45 +            (filter (member (op =)
   29.46 +              [Isabelle_Markup.idN, Isabelle_Markup.fileN] o #1) (Position.properties_of pos))));
   29.47  
   29.48      val input_buffer =
   29.49        Unsynchronized.ref (toks |> map
   29.50 @@ -111,10 +113,10 @@
   29.51        let
   29.52          val pos = position_of loc;
   29.53          val txt =
   29.54 -          (Position.is_reported pos ? Markup.markup Markup.no_report)
   29.55 +          (Position.is_reported pos ? Markup.markup Isabelle_Markup.no_report)
   29.56              ((if hard then "Error" else "Warning") ^ Position.str_of pos ^ ":\n") ^
   29.57            Pretty.string_of (Pretty.from_ML (pretty_ml msg)) ^
   29.58 -          Position.reported_text pos Markup.report "";
   29.59 +          Position.reported_text pos Isabelle_Markup.report "";
   29.60        in if hard then err txt else warn txt end;
   29.61  
   29.62  
    30.1 --- a/src/Pure/ML/ml_context.ML	Mon Nov 28 20:39:08 2011 +0100
    30.2 +++ b/src/Pure/ML/ml_context.ML	Mon Nov 28 22:05:32 2011 +0100
    30.3 @@ -103,7 +103,7 @@
    30.4  structure Antiq_Parsers = Theory_Data
    30.5  (
    30.6    type T = (Position.T -> antiq context_parser) Name_Space.table;
    30.7 -  val empty : T = Name_Space.empty_table Markup.ML_antiquotationN;
    30.8 +  val empty : T = Name_Space.empty_table Isabelle_Markup.ML_antiquotationN;
    30.9    val extend = I;
   30.10    fun merge data : T = Name_Space.merge_tables data;
   30.11  );
   30.12 @@ -121,7 +121,7 @@
   30.13      val thy = Proof_Context.theory_of ctxt;
   30.14      val ((xname, _), pos) = Args.dest_src src;
   30.15      val (_, scan) = Name_Space.check ctxt (Antiq_Parsers.get thy) (xname, pos);
   30.16 -  in Args.context_syntax Markup.ML_antiquotationN (scan pos) src ctxt end;
   30.17 +  in Args.context_syntax Isabelle_Markup.ML_antiquotationN (scan pos) src ctxt end;
   30.18  
   30.19  
   30.20  (* parsing and evaluation *)
    31.1 --- a/src/Pure/ML/ml_lex.ML	Mon Nov 28 20:39:08 2011 +0100
    31.2 +++ b/src/Pure/ML/ml_lex.ML	Mon Nov 28 22:05:32 2011 +0100
    31.3 @@ -104,23 +104,23 @@
    31.4  local
    31.5  
    31.6  val token_kind_markup =
    31.7 - fn Keyword   => Markup.ML_keyword
    31.8 + fn Keyword   => Isabelle_Markup.ML_keyword
    31.9    | Ident     => Markup.empty
   31.10    | LongIdent => Markup.empty
   31.11 -  | TypeVar   => Markup.ML_tvar
   31.12 -  | Word      => Markup.ML_numeral
   31.13 -  | Int       => Markup.ML_numeral
   31.14 -  | Real      => Markup.ML_numeral
   31.15 -  | Char      => Markup.ML_char
   31.16 -  | String    => Markup.ML_string
   31.17 +  | TypeVar   => Isabelle_Markup.ML_tvar
   31.18 +  | Word      => Isabelle_Markup.ML_numeral
   31.19 +  | Int       => Isabelle_Markup.ML_numeral
   31.20 +  | Real      => Isabelle_Markup.ML_numeral
   31.21 +  | Char      => Isabelle_Markup.ML_char
   31.22 +  | String    => Isabelle_Markup.ML_string
   31.23    | Space     => Markup.empty
   31.24 -  | Comment   => Markup.ML_comment
   31.25 -  | Error _   => Markup.ML_malformed
   31.26 +  | Comment   => Isabelle_Markup.ML_comment
   31.27 +  | Error _   => Isabelle_Markup.ML_malformed
   31.28    | EOF       => Markup.empty;
   31.29  
   31.30  fun token_markup kind x =
   31.31    if kind = Keyword andalso exists_string (not o Symbol.is_ascii_letter) x
   31.32 -  then Markup.ML_delimiter
   31.33 +  then Isabelle_Markup.ML_delimiter
   31.34    else token_kind_markup kind;
   31.35  
   31.36  in
   31.37 @@ -278,7 +278,7 @@
   31.38  
   31.39  fun read pos txt =
   31.40    let
   31.41 -    val _ = Position.report pos Markup.ML_source;
   31.42 +    val _ = Position.report pos Isabelle_Markup.ML_source;
   31.43      val syms = Symbol_Pos.explode (txt, pos);
   31.44      val termination =
   31.45        if null syms then []
    32.1 --- a/src/Pure/PIDE/command.scala	Mon Nov 28 20:39:08 2011 +0100
    32.2 +++ b/src/Pure/PIDE/command.scala	Mon Nov 28 22:05:32 2011 +0100
    32.3 @@ -32,7 +32,7 @@
    32.4  
    32.5      def root_info: Text.Markup =
    32.6        Text.Info(command.range,
    32.7 -        XML.Elem(Markup(Markup.STATUS, Nil), status.reverse.map(XML.Elem(_, Nil))))
    32.8 +        XML.Elem(Markup(Isabelle_Markup.STATUS, Nil), status.reverse.map(XML.Elem(_, Nil))))
    32.9      def root_markup: Markup_Tree = markup + root_info
   32.10  
   32.11  
   32.12 @@ -40,14 +40,14 @@
   32.13  
   32.14      def accumulate(message: XML.Elem): Command.State =
   32.15        message match {
   32.16 -        case XML.Elem(Markup(Markup.STATUS, _), msgs) =>
   32.17 +        case XML.Elem(Markup(Isabelle_Markup.STATUS, _), msgs) =>
   32.18            (this /: msgs)((state, msg) =>
   32.19              msg match {
   32.20                case XML.Elem(markup, Nil) => state.add_status(markup)
   32.21                case _ => System.err.println("Ignored status message: " + msg); state
   32.22              })
   32.23  
   32.24 -        case XML.Elem(Markup(Markup.REPORT, _), msgs) =>
   32.25 +        case XML.Elem(Markup(Isabelle_Markup.REPORT, _), msgs) =>
   32.26            (this /: msgs)((state, msg) =>
   32.27              msg match {
   32.28                case XML.Elem(Markup(name, atts @ Position.Id_Range(id, raw_range)), args)
   32.29 @@ -62,7 +62,7 @@
   32.30              })
   32.31          case XML.Elem(Markup(name, atts), body) =>
   32.32            atts match {
   32.33 -            case Markup.Serial(i) =>
   32.34 +            case Isabelle_Markup.Serial(i) =>
   32.35                val result = XML.Elem(Markup(name, Position.purge(atts)), body)
   32.36                val st0 = add_result(i, result)
   32.37                val st1 =
    33.1 --- a/src/Pure/PIDE/document.ML	Mon Nov 28 20:39:08 2011 +0100
    33.2 +++ b/src/Pure/PIDE/document.ML	Mon Nov 28 22:05:32 2011 +0100
    33.3 @@ -333,22 +333,22 @@
    33.4      val is_proof = Keyword.is_proof (Toplevel.name_of tr);
    33.5  
    33.6      val _ = Multithreading.interrupted ();
    33.7 -    val _ = Toplevel.status tr Markup.forked;
    33.8 +    val _ = Toplevel.status tr Isabelle_Markup.forked;
    33.9      val start = Timing.start ();
   33.10      val (errs, result) = run (is_init orelse is_proof) (Toplevel.set_print false tr) st;
   33.11      val _ = timing tr (Timing.result start);
   33.12 -    val _ = Toplevel.status tr Markup.joined;
   33.13 +    val _ = Toplevel.status tr Isabelle_Markup.joined;
   33.14      val _ = List.app (Toplevel.error_msg tr) errs;
   33.15    in
   33.16      (case result of
   33.17        NONE =>
   33.18          let
   33.19            val _ = if null errs then Exn.interrupt () else ();
   33.20 -          val _ = Toplevel.status tr Markup.failed;
   33.21 +          val _ = Toplevel.status tr Isabelle_Markup.failed;
   33.22          in (st, no_print) end
   33.23      | SOME st' =>
   33.24          let
   33.25 -          val _ = Toplevel.status tr Markup.finished;
   33.26 +          val _ = Toplevel.status tr Isabelle_Markup.finished;
   33.27            val _ = proof_status tr st';
   33.28            val do_print =
   33.29              not is_init andalso
    34.1 --- a/src/Pure/PIDE/isar_document.ML	Mon Nov 28 20:39:08 2011 +0100
    34.2 +++ b/src/Pure/PIDE/isar_document.ML	Mon Nov 28 22:05:32 2011 +0100
    34.3 @@ -57,7 +57,7 @@
    34.4          val (assignment, state1) = Document.update old_id new_id edits state;
    34.5          val _ = Future.join_tasks running;
    34.6          val _ =
    34.7 -          Output.raw_message Markup.assign_execs
    34.8 +          Output.raw_message Isabelle_Markup.assign_execs
    34.9              ((new_id, assignment) |>
   34.10                let open XML.Encode
   34.11                in pair int (pair (list (pair int (option int))) (list (pair string (option int)))) end
   34.12 @@ -73,7 +73,7 @@
   34.13            YXML.parse_body versions_yxml |>
   34.14              let open XML.Decode in list int end;
   34.15          val state1 = Document.remove_versions versions state;
   34.16 -        val _ = Output.raw_message Markup.removed_versions versions_yxml;
   34.17 +        val _ = Output.raw_message Isabelle_Markup.removed_versions versions_yxml;
   34.18        in state1 end));
   34.19  
   34.20  val _ =
    35.1 --- a/src/Pure/PIDE/isar_document.scala	Mon Nov 28 20:39:08 2011 +0100
    35.2 +++ b/src/Pure/PIDE/isar_document.scala	Mon Nov 28 22:05:32 2011 +0100
    35.3 @@ -52,13 +52,13 @@
    35.4    def command_status(markup: List[Markup]): Status =
    35.5    {
    35.6      val forks = (0 /: markup) {
    35.7 -      case (i, Markup(Markup.FORKED, _)) => i + 1
    35.8 -      case (i, Markup(Markup.JOINED, _)) => i - 1
    35.9 +      case (i, Markup(Isabelle_Markup.FORKED, _)) => i + 1
   35.10 +      case (i, Markup(Isabelle_Markup.JOINED, _)) => i - 1
   35.11        case (i, _) => i
   35.12      }
   35.13      if (forks != 0) Forked(forks)
   35.14 -    else if (markup.exists(_.name == Markup.FAILED)) Failed
   35.15 -    else if (markup.exists(_.name == Markup.FINISHED)) Finished
   35.16 +    else if (markup.exists(_.name == Isabelle_Markup.FAILED)) Failed
   35.17 +    else if (markup.exists(_.name == Isabelle_Markup.FINISHED)) Finished
   35.18      else Unprocessed
   35.19    }
   35.20  
   35.21 @@ -88,12 +88,12 @@
   35.22    /* result messages */
   35.23  
   35.24    def clean_message(body: XML.Body): XML.Body =
   35.25 -    body filter { case XML.Elem(Markup(Markup.NO_REPORT, _), _) => false case _ => true } map
   35.26 +    body filter { case XML.Elem(Markup(Isabelle_Markup.NO_REPORT, _), _) => false case _ => true } map
   35.27        { case XML.Elem(markup, ts) => XML.Elem(markup, clean_message(ts)) case t => t }
   35.28  
   35.29    def message_reports(msg: XML.Tree): List[XML.Elem] =
   35.30      msg match {
   35.31 -      case elem @ XML.Elem(Markup(Markup.REPORT, _), _) => List(elem)
   35.32 +      case elem @ XML.Elem(Markup(Isabelle_Markup.REPORT, _), _) => List(elem)
   35.33        case XML.Elem(_, body) => body.flatMap(message_reports)
   35.34        case XML.Text(_) => Nil
   35.35      }
   35.36 @@ -103,33 +103,33 @@
   35.37  
   35.38    def is_ready(msg: XML.Tree): Boolean =
   35.39      msg match {
   35.40 -      case XML.Elem(Markup(Markup.STATUS, _),
   35.41 -        List(XML.Elem(Markup(Markup.READY, _), _))) => true
   35.42 +      case XML.Elem(Markup(Isabelle_Markup.STATUS, _),
   35.43 +        List(XML.Elem(Markup(Isabelle_Markup.READY, _), _))) => true
   35.44        case _ => false
   35.45      }
   35.46  
   35.47   def is_tracing(msg: XML.Tree): Boolean =
   35.48      msg match {
   35.49 -      case XML.Elem(Markup(Markup.TRACING, _), _) => true
   35.50 +      case XML.Elem(Markup(Isabelle_Markup.TRACING, _), _) => true
   35.51        case _ => false
   35.52      }
   35.53  
   35.54    def is_warning(msg: XML.Tree): Boolean =
   35.55      msg match {
   35.56 -      case XML.Elem(Markup(Markup.WARNING, _), _) => true
   35.57 +      case XML.Elem(Markup(Isabelle_Markup.WARNING, _), _) => true
   35.58        case _ => false
   35.59      }
   35.60  
   35.61    def is_error(msg: XML.Tree): Boolean =
   35.62      msg match {
   35.63 -      case XML.Elem(Markup(Markup.ERROR, _), _) => true
   35.64 +      case XML.Elem(Markup(Isabelle_Markup.ERROR, _), _) => true
   35.65        case _ => false
   35.66      }
   35.67  
   35.68    def is_state(msg: XML.Tree): Boolean =
   35.69      msg match {
   35.70 -      case XML.Elem(Markup(Markup.WRITELN, _),
   35.71 -        List(XML.Elem(Markup(Markup.STATE, _), _))) => true
   35.72 +      case XML.Elem(Markup(Isabelle_Markup.WRITELN, _),
   35.73 +        List(XML.Elem(Markup(Isabelle_Markup.STATE, _), _))) => true
   35.74        case _ => false
   35.75      }
   35.76  
   35.77 @@ -137,7 +137,8 @@
   35.78    /* reported positions */
   35.79  
   35.80    private val include_pos =
   35.81 -    Set(Markup.BINDING, Markup.ENTITY, Markup.REPORT, Markup.POSITION)
   35.82 +    Set(Isabelle_Markup.BINDING, Isabelle_Markup.ENTITY, Isabelle_Markup.REPORT,
   35.83 +      Isabelle_Markup.POSITION)
   35.84  
   35.85    def message_positions(command: Command, message: XML.Elem): Set[Text.Range] =
   35.86    {
    36.1 --- a/src/Pure/PIDE/yxml.scala	Mon Nov 28 20:39:08 2011 +0100
    36.2 +++ b/src/Pure/PIDE/yxml.scala	Mon Nov 28 22:05:32 2011 +0100
    36.3 @@ -118,18 +118,18 @@
    36.4  
    36.5    /* failsafe parsing */
    36.6  
    36.7 -  private def markup_malformed(source: CharSequence) =
    36.8 -    XML.elem(Markup.MALFORMED, List(XML.Text(source.toString)))
    36.9 +  private def markup_broken(source: CharSequence) =
   36.10 +    XML.elem(Markup.Broken.name, List(XML.Text(source.toString)))
   36.11  
   36.12    def parse_body_failsafe(source: CharSequence): XML.Body =
   36.13    {
   36.14      try { parse_body(source) }
   36.15 -    catch { case ERROR(_) => List(markup_malformed(source)) }
   36.16 +    catch { case ERROR(_) => List(markup_broken(source)) }
   36.17    }
   36.18  
   36.19    def parse_failsafe(source: CharSequence): XML.Tree =
   36.20    {
   36.21      try { parse(source) }
   36.22 -    catch { case ERROR(_) => markup_malformed(source) }
   36.23 +    catch { case ERROR(_) => markup_broken(source) }
   36.24    }
   36.25  }
    37.1 --- a/src/Pure/ProofGeneral/proof_general_emacs.ML	Mon Nov 28 20:39:08 2011 +0100
    37.2 +++ b/src/Pure/ProofGeneral/proof_general_emacs.ML	Mon Nov 28 22:05:32 2011 +0100
    37.3 @@ -34,24 +34,24 @@
    37.4    | render_tree (XML.Elem ((name, props), ts)) =
    37.5        let
    37.6          val (bg1, en1) =
    37.7 -          if name <> Markup.promptN andalso print_mode_active test_markupN
    37.8 +          if name <> Isabelle_Markup.promptN andalso print_mode_active test_markupN
    37.9            then XML.output_markup (name, props)
   37.10            else Markup.no_output;
   37.11          val (bg2, en2) =
   37.12            if null ts then Markup.no_output
   37.13 -          else if name = Markup.stateN then (special "O" ^ "\n", "\n" ^ special "P")
   37.14 -          else if name = Markup.sendbackN then (special "W", special "X")
   37.15 -          else if name = Markup.hiliteN then (special "0", special "1")
   37.16 -          else if name = Markup.tfreeN then (special "C", special "A")
   37.17 -          else if name = Markup.tvarN then (special "D", special "A")
   37.18 -          else if name = Markup.freeN then (special "E", special "A")
   37.19 -          else if name = Markup.boundN then (special "F", special "A")
   37.20 -          else if name = Markup.varN then (special "G", special "A")
   37.21 -          else if name = Markup.skolemN then (special "H", special "A")
   37.22 +          else if name = Isabelle_Markup.stateN then (special "O" ^ "\n", "\n" ^ special "P")
   37.23 +          else if name = Isabelle_Markup.sendbackN then (special "W", special "X")
   37.24 +          else if name = Isabelle_Markup.hiliteN then (special "0", special "1")
   37.25 +          else if name = Isabelle_Markup.tfreeN then (special "C", special "A")
   37.26 +          else if name = Isabelle_Markup.tvarN then (special "D", special "A")
   37.27 +          else if name = Isabelle_Markup.freeN then (special "E", special "A")
   37.28 +          else if name = Isabelle_Markup.boundN then (special "F", special "A")
   37.29 +          else if name = Isabelle_Markup.varN then (special "G", special "A")
   37.30 +          else if name = Isabelle_Markup.skolemN then (special "H", special "A")
   37.31            else
   37.32 -            (case Markup.get_entity_kind (name, props) of
   37.33 +            (case Isabelle_Markup.get_entity_kind (name, props) of
   37.34                SOME kind =>
   37.35 -                if kind = Markup.classN then (special "B", special "A")
   37.36 +                if kind = Isabelle_Markup.classN then (special "B", special "A")
   37.37                  else Markup.no_output
   37.38              | NONE => Markup.no_output);
   37.39        in
   37.40 @@ -108,7 +108,7 @@
   37.41    emacs_notify ("Proof General, you can unlock the file " ^ quote (File.platform_path path));
   37.42  
   37.43  fun sendback heading prts =
   37.44 -  Pretty.writeln (Pretty.big_list heading [Pretty.markup Markup.sendback prts]);
   37.45 +  Pretty.writeln (Pretty.big_list heading [Pretty.markup Isabelle_Markup.sendback prts]);
   37.46  
   37.47  
   37.48  (* theory loader actions *)
    38.1 --- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Mon Nov 28 20:39:08 2011 +0100
    38.2 +++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Mon Nov 28 22:05:32 2011 +0100
    38.3 @@ -101,8 +101,8 @@
    38.4  val pgml_syms = map pgml_sym o Symbol.explode;
    38.5  
    38.6  val token_markups =
    38.7 - [Markup.tfreeN, Markup.tvarN, Markup.freeN,
    38.8 -  Markup.boundN, Markup.varN, Markup.skolemN];
    38.9 + [Isabelle_Markup.tfreeN, Isabelle_Markup.tvarN, Isabelle_Markup.freeN,
   38.10 +  Isabelle_Markup.boundN, Isabelle_Markup.varN, Isabelle_Markup.skolemN];
   38.11  
   38.12  in
   38.13  
   38.14 @@ -112,10 +112,11 @@
   38.15          in [Pgml.Atoms {kind = SOME name, content = content}] end
   38.16        else
   38.17          let val content = maps pgml_terms body in
   38.18 -          if name = Markup.blockN then
   38.19 -            [Pgml.Box {orient = NONE, indent = Properties.get_int atts Markup.indentN, content = content}]
   38.20 -          else if name = Markup.breakN then
   38.21 -            [Pgml.Break {mandatory = NONE, indent = Properties.get_int atts Markup.widthN}]
   38.22 +          if name = Isabelle_Markup.blockN then
   38.23 +            [Pgml.Box {orient = NONE,
   38.24 +              indent = Properties.get_int atts Isabelle_Markup.indentN, content = content}]
   38.25 +          else if name = Isabelle_Markup.breakN then
   38.26 +            [Pgml.Break {mandatory = NONE, indent = Properties.get_int atts Isabelle_Markup.widthN}]
   38.27            else content
   38.28          end
   38.29    | pgml_terms (XML.Text text) = map (Pgml.Raw o Pgml.atom_to_xml) (pgml_syms text);
   38.30 @@ -134,7 +135,7 @@
   38.31      val area =
   38.32        (case body of
   38.33          [XML.Elem ((name, _), _)] =>
   38.34 -          if name = Markup.stateN then PgipTypes.Display else default_area
   38.35 +          if name = Isabelle_Markup.stateN then PgipTypes.Display else default_area
   38.36        | _ => default_area);
   38.37    in Pgml.pgml_to_xml (pgml area (maps pgml_terms body)) end;
   38.38  
    39.1 --- a/src/Pure/ROOT.ML	Mon Nov 28 20:39:08 2011 +0100
    39.2 +++ b/src/Pure/ROOT.ML	Mon Nov 28 22:05:32 2011 +0100
    39.3 @@ -31,7 +31,8 @@
    39.4  use "General/output.ML";
    39.5  use "General/timing.ML";
    39.6  use "General/markup.ML";
    39.7 -fun legacy_feature s = warning (Markup.markup Markup.legacy ("Legacy feature! " ^ s));
    39.8 +use "General/isabelle_markup.ML";
    39.9 +fun legacy_feature s = warning (Markup.markup Isabelle_Markup.legacy ("Legacy feature! " ^ s));
   39.10  use "General/scan.ML";
   39.11  use "General/source.ML";
   39.12  use "General/symbol.ML";
    40.1 --- a/src/Pure/Syntax/lexicon.ML	Mon Nov 28 20:39:08 2011 +0100
    40.2 +++ b/src/Pure/Syntax/lexicon.ML	Mon Nov 28 22:05:32 2011 +0100
    40.3 @@ -189,29 +189,29 @@
    40.4  (* markup *)
    40.5  
    40.6  val token_kind_markup =
    40.7 - fn Literal     => Markup.literal
    40.8 + fn Literal     => Isabelle_Markup.literal
    40.9    | IdentSy     => Markup.empty
   40.10    | LongIdentSy => Markup.empty
   40.11 -  | VarSy       => Markup.var
   40.12 -  | TFreeSy     => Markup.tfree
   40.13 -  | TVarSy      => Markup.tvar
   40.14 -  | NumSy       => Markup.numeral
   40.15 -  | FloatSy     => Markup.numeral
   40.16 -  | XNumSy      => Markup.numeral
   40.17 -  | StrSy       => Markup.inner_string
   40.18 +  | VarSy       => Isabelle_Markup.var
   40.19 +  | TFreeSy     => Isabelle_Markup.tfree
   40.20 +  | TVarSy      => Isabelle_Markup.tvar
   40.21 +  | NumSy       => Isabelle_Markup.numeral
   40.22 +  | FloatSy     => Isabelle_Markup.numeral
   40.23 +  | XNumSy      => Isabelle_Markup.numeral
   40.24 +  | StrSy       => Isabelle_Markup.inner_string
   40.25    | Space       => Markup.empty
   40.26 -  | Comment     => Markup.inner_comment
   40.27 +  | Comment     => Isabelle_Markup.inner_comment
   40.28    | EOF         => Markup.empty;
   40.29  
   40.30  fun report_of_token (Token (kind, s, (pos, _))) =
   40.31    let val markup =
   40.32 -    if kind = Literal andalso not (is_ascii_identifier s) then Markup.delimiter
   40.33 +    if kind = Literal andalso not (is_ascii_identifier s) then Isabelle_Markup.delimiter
   40.34      else token_kind_markup kind
   40.35    in (pos, markup) end;
   40.36  
   40.37  fun reported_token_range ctxt tok =
   40.38    if is_proper tok
   40.39 -  then Context_Position.reported_text ctxt (pos_of_token tok) Markup.token_range ""
   40.40 +  then Context_Position.reported_text ctxt (pos_of_token tok) Isabelle_Markup.token_range ""
   40.41    else "";
   40.42  
   40.43  
    41.1 --- a/src/Pure/Syntax/syntax.ML	Mon Nov 28 20:39:08 2011 +0100
    41.2 +++ b/src/Pure/Syntax/syntax.ML	Mon Nov 28 22:05:32 2011 +0100
    41.3 @@ -185,7 +185,7 @@
    41.4      val pos =
    41.5        (case tree of
    41.6          XML.Elem ((name, props), _) =>
    41.7 -          if name = Markup.tokenN then Position.of_properties props
    41.8 +          if name = Isabelle_Markup.tokenN then Position.of_properties props
    41.9            else Position.none
   41.10        | XML.Text _ => Position.none);
   41.11    in (Symbol_Pos.explode (text, pos), pos) end;
   41.12 @@ -202,7 +202,7 @@
   41.13    in
   41.14      (case YXML.parse_body str handle Fail msg => error msg of
   41.15        body as [tree as XML.Elem ((name, _), _)] =>
   41.16 -        if name = Markup.tokenN then parse_tree tree else decode body
   41.17 +        if name = Isabelle_Markup.tokenN then parse_tree tree else decode body
   41.18      | [tree as XML.Text _] => parse_tree tree
   41.19      | body => decode body)
   41.20    end;
    42.1 --- a/src/Pure/Syntax/syntax_phases.ML	Mon Nov 28 20:39:08 2011 +0100
    42.2 +++ b/src/Pure/Syntax/syntax_phases.ML	Mon Nov 28 22:05:32 2011 +0100
    42.3 @@ -51,16 +51,16 @@
    42.4    [Name_Space.markup (Consts.space_of (Proof_Context.consts_of ctxt)) c];
    42.5  
    42.6  fun markup_free ctxt x =
    42.7 -  [if can Name.dest_skolem x then Markup.skolem else Markup.free] @
    42.8 +  [if can Name.dest_skolem x then Isabelle_Markup.skolem else Isabelle_Markup.free] @
    42.9    (if Variable.is_body ctxt orelse Variable.is_fixed ctxt x
   42.10     then [Variable.markup_fixed ctxt x]
   42.11     else []);
   42.12  
   42.13 -fun markup_var xi = [Markup.name (Term.string_of_vname xi) Markup.var];
   42.14 +fun markup_var xi = [Markup.name (Term.string_of_vname xi) Isabelle_Markup.var];
   42.15  
   42.16  fun markup_bound def ps (name, id) =
   42.17 -  let val entity = Markup.entity Markup.boundN name in
   42.18 -    Markup.bound ::
   42.19 +  let val entity = Isabelle_Markup.entity Isabelle_Markup.boundN name in
   42.20 +    Isabelle_Markup.bound ::
   42.21        map (fn pos => Markup.properties (Position.entity_properties_of def id pos) entity) ps
   42.22    end;
   42.23  
   42.24 @@ -284,7 +284,8 @@
   42.25      val pts = Syntax.parse syn root (filter Lexicon.is_proper toks)
   42.26        handle ERROR msg =>
   42.27          error (msg ^
   42.28 -          implode (map (Markup.markup Markup.report o Lexicon.reported_token_range ctxt) toks));
   42.29 +          implode
   42.30 +            (map (Markup.markup Isabelle_Markup.report o Lexicon.reported_token_range ctxt) toks));
   42.31      val len = length pts;
   42.32  
   42.33      val limit = Config.get ctxt Syntax.ambiguity_limit;
   42.34 @@ -320,10 +321,11 @@
   42.35  
   42.36  fun parse_failed ctxt pos msg kind =
   42.37    cat_error msg ("Failed to parse " ^ kind ^
   42.38 -    Markup.markup Markup.report (Context_Position.reported_text ctxt pos Markup.bad ""));
   42.39 +    Markup.markup Isabelle_Markup.report
   42.40 +      (Context_Position.reported_text ctxt pos Isabelle_Markup.bad ""));
   42.41  
   42.42  fun parse_sort ctxt =
   42.43 -  Syntax.parse_token ctxt Term_XML.Decode.sort Markup.sort
   42.44 +  Syntax.parse_token ctxt Term_XML.Decode.sort Isabelle_Markup.sort
   42.45      (fn (syms, pos) =>
   42.46        parse_raw ctxt "sort" (syms, pos)
   42.47        |> report_result ctxt pos
   42.48 @@ -332,7 +334,7 @@
   42.49        handle ERROR msg => parse_failed ctxt pos msg "sort");
   42.50  
   42.51  fun parse_typ ctxt =
   42.52 -  Syntax.parse_token ctxt Term_XML.Decode.typ Markup.typ
   42.53 +  Syntax.parse_token ctxt Term_XML.Decode.typ Isabelle_Markup.typ
   42.54      (fn (syms, pos) =>
   42.55        parse_raw ctxt "type" (syms, pos)
   42.56        |> report_result ctxt pos
   42.57 @@ -343,8 +345,8 @@
   42.58    let
   42.59      val (markup, kind, root, constrain) =
   42.60        if is_prop
   42.61 -      then (Markup.prop, "proposition", "prop", Type.constraint propT)
   42.62 -      else (Markup.term, "term", Config.get ctxt Syntax.root, I);
   42.63 +      then (Isabelle_Markup.prop, "proposition", "prop", Type.constraint propT)
   42.64 +      else (Isabelle_Markup.term, "term", Config.get ctxt Syntax.root, I);
   42.65      val decode = constrain o Term_XML.Decode.term;
   42.66    in
   42.67      Syntax.parse_token ctxt decode markup
   42.68 @@ -592,34 +594,34 @@
   42.69    let
   42.70      val m =
   42.71        if Variable.is_fixed ctxt x orelse Syntax.is_pretty_global ctxt
   42.72 -      then Markup.fixed x
   42.73 -      else Markup.hilite;
   42.74 +      then Isabelle_Markup.fixed x
   42.75 +      else Isabelle_Markup.hilite;
   42.76    in
   42.77      if can Name.dest_skolem x
   42.78 -    then ([m, Markup.skolem], Variable.revert_fixed ctxt x)
   42.79 -    else ([m, Markup.free], x)
   42.80 +    then ([m, Isabelle_Markup.skolem], Variable.revert_fixed ctxt x)
   42.81 +    else ([m, Isabelle_Markup.free], x)
   42.82    end;
   42.83  
   42.84  fun var_or_skolem s =
   42.85    (case Lexicon.read_variable s of
   42.86      SOME (x, i) =>
   42.87        (case try Name.dest_skolem x of
   42.88 -        NONE => (Markup.var, s)
   42.89 -      | SOME x' => (Markup.skolem, Term.string_of_vname (x', i)))
   42.90 -  | NONE => (Markup.var, s));
   42.91 +        NONE => (Isabelle_Markup.var, s)
   42.92 +      | SOME x' => (Isabelle_Markup.skolem, Term.string_of_vname (x', i)))
   42.93 +  | NONE => (Isabelle_Markup.var, s));
   42.94  
   42.95  fun unparse_t t_to_ast prt_t markup ctxt t =
   42.96    let
   42.97      val syn = Proof_Context.syn_of ctxt;
   42.98  
   42.99 -    fun token_trans "_tfree" x = SOME (Pretty.mark_str (Markup.tfree, x))
  42.100 -      | token_trans "_tvar" x = SOME (Pretty.mark_str (Markup.tvar, x))
  42.101 +    fun token_trans "_tfree" x = SOME (Pretty.mark_str (Isabelle_Markup.tfree, x))
  42.102 +      | token_trans "_tvar" x = SOME (Pretty.mark_str (Isabelle_Markup.tvar, x))
  42.103        | token_trans "_free" x = SOME (Pretty.marks_str (free_or_skolem ctxt x))
  42.104 -      | token_trans "_bound" x = SOME (Pretty.mark_str (Markup.bound, x))
  42.105 -      | token_trans "_loose" x = SOME (Pretty.mark_str (Markup.malformed, x))
  42.106 +      | token_trans "_bound" x = SOME (Pretty.mark_str (Isabelle_Markup.bound, x))
  42.107 +      | token_trans "_loose" x = SOME (Pretty.mark_str (Isabelle_Markup.malformed, x))
  42.108        | token_trans "_var" x = SOME (Pretty.mark_str (var_or_skolem x))
  42.109 -      | token_trans "_numeral" x = SOME (Pretty.mark_str (Markup.numeral, x))
  42.110 -      | token_trans "_inner_string" x = SOME (Pretty.mark_str (Markup.inner_string, x))
  42.111 +      | token_trans "_numeral" x = SOME (Pretty.mark_str (Isabelle_Markup.numeral, x))
  42.112 +      | token_trans "_inner_string" x = SOME (Pretty.mark_str (Isabelle_Markup.inner_string, x))
  42.113        | token_trans _ _ = NONE;
  42.114  
  42.115      fun markup_extern c =
  42.116 @@ -641,8 +643,8 @@
  42.117  
  42.118  in
  42.119  
  42.120 -val unparse_sort = unparse_t sort_to_ast Printer.pretty_typ_ast Markup.sort;
  42.121 -val unparse_typ = unparse_t typ_to_ast Printer.pretty_typ_ast Markup.typ;
  42.122 +val unparse_sort = unparse_t sort_to_ast Printer.pretty_typ_ast Isabelle_Markup.sort;
  42.123 +val unparse_typ = unparse_t typ_to_ast Printer.pretty_typ_ast Isabelle_Markup.typ;
  42.124  
  42.125  fun unparse_term ctxt =
  42.126    let
  42.127 @@ -652,7 +654,7 @@
  42.128    in
  42.129      unparse_t (term_to_ast idents (is_some o Syntax.lookup_const syn))
  42.130        (Printer.pretty_term_ast (not (Pure_Thy.old_appl_syntax thy)))
  42.131 -      Markup.term ctxt
  42.132 +      Isabelle_Markup.term ctxt
  42.133    end;
  42.134  
  42.135  end;
  42.136 @@ -813,7 +815,7 @@
  42.137      val _ =
  42.138        map2 (fn (pos, _) => fn ty =>
  42.139          if Position.is_reported pos then
  42.140 -          Markup.markup (Position.markup pos Markup.typing)
  42.141 +          Markup.markup (Position.markup pos Isabelle_Markup.typing)
  42.142              (Syntax.string_of_typ ctxt (Logic.dest_type ty))
  42.143          else "") ps tys'
  42.144        |> implode |> Output.report
    43.1 --- a/src/Pure/Syntax/term_position.ML	Mon Nov 28 20:39:08 2011 +0100
    43.2 +++ b/src/Pure/Syntax/term_position.ML	Mon Nov 28 22:05:32 2011 +0100
    43.3 @@ -25,15 +25,15 @@
    43.4  val position_text = XML.Text position_dummy;
    43.5  
    43.6  fun pretty pos =
    43.7 -  Pretty.markup (Position.markup pos Markup.position) [Pretty.str position_dummy];
    43.8 +  Pretty.markup (Position.markup pos Isabelle_Markup.position) [Pretty.str position_dummy];
    43.9  
   43.10  fun encode pos =
   43.11 -  YXML.string_of (XML.Elem (Position.markup pos Markup.position, [position_text]));
   43.12 +  YXML.string_of (XML.Elem (Position.markup pos Isabelle_Markup.position, [position_text]));
   43.13  
   43.14  fun decode str =
   43.15    (case YXML.parse_body str handle Fail msg => error msg of
   43.16      [XML.Elem ((name, props), [arg])] =>
   43.17 -      if name = Markup.positionN andalso arg = position_text
   43.18 +      if name = Isabelle_Markup.positionN andalso arg = position_text
   43.19        then SOME (Position.of_properties props)
   43.20        else NONE
   43.21    | _ => NONE);
    44.1 --- a/src/Pure/System/invoke_scala.ML	Mon Nov 28 20:39:08 2011 +0100
    44.2 +++ b/src/Pure/System/invoke_scala.ML	Mon Nov 28 22:05:32 2011 +0100
    44.3 @@ -33,10 +33,10 @@
    44.4  fun promise_method name arg =
    44.5    let
    44.6      val id = new_id ();
    44.7 -    fun abort () = Output.raw_message (Markup.cancel_scala id) "";
    44.8 +    fun abort () = Output.raw_message (Isabelle_Markup.cancel_scala id) "";
    44.9      val promise = Future.promise abort : string future;
   44.10      val _ = Synchronized.change promises (Symtab.update (id, promise));
   44.11 -    val _ = Output.raw_message (Markup.invoke_scala name id) arg;
   44.12 +    val _ = Output.raw_message (Isabelle_Markup.invoke_scala name id) arg;
   44.13    in promise end;
   44.14  
   44.15  fun method name arg = Future.join (promise_method name arg);
    45.1 --- a/src/Pure/System/isabelle_process.ML	Mon Nov 28 20:39:08 2011 +0100
    45.2 +++ b/src/Pure/System/isabelle_process.ML	Mon Nov 28 22:05:32 2011 +0100
    45.3 @@ -77,7 +77,7 @@
    45.4    if body = "" then ()
    45.5    else
    45.6      message false mbox ch
    45.7 -      ((case opt_serial of SOME i => cons (Markup.serialN, string_of_int i) | _ => I)
    45.8 +      ((case opt_serial of SOME i => cons (Isabelle_Markup.serialN, string_of_int i) | _ => I)
    45.9          (Position.properties_of (Position.thread_data ()))) body;
   45.10  
   45.11  fun message_output mbox channel =
   45.12 @@ -189,7 +189,7 @@
   45.13  
   45.14      val _ = Keyword.status ();
   45.15      val _ = Thy_Info.status ();
   45.16 -    val _ = Output.status (Markup.markup Markup.ready "process ready");
   45.17 +    val _ = Output.status (Markup.markup Isabelle_Markup.ready "process ready");
   45.18    in loop channel end));
   45.19  
   45.20  fun init_fifos fifo1 fifo2 = init (fn () => System_Channel.fifo_rendezvous fifo1 fifo2);
    46.1 --- a/src/Pure/System/isabelle_process.scala	Mon Nov 28 20:39:08 2011 +0100
    46.2 +++ b/src/Pure/System/isabelle_process.scala	Mon Nov 28 22:05:32 2011 +0100
    46.3 @@ -23,14 +23,14 @@
    46.4    object Kind
    46.5    {
    46.6      val message_markup = Map(
    46.7 -      ('A' : Int) -> Markup.INIT,
    46.8 -      ('B' : Int) -> Markup.STATUS,
    46.9 -      ('C' : Int) -> Markup.REPORT,
   46.10 -      ('D' : Int) -> Markup.WRITELN,
   46.11 -      ('E' : Int) -> Markup.TRACING,
   46.12 -      ('F' : Int) -> Markup.WARNING,
   46.13 -      ('G' : Int) -> Markup.ERROR,
   46.14 -      ('H' : Int) -> Markup.RAW)
   46.15 +      ('A' : Int) -> Isabelle_Markup.INIT,
   46.16 +      ('B' : Int) -> Isabelle_Markup.STATUS,
   46.17 +      ('C' : Int) -> Isabelle_Markup.REPORT,
   46.18 +      ('D' : Int) -> Isabelle_Markup.WRITELN,
   46.19 +      ('E' : Int) -> Isabelle_Markup.TRACING,
   46.20 +      ('F' : Int) -> Isabelle_Markup.WARNING,
   46.21 +      ('G' : Int) -> Isabelle_Markup.ERROR,
   46.22 +      ('H' : Int) -> Isabelle_Markup.RAW)
   46.23    }
   46.24  
   46.25    sealed abstract class Message
   46.26 @@ -38,9 +38,10 @@
   46.27    class Input(name: String, args: List[String]) extends Message
   46.28    {
   46.29      override def toString: String =
   46.30 -      XML.Elem(Markup(Markup.PROVER_COMMAND, List((Markup.NAME, name))),
   46.31 +      XML.Elem(Markup(Isabelle_Markup.PROVER_COMMAND, List((Markup.NAME, name))),
   46.32          args.map(s =>
   46.33 -          List(XML.Text("\n"), XML.elem(Markup.PROVER_ARG, YXML.parse_body(s)))).flatten).toString
   46.34 +          List(XML.Text("\n"),
   46.35 +            XML.elem(Isabelle_Markup.PROVER_ARG, YXML.parse_body(s)))).flatten).toString
   46.36    }
   46.37  
   46.38    class Result(val message: XML.Elem) extends Message
   46.39 @@ -49,14 +50,14 @@
   46.40      def properties: Properties.T = message.markup.properties
   46.41      def body: XML.Body = message.body
   46.42  
   46.43 -    def is_init = kind == Markup.INIT
   46.44 -    def is_exit = kind == Markup.EXIT
   46.45 -    def is_stdout = kind == Markup.STDOUT
   46.46 -    def is_stderr = kind == Markup.STDERR
   46.47 -    def is_system = kind == Markup.SYSTEM
   46.48 -    def is_status = kind == Markup.STATUS
   46.49 -    def is_report = kind == Markup.REPORT
   46.50 -    def is_raw = kind == Markup.RAW
   46.51 +    def is_init = kind == Isabelle_Markup.INIT
   46.52 +    def is_exit = kind == Isabelle_Markup.EXIT
   46.53 +    def is_stdout = kind == Isabelle_Markup.STDOUT
   46.54 +    def is_stderr = kind == Isabelle_Markup.STDERR
   46.55 +    def is_system = kind == Isabelle_Markup.SYSTEM
   46.56 +    def is_status = kind == Isabelle_Markup.STATUS
   46.57 +    def is_report = kind == Isabelle_Markup.REPORT
   46.58 +    def is_raw = kind == Isabelle_Markup.RAW
   46.59      def is_ready = Isar_Document.is_ready(message)
   46.60      def is_syslog = is_init || is_exit || is_system || is_ready || is_stderr
   46.61  
   46.62 @@ -88,15 +89,15 @@
   46.63  
   46.64    private def system_result(text: String)
   46.65    {
   46.66 -    receiver(new Result(XML.Elem(Markup(Markup.SYSTEM, Nil), List(XML.Text(text)))))
   46.67 +    receiver(new Result(XML.Elem(Markup(Isabelle_Markup.SYSTEM, Nil), List(XML.Text(text)))))
   46.68    }
   46.69  
   46.70    private val xml_cache = new XML.Cache()
   46.71  
   46.72    private def put_result(kind: String, props: Properties.T, body: XML.Body)
   46.73    {
   46.74 -    if (kind == Markup.INIT) system_channel.accepted()
   46.75 -    if (kind == Markup.RAW)
   46.76 +    if (kind == Isabelle_Markup.INIT) system_channel.accepted()
   46.77 +    if (kind == Isabelle_Markup.RAW)
   46.78        receiver(new Result(XML.Elem(Markup(kind, props), body)))
   46.79      else {
   46.80        val msg = XML.Elem(Markup(kind, props), Isar_Document.clean_message(body))
   46.81 @@ -172,7 +173,7 @@
   46.82      system_result(startup_output)
   46.83  
   46.84      if (startup_failed) {
   46.85 -      put_result(Markup.EXIT, "Return code: 127")
   46.86 +      put_result(Isabelle_Markup.EXIT, "Return code: 127")
   46.87        process.stdin.close
   46.88        Thread.sleep(300)
   46.89        terminate_process()
   46.90 @@ -192,7 +193,7 @@
   46.91        for ((thread, _) <- List(standard_input, stdout, stderr, command_input, message))
   46.92          thread.join
   46.93        system_result("process_manager terminated")
   46.94 -      put_result(Markup.EXIT, "Return code: " + rc.toString)
   46.95 +      put_result(Isabelle_Markup.EXIT, "Return code: " + rc.toString)
   46.96      }
   46.97      system_channel.accepted()
   46.98    }
   46.99 @@ -246,8 +247,8 @@
  46.100    private def raw_output_actor(err: Boolean): (Thread, Actor) =
  46.101    {
  46.102      val (name, reader, markup) =
  46.103 -      if (err) ("standard_error", process.stderr, Markup.STDERR)
  46.104 -      else ("standard_output", process.stdout, Markup.STDOUT)
  46.105 +      if (err) ("standard_error", process.stderr, Isabelle_Markup.STDERR)
  46.106 +      else ("standard_output", process.stdout, Isabelle_Markup.STDOUT)
  46.107  
  46.108      Simple_Thread.actor(name) {
  46.109        var result = new StringBuilder(100)
  46.110 @@ -363,7 +364,7 @@
  46.111              case List(XML.Elem(Markup(name, props), Nil))
  46.112                  if name.size == 1 && Kind.message_markup.isDefinedAt(name(0)) =>
  46.113                val kind = Kind.message_markup(name(0))
  46.114 -              val body = read_chunk(kind != Markup.RAW)
  46.115 +              val body = read_chunk(kind != Isabelle_Markup.RAW)
  46.116                put_result(kind, props, body)
  46.117              case _ =>
  46.118                read_chunk(false)
    47.1 --- a/src/Pure/System/session.scala	Mon Nov 28 20:39:08 2011 +0100
    47.2 +++ b/src/Pure/System/session.scala	Mon Nov 28 22:05:32 2011 +0100
    47.3 @@ -363,7 +363,7 @@
    47.4            catch {
    47.5              case _: Document.State.Fail => bad_result(result)
    47.6            }
    47.7 -        case Markup.Assign_Execs if result.is_raw =>
    47.8 +        case Isabelle_Markup.Assign_Execs if result.is_raw =>
    47.9            XML.content(result.body).mkString match {
   47.10              case Isar_Document.Assign(id, assign) =>
   47.11                try { handle_assign(id, assign) }
   47.12 @@ -376,20 +376,20 @@
   47.13              if (!old_versions.isEmpty) prover.get.remove_versions(old_versions)
   47.14              prune_next = System.currentTimeMillis() + prune_delay.ms
   47.15            }
   47.16 -        case Markup.Removed_Versions if result.is_raw =>
   47.17 +        case Isabelle_Markup.Removed_Versions if result.is_raw =>
   47.18            XML.content(result.body).mkString match {
   47.19              case Isar_Document.Removed(removed) =>
   47.20                try { handle_removed(removed) }
   47.21                catch { case _: Document.State.Fail => bad_result(result) }
   47.22              case _ => bad_result(result)
   47.23            }
   47.24 -        case Markup.Invoke_Scala(name, id) if result.is_raw =>
   47.25 +        case Isabelle_Markup.Invoke_Scala(name, id) if result.is_raw =>
   47.26            Future.fork {
   47.27              val arg = XML.content(result.body).mkString
   47.28              val (tag, res) = Invoke_Scala.method(name, arg)
   47.29              prover.get.invoke_scala(id, tag, res)
   47.30            }
   47.31 -        case Markup.Cancel_Scala(id) =>
   47.32 +        case Isabelle_Markup.Cancel_Scala(id) =>
   47.33            System.err.println("cancel_scala " + id)  // FIXME cancel JVM task
   47.34          case _ =>
   47.35            if (result.is_syslog) {
    48.1 --- a/src/Pure/Thy/html.ML	Mon Nov 28 20:39:08 2011 +0100
    48.2 +++ b/src/Pure/Thy/html.ML	Mon Nov 28 22:05:32 2011 +0100
    48.3 @@ -49,8 +49,8 @@
    48.4  fun span class = ("<span class=" ^ quote (XML.text class) ^ ">", "</span>");
    48.5  
    48.6  fun span_class (name, props) =
    48.7 -  (case Markup.get_entity_kind (name, props) of
    48.8 -    SOME kind => Markup.entityN ^ "_" ^ name
    48.9 +  (case Isabelle_Markup.get_entity_kind (name, props) of
   48.10 +    SOME kind => Isabelle_Markup.entityN ^ "_" ^ name
   48.11    | NONE => name);
   48.12  
   48.13  val _ = Markup.add_mode htmlN (span o span_class);
   48.14 @@ -59,7 +59,7 @@
   48.15  (* symbol output *)
   48.16  
   48.17  local
   48.18 -  val hidden = span Markup.hiddenN |-> enclose;
   48.19 +  val hidden = span Isabelle_Markup.hiddenN |-> enclose;
   48.20  
   48.21    (* FIXME proper unicode -- produced on Scala side *)
   48.22    val html_syms = Symtab.make
    49.1 --- a/src/Pure/Thy/html.scala	Mon Nov 28 20:39:08 2011 +0100
    49.2 +++ b/src/Pure/Thy/html.scala	Mon Nov 28 22:05:32 2011 +0100
    49.3 @@ -49,7 +49,7 @@
    49.4      XML.Elem(Markup(SPAN, List((STYLE, "font-family: " + font))), List(XML.Text(txt)))
    49.5  
    49.6    def hidden(txt: String): XML.Elem =
    49.7 -    span(Markup.HIDDEN, List(XML.Text(txt)))
    49.8 +    span(Isabelle_Markup.HIDDEN, List(XML.Text(txt)))
    49.9  
   49.10    def sub(txt: String): XML.Elem = XML.elem("sub", List(XML.Text(txt)))
   49.11    def sup(txt: String): XML.Elem = XML.elem("sup", List(XML.Text(txt)))
   49.12 @@ -61,7 +61,7 @@
   49.13        tree match {
   49.14          case XML.Elem(m @ Markup(name, props), ts) =>
   49.15            val span_class =
   49.16 -            m match { case Markup.Entity(kind, _) => name + "_" + kind case _ => name }
   49.17 +            m match { case Isabelle_Markup.Entity(kind, _) => name + "_" + kind case _ => name }
   49.18            val html_span = span(span_class, ts.flatMap(html_spans))
   49.19            if (original_data) List(XML.Elem(Markup.Data, List(tree, html_span)))
   49.20            else List(html_span)
    50.1 --- a/src/Pure/Thy/latex.ML	Mon Nov 28 20:39:08 2011 +0100
    50.2 +++ b/src/Pure/Thy/latex.ML	Mon Nov 28 22:05:32 2011 +0100
    50.3 @@ -203,8 +203,8 @@
    50.4    in (output_symbols syms, Symbol.length syms) end;
    50.5  
    50.6  fun latex_markup (s, _) =
    50.7 -  if s = Markup.keywordN then ("\\isakeyword{", "}")
    50.8 -  else if s = Markup.commandN then ("\\isacommand{", "}")
    50.9 +  if s = Isabelle_Markup.keywordN then ("\\isakeyword{", "}")
   50.10 +  else if s = Isabelle_Markup.commandN then ("\\isacommand{", "}")
   50.11    else Markup.no_output;
   50.12  
   50.13  fun latex_indent "" _ = ""
    51.1 --- a/src/Pure/Thy/thy_info.ML	Mon Nov 28 20:39:08 2011 +0100
    51.2 +++ b/src/Pure/Thy/thy_info.ML	Mon Nov 28 22:05:32 2011 +0100
    51.3 @@ -89,7 +89,7 @@
    51.4  fun get_names () = Graph.topological_order (get_thys ());
    51.5  
    51.6  fun status () =
    51.7 -  List.app (Output.status o Markup.markup_only o Markup.loaded_theory) (get_names ());
    51.8 +  List.app (Output.status o Markup.markup_only o Isabelle_Markup.loaded_theory) (get_names ());
    51.9  
   51.10  
   51.11  (* access thy *)
    52.1 --- a/src/Pure/Thy/thy_info.scala	Mon Nov 28 20:39:08 2011 +0100
    52.2 +++ b/src/Pure/Thy/thy_info.scala	Mon Nov 28 22:05:32 2011 +0100
    52.3 @@ -14,7 +14,8 @@
    52.4    object Loaded_Theory {
    52.5      def unapply(msg: XML.Tree): Option[String] =
    52.6        msg match {
    52.7 -        case XML.Elem(Markup(Markup.LOADED_THEORY, List((Markup.NAME, name))), _) => Some(name)
    52.8 +        case XML.Elem(Markup(Isabelle_Markup.LOADED_THEORY, List((Markup.NAME, name))), _) =>
    52.9 +          Some(name)
   52.10          case _ => None
   52.11        }
   52.12    }
    53.1 --- a/src/Pure/Thy/thy_output.ML	Mon Nov 28 20:39:08 2011 +0100
    53.2 +++ b/src/Pure/Thy/thy_output.ML	Mon Nov 28 22:05:32 2011 +0100
    53.3 @@ -81,8 +81,8 @@
    53.4      (Args.src -> Toplevel.state -> Proof.context -> string) Name_Space.table *
    53.5        (string -> Proof.context -> Proof.context) Name_Space.table;
    53.6    val empty : T =
    53.7 -    (Name_Space.empty_table Markup.doc_antiquotationN,
    53.8 -      Name_Space.empty_table Markup.doc_antiquotation_optionN);
    53.9 +    (Name_Space.empty_table Isabelle_Markup.doc_antiquotationN,
   53.10 +      Name_Space.empty_table Isabelle_Markup.doc_antiquotation_optionN);
   53.11    val extend = I;
   53.12    fun merge ((commands1, options1), (commands2, options2)) : T =
   53.13      (Name_Space.merge_tables (commands1, commands2),
    54.1 --- a/src/Pure/Thy/thy_syntax.ML	Mon Nov 28 20:39:08 2011 +0100
    54.2 +++ b/src/Pure/Thy/thy_syntax.ML	Mon Nov 28 22:05:32 2011 +0100
    54.3 @@ -43,28 +43,28 @@
    54.4  local
    54.5  
    54.6  val token_kind_markup =
    54.7 - fn Token.Command       => Markup.command
    54.8 -  | Token.Keyword       => Markup.keyword
    54.9 + fn Token.Command       => Isabelle_Markup.command
   54.10 +  | Token.Keyword       => Isabelle_Markup.keyword
   54.11    | Token.Ident         => Markup.empty
   54.12    | Token.LongIdent     => Markup.empty
   54.13    | Token.SymIdent      => Markup.empty
   54.14 -  | Token.Var           => Markup.var
   54.15 -  | Token.TypeIdent     => Markup.tfree
   54.16 -  | Token.TypeVar       => Markup.tvar
   54.17 +  | Token.Var           => Isabelle_Markup.var
   54.18 +  | Token.TypeIdent     => Isabelle_Markup.tfree
   54.19 +  | Token.TypeVar       => Isabelle_Markup.tvar
   54.20    | Token.Nat           => Markup.empty
   54.21    | Token.Float         => Markup.empty
   54.22 -  | Token.String        => Markup.string
   54.23 -  | Token.AltString     => Markup.altstring
   54.24 -  | Token.Verbatim      => Markup.verbatim
   54.25 +  | Token.String        => Isabelle_Markup.string
   54.26 +  | Token.AltString     => Isabelle_Markup.altstring
   54.27 +  | Token.Verbatim      => Isabelle_Markup.verbatim
   54.28    | Token.Space         => Markup.empty
   54.29 -  | Token.Comment       => Markup.comment
   54.30 +  | Token.Comment       => Isabelle_Markup.comment
   54.31    | Token.InternalValue => Markup.empty
   54.32 -  | Token.Error _       => Markup.malformed
   54.33 -  | Token.Sync          => Markup.control
   54.34 -  | Token.EOF           => Markup.control;
   54.35 +  | Token.Error _       => Isabelle_Markup.malformed
   54.36 +  | Token.Sync          => Isabelle_Markup.control
   54.37 +  | Token.EOF           => Isabelle_Markup.control;
   54.38  
   54.39  fun token_markup tok =
   54.40 -  if Token.keyword_with (not o Lexicon.is_ascii_identifier) tok then Markup.operator
   54.41 +  if Token.keyword_with (not o Lexicon.is_ascii_identifier) tok then Isabelle_Markup.operator
   54.42    else
   54.43      let
   54.44        val kind = Token.kind_of tok;
   54.45 @@ -75,7 +75,7 @@
   54.46      in props (token_kind_markup kind) end;
   54.47  
   54.48  fun reports_of_symbol (sym, pos) =
   54.49 -  if Symbol.is_malformed sym then [(pos, Markup.malformed)] else [];
   54.50 +  if Symbol.is_malformed sym then [(pos, Isabelle_Markup.malformed)] else [];
   54.51  
   54.52  in
   54.53  
   54.54 @@ -133,9 +133,9 @@
   54.55  
   54.56  local
   54.57  
   54.58 -fun kind_markup (Command name) = Markup.command_span name
   54.59 -  | kind_markup Ignored = Markup.ignored_span
   54.60 -  | kind_markup Malformed = Markup.malformed_span;
   54.61 +fun kind_markup (Command name) = Isabelle_Markup.command_span name
   54.62 +  | kind_markup Ignored = Isabelle_Markup.ignored_span
   54.63 +  | kind_markup Malformed = Isabelle_Markup.malformed_span;
   54.64  
   54.65  in
   54.66  
    55.1 --- a/src/Pure/build-jars	Mon Nov 28 20:39:08 2011 +0100
    55.2 +++ b/src/Pure/build-jars	Mon Nov 28 22:05:32 2011 +0100
    55.3 @@ -14,7 +14,7 @@
    55.4    Concurrent/simple_thread.scala
    55.5    Concurrent/volatile.scala
    55.6    General/exn.scala
    55.7 -  General/timing.scala
    55.8 +  General/isabelle_markup.scala
    55.9    General/linear_set.scala
   55.10    General/markup.scala
   55.11    General/path.scala
   55.12 @@ -24,6 +24,7 @@
   55.13    General/scan.scala
   55.14    General/sha1.scala
   55.15    General/symbol.scala
   55.16 +  General/timing.scala
   55.17    Isar/keyword.scala
   55.18    Isar/outer_syntax.scala
   55.19    Isar/parse.scala
    56.1 --- a/src/Pure/consts.ML	Mon Nov 28 20:39:08 2011 +0100
    56.2 +++ b/src/Pure/consts.ML	Mon Nov 28 22:05:32 2011 +0100
    56.3 @@ -311,7 +311,8 @@
    56.4  
    56.5  (* empty and merge *)
    56.6  
    56.7 -val empty = make_consts (Name_Space.empty_table Markup.constantN, Symtab.empty, Symtab.empty);
    56.8 +val empty =
    56.9 +  make_consts (Name_Space.empty_table Isabelle_Markup.constantN, Symtab.empty, Symtab.empty);
   56.10  
   56.11  fun merge
   56.12     (Consts {decls = decls1, constraints = constraints1, rev_abbrevs = rev_abbrevs1},
    57.1 --- a/src/Pure/global_theory.ML	Mon Nov 28 20:39:08 2011 +0100
    57.2 +++ b/src/Pure/global_theory.ML	Mon Nov 28 22:05:32 2011 +0100
    57.3 @@ -108,7 +108,8 @@
    57.4        NONE => error ("Unknown fact " ^ quote name ^ Position.str_of pos)
    57.5      | SOME (static, ths) =>
    57.6          (Context_Position.report ctxt pos (Name_Space.markup (Facts.space_of facts) name);
    57.7 -         if static then () else Context_Position.report ctxt pos (Markup.dynamic_fact name);
    57.8 +         if static then ()
    57.9 +         else Context_Position.report ctxt pos (Isabelle_Markup.dynamic_fact name);
   57.10           Facts.select xthmref (map (Thm.transfer thy) ths)))
   57.11    end;
   57.12  
    58.1 --- a/src/Pure/goal_display.ML	Mon Nov 28 20:39:08 2011 +0100
    58.2 +++ b/src/Pure/goal_display.ML	Mon Nov 28 22:05:32 2011 +0100
    58.3 @@ -114,8 +114,9 @@
    58.4      fun pretty_list _ _ [] = []
    58.5        | pretty_list name prt lst = [Pretty.big_list name (map prt lst)];
    58.6  
    58.7 -    fun pretty_subgoal (n, A) = Pretty.markup Markup.subgoal
    58.8 -      [Pretty.str (" " ^ string_of_int n ^ ". "), prt_term A];
    58.9 +    fun pretty_subgoal (n, A) =
   58.10 +      Pretty.markup Isabelle_Markup.subgoal
   58.11 +        [Pretty.str (" " ^ string_of_int n ^ ". "), prt_term A];
   58.12      fun pretty_subgoals As = map pretty_subgoal (1 upto length As ~~ As);
   58.13  
   58.14      val pretty_ffpairs = pretty_list "flex-flex pairs:" (pretty_flexpair ctxt);
    59.1 --- a/src/Pure/type.ML	Mon Nov 28 20:39:08 2011 +0100
    59.2 +++ b/src/Pure/type.ML	Mon Nov 28 22:05:32 2011 +0100
    59.3 @@ -186,8 +186,8 @@
    59.4    build_tsig (f (classes, default, types));
    59.5  
    59.6  val empty_tsig =
    59.7 -  build_tsig ((Name_Space.empty Markup.classN, Sorts.empty_algebra), [],
    59.8 -    Name_Space.empty_table Markup.typeN);
    59.9 +  build_tsig ((Name_Space.empty Isabelle_Markup.classN, Sorts.empty_algebra), [],
   59.10 +    Name_Space.empty_table Isabelle_Markup.typeN);
   59.11  
   59.12  
   59.13  (* classes and sorts *)
    60.1 --- a/src/Pure/variable.ML	Mon Nov 28 20:39:08 2011 +0100
    60.2 +++ b/src/Pure/variable.ML	Mon Nov 28 22:05:32 2011 +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 Markup.fixedN;
    60.8 +val empty_fixes: fixes = Name_Space.empty_table Isabelle_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/html_panel.scala	Mon Nov 28 20:39:08 2011 +0100
    61.2 +++ b/src/Tools/jEdit/src/html_panel.scala	Mon Nov 28 22:05:32 2011 +0100
    61.3 @@ -164,7 +164,8 @@
    61.4          current_body.flatMap(div =>
    61.5            Pretty.formatted(List(div), current_margin, Pretty.font_metric(current_font_metrics))
    61.6              .map(t =>
    61.7 -              XML.Elem(Markup(HTML.PRE, List((HTML.CLASS, Markup.MESSAGE))), HTML.spans(t, true))))
    61.8 +              XML.Elem(Markup(HTML.PRE, List((HTML.CLASS, Isabelle_Markup.MESSAGE))),
    61.9 +                HTML.spans(t, true))))
   61.10        val doc =
   61.11          builder.parse(
   61.12            new InputSourceImpl(
    62.1 --- a/src/Tools/jEdit/src/isabelle_hyperlinks.scala	Mon Nov 28 20:39:08 2011 +0100
    62.2 +++ b/src/Tools/jEdit/src/isabelle_hyperlinks.scala	Mon Nov 28 22:05:32 2011 +0100
    62.3 @@ -62,10 +62,10 @@
    62.4                  {
    62.5                    // FIXME Isar_Document.Hyperlink extractor
    62.6                    case Text.Info(info_range,
    62.7 -                      XML.Elem(Markup(Markup.ENTITY, props), _))
    62.8 +                      XML.Elem(Markup(Isabelle_Markup.ENTITY, props), _))
    62.9                      if (props.find(
   62.10 -                      { case (Markup.KIND, Markup.ML_OPEN) => true
   62.11 -                        case (Markup.KIND, Markup.ML_STRUCT) => true
   62.12 +                      { case (Markup.KIND, Isabelle_Markup.ML_OPEN) => true
   62.13 +                        case (Markup.KIND, Isabelle_Markup.ML_STRUCT) => true
   62.14                          case _ => false }).isEmpty) =>
   62.15                      val Text.Range(begin, end) = info_range
   62.16                      val line = buffer.getLineOfOffset(begin)
   62.17 @@ -90,7 +90,7 @@
   62.18                        case _ => null
   62.19                      }
   62.20                  },
   62.21 -                Some(Set(Markup.ENTITY))))
   62.22 +                Some(Set(Isabelle_Markup.ENTITY))))
   62.23            markup match {
   62.24              case Text.Info(_, Some(link)) #:: _ => link
   62.25              case _ => null
    63.1 --- a/src/Tools/jEdit/src/isabelle_rendering.scala	Mon Nov 28 20:39:08 2011 +0100
    63.2 +++ b/src/Tools/jEdit/src/isabelle_rendering.scala	Mon Nov 28 22:05:32 2011 +0100
    63.3 @@ -90,82 +90,84 @@
    63.4    val message =
    63.5      Markup_Tree.Select[Color](
    63.6        {
    63.7 -        case Text.Info(_, XML.Elem(Markup(Markup.WRITELN, _), _)) => regular_color
    63.8 -        case Text.Info(_, XML.Elem(Markup(Markup.WARNING, _), _)) => warning_color
    63.9 -        case Text.Info(_, XML.Elem(Markup(Markup.ERROR, _), _)) => error_color
   63.10 +        case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.WRITELN, _), _)) => regular_color
   63.11 +        case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.WARNING, _), _)) => warning_color
   63.12 +        case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.ERROR, _), _)) => error_color
   63.13        },
   63.14 -      Some(Set(Markup.WRITELN, Markup.WARNING, Markup.ERROR)))
   63.15 +      Some(Set(Isabelle_Markup.WRITELN, Isabelle_Markup.WARNING, Isabelle_Markup.ERROR)))
   63.16  
   63.17    val tooltip_message =
   63.18      Markup_Tree.Cumulate[SortedMap[Long, String]](SortedMap.empty,
   63.19        {
   63.20 -        case (msgs, Text.Info(_, msg @ XML.Elem(Markup(markup, Markup.Serial(serial)), _)))
   63.21 -        if markup == Markup.WRITELN || markup == Markup.WARNING || markup == Markup.ERROR =>
   63.22 +        case (msgs, Text.Info(_, msg @ XML.Elem(Markup(markup, Isabelle_Markup.Serial(serial)), _)))
   63.23 +        if markup == Isabelle_Markup.WRITELN ||
   63.24 +            markup == Isabelle_Markup.WARNING ||
   63.25 +            markup == Isabelle_Markup.ERROR =>
   63.26            msgs + (serial ->
   63.27              Pretty.string_of(List(msg), margin = Isabelle.Int_Property("tooltip-margin")))
   63.28        },
   63.29 -      Some(Set(Markup.WRITELN, Markup.WARNING, Markup.ERROR)))
   63.30 +      Some(Set(Isabelle_Markup.WRITELN, Isabelle_Markup.WARNING, Isabelle_Markup.ERROR)))
   63.31  
   63.32    val gutter_message =
   63.33      Markup_Tree.Select[Icon](
   63.34        {
   63.35 -        case Text.Info(_, XML.Elem(Markup(Markup.WARNING, _), body)) =>
   63.36 +        case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.WARNING, _), body)) =>
   63.37            body match {
   63.38 -            case List(XML.Elem(Markup(Markup.LEGACY, _), _)) => legacy_icon
   63.39 +            case List(XML.Elem(Markup(Isabelle_Markup.LEGACY, _), _)) => legacy_icon
   63.40              case _ => warning_icon
   63.41            }
   63.42 -        case Text.Info(_, XML.Elem(Markup(Markup.ERROR, _), _)) => error_icon
   63.43 +        case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.ERROR, _), _)) => error_icon
   63.44        },
   63.45 -      Some(Set(Markup.WARNING, Markup.ERROR)))
   63.46 +      Some(Set(Isabelle_Markup.WARNING, Isabelle_Markup.ERROR)))
   63.47  
   63.48    val background1 =
   63.49      Markup_Tree.Select[Color](
   63.50        {
   63.51 -        case Text.Info(_, XML.Elem(Markup(Markup.BAD, _), _)) => bad_color
   63.52 -        case Text.Info(_, XML.Elem(Markup(Markup.HILITE, _), _)) => hilite_color
   63.53 +        case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.BAD, _), _)) => bad_color
   63.54 +        case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.HILITE, _), _)) => hilite_color
   63.55        },
   63.56 -      Some(Set(Markup.BAD, Markup.HILITE)))
   63.57 +      Some(Set(Isabelle_Markup.BAD, Isabelle_Markup.HILITE)))
   63.58  
   63.59    val background2 =
   63.60      Markup_Tree.Select[Color](
   63.61        {
   63.62 -        case Text.Info(_, XML.Elem(Markup(Markup.TOKEN_RANGE, _), _)) => light_color
   63.63 +        case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.TOKEN_RANGE, _), _)) => light_color
   63.64        },
   63.65 -      Some(Set(Markup.TOKEN_RANGE)))
   63.66 +      Some(Set(Isabelle_Markup.TOKEN_RANGE)))
   63.67  
   63.68    val foreground =
   63.69      Markup_Tree.Select[Color](
   63.70        {
   63.71 -        case Text.Info(_, XML.Elem(Markup(Markup.STRING, _), _)) => quoted_color
   63.72 -        case Text.Info(_, XML.Elem(Markup(Markup.ALTSTRING, _), _)) => quoted_color
   63.73 -        case Text.Info(_, XML.Elem(Markup(Markup.VERBATIM, _), _)) => quoted_color
   63.74 +        case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.STRING, _), _)) => quoted_color
   63.75 +        case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.ALTSTRING, _), _)) => quoted_color
   63.76 +        case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.VERBATIM, _), _)) => quoted_color
   63.77        },
   63.78 -      Some(Set(Markup.STRING, Markup.ALTSTRING, Markup.VERBATIM)))
   63.79 +      Some(Set(Isabelle_Markup.STRING, Isabelle_Markup.ALTSTRING, Isabelle_Markup.VERBATIM)))
   63.80  
   63.81    private val text_colors: Map[String, Color] =
   63.82      Map(
   63.83 -      Markup.STRING -> get_color("black"),
   63.84 -      Markup.ALTSTRING -> get_color("black"),
   63.85 -      Markup.VERBATIM -> get_color("black"),
   63.86 -      Markup.LITERAL -> keyword1_color,
   63.87 -      Markup.DELIMITER -> get_color("black"),
   63.88 -      Markup.TFREE -> get_color("#A020F0"),
   63.89 -      Markup.TVAR -> get_color("#A020F0"),
   63.90 -      Markup.FREE -> get_color("blue"),
   63.91 -      Markup.SKOLEM -> get_color("#D2691E"),
   63.92 -      Markup.BOUND -> get_color("green"),
   63.93 -      Markup.VAR -> get_color("#00009B"),
   63.94 -      Markup.INNER_STRING -> get_color("#D2691E"),
   63.95 -      Markup.INNER_COMMENT -> get_color("#8B0000"),
   63.96 -      Markup.DYNAMIC_FACT -> get_color("#7BA428"),
   63.97 -      Markup.ML_KEYWORD -> keyword1_color,
   63.98 -      Markup.ML_DELIMITER -> get_color("black"),
   63.99 -      Markup.ML_NUMERAL -> get_color("red"),
  63.100 -      Markup.ML_CHAR -> get_color("#D2691E"),
  63.101 -      Markup.ML_STRING -> get_color("#D2691E"),
  63.102 -      Markup.ML_COMMENT -> get_color("#8B0000"),
  63.103 -      Markup.ML_MALFORMED -> get_color("#FF6A6A"),
  63.104 -      Markup.ANTIQ -> get_color("blue"))
  63.105 +      Isabelle_Markup.STRING -> get_color("black"),
  63.106 +      Isabelle_Markup.ALTSTRING -> get_color("black"),
  63.107 +      Isabelle_Markup.VERBATIM -> get_color("black"),
  63.108 +      Isabelle_Markup.LITERAL -> keyword1_color,
  63.109 +      Isabelle_Markup.DELIMITER -> get_color("black"),
  63.110 +      Isabelle_Markup.TFREE -> get_color("#A020F0"),
  63.111 +      Isabelle_Markup.TVAR -> get_color("#A020F0"),
  63.112 +      Isabelle_Markup.FREE -> get_color("blue"),
  63.113 +      Isabelle_Markup.SKOLEM -> get_color("#D2691E"),
  63.114 +      Isabelle_Markup.BOUND -> get_color("green"),
  63.115 +      Isabelle_Markup.VAR -> get_color("#00009B"),
  63.116 +      Isabelle_Markup.INNER_STRING -> get_color("#D2691E"),
  63.117 +      Isabelle_Markup.INNER_COMMENT -> get_color("#8B0000"),
  63.118 +      Isabelle_Markup.DYNAMIC_FACT -> get_color("#7BA428"),
  63.119 +      Isabelle_Markup.ML_KEYWORD -> keyword1_color,
  63.120 +      Isabelle_Markup.ML_DELIMITER -> get_color("black"),
  63.121 +      Isabelle_Markup.ML_NUMERAL -> get_color("red"),
  63.122 +      Isabelle_Markup.ML_CHAR -> get_color("#D2691E"),
  63.123 +      Isabelle_Markup.ML_STRING -> get_color("#D2691E"),
  63.124 +      Isabelle_Markup.ML_COMMENT -> get_color("#8B0000"),
  63.125 +      Isabelle_Markup.ML_MALFORMED -> get_color("#FF6A6A"),
  63.126 +      Isabelle_Markup.ANTIQ -> get_color("blue"))
  63.127  
  63.128    val text_color =
  63.129      Markup_Tree.Select[Color](
  63.130 @@ -177,19 +179,19 @@
  63.131  
  63.132    private val tooltips: Map[String, String] =
  63.133      Map(
  63.134 -      Markup.SORT -> "sort",
  63.135 -      Markup.TYP -> "type",
  63.136 -      Markup.TERM -> "term",
  63.137 -      Markup.PROP -> "proposition",
  63.138 -      Markup.TOKEN_RANGE -> "inner syntax token",
  63.139 -      Markup.FREE -> "free variable",
  63.140 -      Markup.SKOLEM -> "skolem variable",
  63.141 -      Markup.BOUND -> "bound variable",
  63.142 -      Markup.VAR -> "schematic variable",
  63.143 -      Markup.TFREE -> "free type variable",
  63.144 -      Markup.TVAR -> "schematic type variable",
  63.145 -      Markup.ML_SOURCE -> "ML source",
  63.146 -      Markup.DOC_SOURCE -> "document source")
  63.147 +      Isabelle_Markup.SORT -> "sort",
  63.148 +      Isabelle_Markup.TYP -> "type",
  63.149 +      Isabelle_Markup.TERM -> "term",
  63.150 +      Isabelle_Markup.PROP -> "proposition",
  63.151 +      Isabelle_Markup.TOKEN_RANGE -> "inner syntax token",
  63.152 +      Isabelle_Markup.FREE -> "free variable",
  63.153 +      Isabelle_Markup.SKOLEM -> "skolem variable",
  63.154 +      Isabelle_Markup.BOUND -> "bound variable",
  63.155 +      Isabelle_Markup.VAR -> "schematic variable",
  63.156 +      Isabelle_Markup.TFREE -> "free type variable",
  63.157 +      Isabelle_Markup.TVAR -> "schematic type variable",
  63.158 +      Isabelle_Markup.ML_SOURCE -> "ML source",
  63.159 +      Isabelle_Markup.DOC_SOURCE -> "document source")
  63.160  
  63.161    private def string_of_typing(kind: String, body: XML.Body): String =
  63.162      Pretty.string_of(List(Pretty.block(XML.Text(kind) :: Pretty.Break(1) :: body)),
  63.163 @@ -198,25 +200,28 @@
  63.164    val tooltip1 =
  63.165      Markup_Tree.Select[String](
  63.166        {
  63.167 -        case Text.Info(_, XML.Elem(Markup.Entity(kind, name), _)) => kind + " " + quote(name)
  63.168 -        case Text.Info(_, XML.Elem(Markup(Markup.ML_TYPING, _), body)) =>
  63.169 +        case Text.Info(_, XML.Elem(Isabelle_Markup.Entity(kind, name), _)) => kind + " " + quote(name)
  63.170 +        case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.ML_TYPING, _), body)) =>
  63.171            string_of_typing("ML:", body)
  63.172          case Text.Info(_, XML.Elem(Markup(name, _), _))
  63.173          if tooltips.isDefinedAt(name) => tooltips(name)
  63.174        },
  63.175 -      Some(Set(Markup.ENTITY, Markup.ML_TYPING) ++ tooltips.keys))
  63.176 +      Some(Set(Isabelle_Markup.ENTITY, Isabelle_Markup.ML_TYPING) ++ tooltips.keys))
  63.177  
  63.178    val tooltip2 =
  63.179      Markup_Tree.Select[String](
  63.180        {
  63.181 -        case Text.Info(_, XML.Elem(Markup(Markup.TYPING, _), body)) => string_of_typing("::", body)
  63.182 +        case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.TYPING, _), body)) =>
  63.183 +          string_of_typing("::", body)
  63.184        },
  63.185 -      Some(Set(Markup.TYPING)))
  63.186 +      Some(Set(Isabelle_Markup.TYPING)))
  63.187  
  63.188    private val subexp_include =
  63.189 -    Set(Markup.SORT, Markup.TYP, Markup.TERM, Markup.PROP, Markup.ML_TYPING, Markup.TOKEN_RANGE,
  63.190 -      Markup.ENTITY, Markup.TYPING, Markup.FREE, Markup.SKOLEM, Markup.BOUND, Markup.VAR,
  63.191 -      Markup.TFREE, Markup.TVAR, Markup.ML_SOURCE, Markup.DOC_SOURCE)
  63.192 +    Set(Isabelle_Markup.SORT, Isabelle_Markup.TYP, Isabelle_Markup.TERM, Isabelle_Markup.PROP,
  63.193 +      Isabelle_Markup.ML_TYPING, Isabelle_Markup.TOKEN_RANGE, Isabelle_Markup.ENTITY,
  63.194 +      Isabelle_Markup.TYPING, Isabelle_Markup.FREE, Isabelle_Markup.SKOLEM, Isabelle_Markup.BOUND,
  63.195 +      Isabelle_Markup.VAR, Isabelle_Markup.TFREE, Isabelle_Markup.TVAR, Isabelle_Markup.ML_SOURCE,
  63.196 +      Isabelle_Markup.DOC_SOURCE)
  63.197  
  63.198    val subexp =
  63.199      Markup_Tree.Select[(Text.Range, Color)](
    64.1 --- a/src/Tools/jEdit/src/output_dockable.scala	Mon Nov 28 20:39:08 2011 +0100
    64.2 +++ b/src/Tools/jEdit/src/output_dockable.scala	Mon Nov 28 22:05:32 2011 +0100
    64.3 @@ -87,7 +87,7 @@
    64.4                val snapshot = doc_view.update_snapshot()
    64.5                val filtered_results =
    64.6                  snapshot.command_state(cmd).results.iterator.map(_._2) filter {
    64.7 -                  case XML.Elem(Markup(Markup.TRACING, _), _) => show_tracing  // FIXME not scalable
    64.8 +                  case XML.Elem(Markup(Isabelle_Markup.TRACING, _), _) => show_tracing  // FIXME not scalable
    64.9                    case _ => true
   64.10                  }
   64.11                html_panel.render(filtered_results.toList)
    65.1 --- a/src/Tools/quickcheck.ML	Mon Nov 28 20:39:08 2011 +0100
    65.2 +++ b/src/Tools/quickcheck.ML	Mon Nov 28 22:05:32 2011 +0100
    65.3 @@ -502,7 +502,7 @@
    65.4               state
    65.5               |> (if auto then
    65.6                     Proof.goal_message (K (Pretty.chunks [Pretty.str "",
    65.7 -                       Pretty.mark Markup.hilite msg]))
    65.8 +                       Pretty.mark Isabelle_Markup.hilite msg]))
    65.9                   else
   65.10                     tap (fn _ => Output.urgent_message (Pretty.string_of msg))))
   65.11            else
    66.1 --- a/src/Tools/solve_direct.ML	Mon Nov 28 20:39:08 2011 +0100
    66.2 +++ b/src/Tools/solve_direct.ML	Mon Nov 28 22:05:32 2011 +0100
    66.3 @@ -89,7 +89,7 @@
    66.4                 Proof.goal_message
    66.5                   (fn () =>
    66.6                     Pretty.chunks
    66.7 -                    [Pretty.str "", Pretty.markup Markup.hilite (message results)])
    66.8 +                    [Pretty.str "", Pretty.markup Isabelle_Markup.hilite (message results)])
    66.9               else
   66.10                 tap (fn _ =>
   66.11                   Output.urgent_message (Pretty.string_of (Pretty.chunks (message results))))))