--- a/src/HOL/Library/Sum_of_Squares/sos_wrapper.ML Mon Nov 28 20:39:08 2011 +0100
+++ b/src/HOL/Library/Sum_of_Squares/sos_wrapper.ML Mon Nov 28 22:05:32 2011 +0100
@@ -130,7 +130,7 @@
fun output_line cert =
"To repeat this proof with a certifiate use this command:\n" ^
- Markup.markup Markup.sendback ("by (sos_cert \"" ^ cert ^ "\")")
+ Markup.markup Isabelle_Markup.sendback ("by (sos_cert \"" ^ cert ^ "\")")
val print_cert = warning o output_line o PositivstellensatzTools.pss_tree_to_cert
--- a/src/HOL/Statespace/StateSpaceEx.thy Mon Nov 28 20:39:08 2011 +0100
+++ b/src/HOL/Statespace/StateSpaceEx.thy Mon Nov 28 22:05:32 2011 +0100
@@ -235,7 +235,7 @@
ML {*
fun make_benchmark n =
- writeln (Markup.markup Markup.sendback
+ writeln (Markup.markup Isabelle_Markup.sendback
("statespace benchmark" ^ string_of_int n ^ " =\n" ^
(cat_lines (map (fn i => "A" ^ string_of_int i ^ "::nat") (1 upto n)))));
*}
--- a/src/HOL/Tools/ATP/atp_reconstruct.ML Mon Nov 28 20:39:08 2011 +0100
+++ b/src/HOL/Tools/ATP/atp_reconstruct.ML Mon Nov 28 22:05:32 2011 +0100
@@ -233,7 +233,7 @@
name |> not (Lexicon.is_identifier name) ? enclose "(" ")"
| command_call name args = "(" ^ name ^ " " ^ space_implode " " args ^ ")"
fun try_command_line banner time command =
- banner ^ ": " ^ Markup.markup Markup.sendback command ^ show_time time ^ "."
+ banner ^ ": " ^ Markup.markup Isabelle_Markup.sendback command ^ show_time time ^ "."
fun using_labels [] = ""
| using_labels ls =
"using " ^ space_implode " " (map string_for_label ls) ^ " "
@@ -244,7 +244,7 @@
| minimize_line minimize_command ss =
case minimize_command ss of
"" => ""
- | command => "\nTo minimize: " ^ Markup.markup Markup.sendback command ^ "."
+ | command => "\nTo minimize: " ^ Markup.markup Isabelle_Markup.sendback command ^ "."
val split_used_facts =
List.partition (curry (op =) Chained o snd)
@@ -1048,7 +1048,7 @@
| proof =>
"\n\n" ^ (if isar_proof_requested then "Structured proof"
else "Perhaps this will work") ^
- ":\n" ^ Markup.markup Markup.sendback proof
+ ":\n" ^ Markup.markup Isabelle_Markup.sendback proof
val isar_proof =
if debug then
isar_proof_for ()
--- a/src/HOL/Tools/Nitpick/nitpick.ML Mon Nov 28 20:39:08 2011 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick.ML Mon Nov 28 22:05:32 2011 +0100
@@ -239,7 +239,7 @@
if mode = Auto_Try then
Unsynchronized.change state_ref o Proof.goal_message o K
o Pretty.chunks o cons (Pretty.str "") o single
- o Pretty.mark Markup.hilite
+ o Pretty.mark Isabelle_Markup.hilite
else
(fn s => (Output.urgent_message s; if debug then tracing s else ()))
o Pretty.string_of
@@ -459,7 +459,7 @@
pprint_n (fn () => Pretty.blk (0,
pstrs "Hint: To check that the induction hypothesis is \
\general enough, try this command: " @
- [Pretty.mark Markup.sendback (Pretty.blk (0,
+ [Pretty.mark Isabelle_Markup.sendback (Pretty.blk (0,
pstrs ("nitpick [non_std, show_all]")))] @ pstrs "."))
else
()
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Mon Nov 28 20:39:08 2011 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Mon Nov 28 22:05:32 2011 +0100
@@ -238,7 +238,7 @@
|> outcome_code = someN
? Proof.goal_message (fn () =>
[Pretty.str "",
- Pretty.mark Markup.hilite (Pretty.str (message ()))]
+ Pretty.mark Isabelle_Markup.hilite (Pretty.str (message ()))]
|> Pretty.chunks))
end
else if blocking then
--- a/src/HOL/Tools/try_methods.ML Mon Nov 28 20:39:08 2011 +0100
+++ b/src/HOL/Tools/try_methods.ML Mon Nov 28 22:05:32 2011 +0100
@@ -138,7 +138,7 @@
Auto_Try => "Auto Try Methods found a proof"
| Try => "Try Methods found a proof"
| Normal => "Try this") ^ ": " ^
- Markup.markup Markup.sendback
+ Markup.markup Isabelle_Markup.sendback
((if nprems_of (#goal (Proof.goal st)) = 1 then "by"
else "apply") ^ " " ^ (s |> need_parens ? enclose "(" ")")) ^
"\n(" ^ space_implode "; " (map time_string xs) ^ ").\n"
@@ -146,7 +146,7 @@
(true, (s, st |> (if mode = Auto_Try then
Proof.goal_message
(fn () => Pretty.chunks [Pretty.str "",
- Pretty.markup Markup.hilite
+ Pretty.markup Isabelle_Markup.hilite
[Pretty.str message]])
else
tap (fn _ => Output.urgent_message message))))
--- a/src/Pure/Concurrent/future.ML Mon Nov 28 20:39:08 2011 +0100
+++ b/src/Pure/Concurrent/future.ML Mon Nov 28 22:05:32 2011 +0100
@@ -643,10 +643,10 @@
val task_props =
(case worker_task () of
NONE => I
- | SOME task => Markup.properties [(Markup.taskN, Task_Queue.str_of_task task)]);
- val _ = Output.status (Markup.markup_only (task_props Markup.forked));
+ | SOME task => Markup.properties [(Isabelle_Markup.taskN, Task_Queue.str_of_task task)]);
+ val _ = Output.status (Markup.markup_only (task_props Isabelle_Markup.forked));
val x = e (); (*sic -- report "joined" only for success*)
- val _ = Output.status (Markup.markup_only (task_props Markup.joined));
+ val _ = Output.status (Markup.markup_only (task_props Isabelle_Markup.joined));
in x end;
--- a/src/Pure/General/antiquote.ML Mon Nov 28 20:39:08 2011 +0100
+++ b/src/Pure/General/antiquote.ML Mon Nov 28 22:05:32 2011 +0100
@@ -40,9 +40,9 @@
fun reports_of text =
maps
(fn Text x => text x
- | Antiq (_, (pos, _)) => [(pos, Markup.antiq)]
- | Open pos => [(pos, Markup.antiq)]
- | Close pos => [(pos, Markup.antiq)]);
+ | Antiq (_, (pos, _)) => [(pos, Isabelle_Markup.antiq)]
+ | Open pos => [(pos, Isabelle_Markup.antiq)]
+ | Close pos => [(pos, Isabelle_Markup.antiq)]);
(* check_nesting *)
--- a/src/Pure/General/binding.ML Mon Nov 28 20:39:08 2011 +0100
+++ b/src/Pure/General/binding.ML Mon Nov 28 22:05:32 2011 +0100
@@ -122,7 +122,7 @@
(* print *)
fun pretty (Binding {prefix, qualifier, name, pos, ...}) =
- Pretty.markup (Position.markup pos Markup.binding)
+ Pretty.markup (Position.markup pos Isabelle_Markup.binding)
[Pretty.str (Long_Name.implode (map #1 (prefix @ qualifier) @ [name]))]
|> Pretty.quote;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/isabelle_markup.ML Mon Nov 28 22:05:32 2011 +0100
@@ -0,0 +1,310 @@
+(* Title: Pure/General/isabelle_markup.ML
+ Author: Makarius
+
+Isabelle markup elements.
+*)
+
+signature ISABELLE_MARKUP =
+sig
+ val bindingN: string val binding: Markup.T
+ val entityN: string val entity: string -> string -> Markup.T
+ val get_entity_kind: Markup.T -> string option
+ val defN: string
+ val refN: string
+ val lineN: string
+ val offsetN: string
+ val end_offsetN: string
+ val fileN: string
+ val idN: string
+ val position_properties': string list
+ val position_properties: string list
+ val positionN: string val position: Markup.T
+ val pathN: string val path: string -> Markup.T
+ val indentN: string
+ val blockN: string val block: int -> Markup.T
+ val widthN: string
+ val breakN: string val break: int -> Markup.T
+ val fbreakN: string val fbreak: Markup.T
+ val hiddenN: string val hidden: Markup.T
+ val classN: string
+ val typeN: string
+ val constantN: string
+ val fixedN: string val fixed: string -> Markup.T
+ val dynamic_factN: string val dynamic_fact: string -> Markup.T
+ val tfreeN: string val tfree: Markup.T
+ val tvarN: string val tvar: Markup.T
+ val freeN: string val free: Markup.T
+ val skolemN: string val skolem: Markup.T
+ val boundN: string val bound: Markup.T
+ val varN: string val var: Markup.T
+ val numeralN: string val numeral: Markup.T
+ val literalN: string val literal: Markup.T
+ val delimiterN: string val delimiter: Markup.T
+ val inner_stringN: string val inner_string: Markup.T
+ val inner_commentN: string val inner_comment: Markup.T
+ val token_rangeN: string val token_range: Markup.T
+ val sortN: string val sort: Markup.T
+ val typN: string val typ: Markup.T
+ val termN: string val term: Markup.T
+ val propN: string val prop: Markup.T
+ val typingN: string val typing: Markup.T
+ val ML_keywordN: string val ML_keyword: Markup.T
+ val ML_delimiterN: string val ML_delimiter: Markup.T
+ val ML_tvarN: string val ML_tvar: Markup.T
+ val ML_numeralN: string val ML_numeral: Markup.T
+ val ML_charN: string val ML_char: Markup.T
+ val ML_stringN: string val ML_string: Markup.T
+ val ML_commentN: string val ML_comment: Markup.T
+ val ML_malformedN: string val ML_malformed: Markup.T
+ val ML_defN: string
+ val ML_openN: string
+ val ML_structN: string
+ val ML_typingN: string val ML_typing: Markup.T
+ val ML_sourceN: string val ML_source: Markup.T
+ val doc_sourceN: string val doc_source: Markup.T
+ val antiqN: string val antiq: Markup.T
+ val ML_antiquotationN: string
+ val doc_antiquotationN: string
+ val doc_antiquotation_optionN: string
+ val keyword_declN: string val keyword_decl: string -> Markup.T
+ val command_declN: string val command_decl: string -> string -> Markup.T
+ val keywordN: string val keyword: Markup.T
+ val operatorN: string val operator: Markup.T
+ val commandN: string val command: Markup.T
+ val stringN: string val string: Markup.T
+ val altstringN: string val altstring: Markup.T
+ val verbatimN: string val verbatim: Markup.T
+ val commentN: string val comment: Markup.T
+ val controlN: string val control: Markup.T
+ val malformedN: string val malformed: Markup.T
+ val tokenN: string val token: Properties.T -> Markup.T
+ val command_spanN: string val command_span: string -> Markup.T
+ val ignored_spanN: string val ignored_span: Markup.T
+ val malformed_spanN: string val malformed_span: Markup.T
+ val loaded_theoryN: string val loaded_theory: string -> Markup.T
+ val subgoalsN: string
+ val proof_stateN: string val proof_state: int -> Markup.T
+ val stateN: string val state: Markup.T
+ val subgoalN: string val subgoal: Markup.T
+ val sendbackN: string val sendback: Markup.T
+ val hiliteN: string val hilite: Markup.T
+ val taskN: string
+ val forkedN: string val forked: Markup.T
+ val joinedN: string val joined: Markup.T
+ val failedN: string val failed: Markup.T
+ val finishedN: string val finished: Markup.T
+ val serialN: string
+ val legacyN: string val legacy: Markup.T
+ val promptN: string val prompt: Markup.T
+ val readyN: string val ready: Markup.T
+ val reportN: string val report: Markup.T
+ val no_reportN: string val no_report: Markup.T
+ val badN: string val bad: Markup.T
+ val functionN: string
+ val assign_execs: Properties.T
+ val removed_versions: Properties.T
+ val invoke_scala: string -> string -> Properties.T
+ val cancel_scala: string -> Properties.T
+end;
+
+structure Isabelle_Markup: ISABELLE_MARKUP =
+struct
+
+(** markup elements **)
+
+fun markup_elem elem = (elem, (elem, []): Markup.T);
+fun markup_string elem prop = (elem, fn s => (elem, [(prop, s)]): Markup.T);
+fun markup_int elem prop = (elem, fn i => (elem, [(prop, Markup.print_int i)]): Markup.T);
+
+
+(* formal entities *)
+
+val (bindingN, binding) = markup_elem "binding";
+
+val entityN = "entity";
+fun entity kind name = (entityN, [(Markup.nameN, name), (Markup.kindN, kind)]);
+
+fun get_entity_kind (name, props) =
+ if name = entityN then AList.lookup (op =) props Markup.kindN
+ else NONE;
+
+val defN = "def";
+val refN = "ref";
+
+
+(* position *)
+
+val lineN = "line";
+val offsetN = "offset";
+val end_offsetN = "end_offset";
+val fileN = "file";
+val idN = "id";
+
+val position_properties' = [fileN, idN];
+val position_properties = [lineN, offsetN, end_offsetN] @ position_properties';
+
+val (positionN, position) = markup_elem "position";
+
+
+(* path *)
+
+val (pathN, path) = markup_string "path" Markup.nameN;
+
+
+(* pretty printing *)
+
+val indentN = "indent";
+val (blockN, block) = markup_int "block" indentN;
+
+val widthN = "width";
+val (breakN, break) = markup_int "break" widthN;
+
+val (fbreakN, fbreak) = markup_elem "fbreak";
+
+
+(* hidden text *)
+
+val (hiddenN, hidden) = markup_elem "hidden";
+
+
+(* logical entities *)
+
+val classN = "class";
+val typeN = "type";
+val constantN = "constant";
+
+val (fixedN, fixed) = markup_string "fixed" Markup.nameN;
+val (dynamic_factN, dynamic_fact) = markup_string "dynamic_fact" Markup.nameN;
+
+
+(* inner syntax *)
+
+val (tfreeN, tfree) = markup_elem "tfree";
+val (tvarN, tvar) = markup_elem "tvar";
+val (freeN, free) = markup_elem "free";
+val (skolemN, skolem) = markup_elem "skolem";
+val (boundN, bound) = markup_elem "bound";
+val (varN, var) = markup_elem "var";
+val (numeralN, numeral) = markup_elem "numeral";
+val (literalN, literal) = markup_elem "literal";
+val (delimiterN, delimiter) = markup_elem "delimiter";
+val (inner_stringN, inner_string) = markup_elem "inner_string";
+val (inner_commentN, inner_comment) = markup_elem "inner_comment";
+
+val (token_rangeN, token_range) = markup_elem "token_range";
+
+val (sortN, sort) = markup_elem "sort";
+val (typN, typ) = markup_elem "typ";
+val (termN, term) = markup_elem "term";
+val (propN, prop) = markup_elem "prop";
+
+val (typingN, typing) = markup_elem "typing";
+
+
+(* ML syntax *)
+
+val (ML_keywordN, ML_keyword) = markup_elem "ML_keyword";
+val (ML_delimiterN, ML_delimiter) = markup_elem "ML_delimiter";
+val (ML_tvarN, ML_tvar) = markup_elem "ML_tvar";
+val (ML_numeralN, ML_numeral) = markup_elem "ML_numeral";
+val (ML_charN, ML_char) = markup_elem "ML_char";
+val (ML_stringN, ML_string) = markup_elem "ML_string";
+val (ML_commentN, ML_comment) = markup_elem "ML_comment";
+val (ML_malformedN, ML_malformed) = markup_elem "ML_malformed";
+
+val ML_defN = "ML_def";
+val ML_openN = "ML_open";
+val ML_structN = "ML_struct";
+val (ML_typingN, ML_typing) = markup_elem "ML_typing";
+
+
+(* embedded source text *)
+
+val (ML_sourceN, ML_source) = markup_elem "ML_source";
+val (doc_sourceN, doc_source) = markup_elem "doc_source";
+
+val (antiqN, antiq) = markup_elem "antiq";
+val ML_antiquotationN = "ML antiquotation";
+val doc_antiquotationN = "document antiquotation";
+val doc_antiquotation_optionN = "document antiquotation option";
+
+
+(* outer syntax *)
+
+val (keyword_declN, keyword_decl) = markup_string "keyword_decl" Markup.nameN;
+
+val command_declN = "command_decl";
+
+fun command_decl name kind : Markup.T =
+ (command_declN, [(Markup.nameN, name), (Markup.kindN, kind)]);
+
+val (keywordN, keyword) = markup_elem "keyword";
+val (operatorN, operator) = markup_elem "operator";
+val (commandN, command) = markup_elem "command";
+val (stringN, string) = markup_elem "string";
+val (altstringN, altstring) = markup_elem "altstring";
+val (verbatimN, verbatim) = markup_elem "verbatim";
+val (commentN, comment) = markup_elem "comment";
+val (controlN, control) = markup_elem "control";
+val (malformedN, malformed) = markup_elem "malformed";
+
+val tokenN = "token";
+fun token props = (tokenN, props);
+
+val (command_spanN, command_span) = markup_string "command_span" Markup.nameN;
+val (ignored_spanN, ignored_span) = markup_elem "ignored_span";
+val (malformed_spanN, malformed_span) = markup_elem "malformed_span";
+
+
+(* theory loader *)
+
+val (loaded_theoryN, loaded_theory) = markup_string "loaded_theory" Markup.nameN;
+
+
+(* toplevel *)
+
+val subgoalsN = "subgoals";
+val (proof_stateN, proof_state) = markup_int "proof_state" subgoalsN;
+
+val (stateN, state) = markup_elem "state";
+val (subgoalN, subgoal) = markup_elem "subgoal";
+val (sendbackN, sendback) = markup_elem "sendback";
+val (hiliteN, hilite) = markup_elem "hilite";
+
+
+(* command status *)
+
+val taskN = "task";
+
+val (forkedN, forked) = markup_elem "forked";
+val (joinedN, joined) = markup_elem "joined";
+
+val (failedN, failed) = markup_elem "failed";
+val (finishedN, finished) = markup_elem "finished";
+
+
+(* messages *)
+
+val serialN = "serial";
+
+val (legacyN, legacy) = markup_elem "legacy";
+val (promptN, prompt) = markup_elem "prompt";
+val (readyN, ready) = markup_elem "ready";
+
+val (reportN, report) = markup_elem "report";
+val (no_reportN, no_report) = markup_elem "no_report";
+
+val (badN, bad) = markup_elem "bad";
+
+
+(* raw message functions *)
+
+val functionN = "function"
+
+val assign_execs = [(functionN, "assign_execs")];
+val removed_versions = [(functionN, "removed_versions")];
+
+fun invoke_scala name id = [(functionN, "invoke_scala"), (Markup.nameN, name), (idN, id)];
+fun cancel_scala id = [(functionN, "cancel_scala"), (idN, id)];
+
+end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/isabelle_markup.scala Mon Nov 28 22:05:32 2011 +0100
@@ -0,0 +1,260 @@
+/* Title: Pure/General/isabelle_markup.scala
+ Author: Makarius
+
+Isabelle markup elements.
+*/
+
+package isabelle
+
+
+object Isabelle_Markup
+{
+ /* formal entities */
+
+ val BINDING = "binding"
+ val ENTITY = "entity"
+ val DEF = "def"
+ val REF = "ref"
+
+ object Entity
+ {
+ def unapply(markup: Markup): Option[(String, String)] =
+ markup match {
+ case Markup(ENTITY, props @ Markup.Kind(kind)) =>
+ props match {
+ case Markup.Name(name) => Some(kind, name)
+ case _ => None
+ }
+ case _ => None
+ }
+ }
+
+
+ /* position */
+
+ val LINE = "line"
+ val OFFSET = "offset"
+ val END_OFFSET = "end_offset"
+ val FILE = "file"
+ val ID = "id"
+
+ val DEF_LINE = "def_line"
+ val DEF_OFFSET = "def_offset"
+ val DEF_END_OFFSET = "def_end_offset"
+ val DEF_FILE = "def_file"
+ val DEF_ID = "def_id"
+
+ val POSITION_PROPERTIES = Set(LINE, OFFSET, END_OFFSET, FILE, ID)
+ val POSITION = "position"
+
+
+ /* path */
+
+ val PATH = "path"
+
+ object Path
+ {
+ def unapply(markup: Markup): Option[String] =
+ markup match {
+ case Markup(PATH, Markup.Name(name)) => Some(name)
+ case _ => None
+ }
+ }
+
+
+ /* pretty printing */
+
+ val Indent = new Properties.Int("indent")
+ val BLOCK = "block"
+ val Width = new Properties.Int("width")
+ val BREAK = "break"
+
+
+ /* hidden text */
+
+ val HIDDEN = "hidden"
+
+
+ /* logical entities */
+
+ val CLASS = "class"
+ val TYPE = "type"
+ val FIXED = "fixed"
+ val CONSTANT = "constant"
+
+ val DYNAMIC_FACT = "dynamic_fact"
+
+
+ /* inner syntax */
+
+ val TFREE = "tfree"
+ val TVAR = "tvar"
+ val FREE = "free"
+ val SKOLEM = "skolem"
+ val BOUND = "bound"
+ val VAR = "var"
+ val NUM = "num"
+ val FLOAT = "float"
+ val XNUM = "xnum"
+ val XSTR = "xstr"
+ val LITERAL = "literal"
+ val DELIMITER = "delimiter"
+ val INNER_STRING = "inner_string"
+ val INNER_COMMENT = "inner_comment"
+
+ val TOKEN_RANGE = "token_range"
+
+ val SORT = "sort"
+ val TYP = "typ"
+ val TERM = "term"
+ val PROP = "prop"
+
+ val TYPING = "typing"
+
+ val ATTRIBUTE = "attribute"
+ val METHOD = "method"
+
+
+ /* embedded source text */
+
+ val ML_SOURCE = "ML_source"
+ val DOC_SOURCE = "doc_source"
+
+ val ANTIQ = "antiq"
+ val ML_ANTIQUOTATION = "ML antiquotation"
+ val DOCUMENT_ANTIQUOTATION = "document antiquotation"
+ val DOCUMENT_ANTIQUOTATION_OPTION = "document antiquotation option"
+
+
+ /* ML syntax */
+
+ val ML_KEYWORD = "ML_keyword"
+ val ML_DELIMITER = "ML_delimiter"
+ val ML_TVAR = "ML_tvar"
+ val ML_NUMERAL = "ML_numeral"
+ val ML_CHAR = "ML_char"
+ val ML_STRING = "ML_string"
+ val ML_COMMENT = "ML_comment"
+ val ML_MALFORMED = "ML_malformed"
+
+ val ML_DEF = "ML_def"
+ val ML_OPEN = "ML_open"
+ val ML_STRUCT = "ML_struct"
+ val ML_TYPING = "ML_typing"
+
+
+ /* outer syntax */
+
+ val KEYWORD_DECL = "keyword_decl"
+ val COMMAND_DECL = "command_decl"
+
+ val KEYWORD = "keyword"
+ val OPERATOR = "operator"
+ val COMMAND = "command"
+ val STRING = "string"
+ val ALTSTRING = "altstring"
+ val VERBATIM = "verbatim"
+ val COMMENT = "comment"
+ val CONTROL = "control"
+ val MALFORMED = "malformed"
+
+ val COMMAND_SPAN = "command_span"
+ val IGNORED_SPAN = "ignored_span"
+ val MALFORMED_SPAN = "malformed_span"
+
+
+ /* theory loader */
+
+ val LOADED_THEORY = "loaded_theory"
+
+
+ /* toplevel */
+
+ val SUBGOALS = "subgoals"
+ val PROOF_STATE = "proof_state"
+
+ val STATE = "state"
+ val SUBGOAL = "subgoal"
+ val SENDBACK = "sendback"
+ val HILITE = "hilite"
+
+
+ /* command status */
+
+ val TASK = "task"
+
+ val FORKED = "forked"
+ val JOINED = "joined"
+ val FAILED = "failed"
+ val FINISHED = "finished"
+
+
+ /* interactive documents */
+
+ val VERSION = "version"
+ val ASSIGN = "assign"
+
+
+ /* prover process */
+
+ val PROVER_COMMAND = "prover_command"
+ val PROVER_ARG = "prover_arg"
+
+
+ /* messages */
+
+ val Serial = new Properties.Long("serial")
+
+ val MESSAGE = "message"
+
+ val INIT = "init"
+ val STATUS = "status"
+ val REPORT = "report"
+ val WRITELN = "writeln"
+ val TRACING = "tracing"
+ val WARNING = "warning"
+ val ERROR = "error"
+ val RAW = "raw"
+ val SYSTEM = "system"
+ val STDOUT = "stdout"
+ val STDERR = "stderr"
+ val EXIT = "exit"
+
+ val LEGACY = "legacy"
+
+ val NO_REPORT = "no_report"
+
+ val BAD = "bad"
+
+ val READY = "ready"
+
+
+ /* raw message functions */
+
+ val FUNCTION = "function"
+ val Function = new Properties.String(FUNCTION)
+
+ val Assign_Execs: Properties.T = List((FUNCTION, "assign_execs"))
+ val Removed_Versions: Properties.T = List((FUNCTION, "removed_versions"))
+
+ val INVOKE_SCALA = "invoke_scala"
+ object Invoke_Scala
+ {
+ def unapply(props: Properties.T): Option[(String, String)] =
+ props match {
+ case List((FUNCTION, INVOKE_SCALA), (Markup.NAME, name), (ID, id)) => Some((name, id))
+ case _ => None
+ }
+ }
+
+ val CANCEL_SCALA = "cancel_scala"
+ object Cancel_Scala
+ {
+ def unapply(props: Properties.T): Option[String] =
+ props match {
+ case List((FUNCTION, CANCEL_SCALA), (ID, id)) => Some(id)
+ case _ => None
+ }
+ }
+}
+
--- a/src/Pure/General/markup.ML Mon Nov 28 20:39:08 2011 +0100
+++ b/src/Pure/General/markup.ML Mon Nov 28 22:05:32 2011 +0100
@@ -1,7 +1,7 @@
(* Title: Pure/General/markup.ML
Author: Makarius
-Common markup elements.
+Generic markup elements.
*)
signature MARKUP =
@@ -15,109 +15,10 @@
val nameN: string
val name: string -> T -> T
val kindN: string
- val bindingN: string val binding: T
- val entityN: string val entity: string -> string -> T
- val get_entity_kind: T -> string option
- val defN: string
- val refN: string
- val lineN: string
- val offsetN: string
- val end_offsetN: string
- val fileN: string
- val idN: string
- val position_properties': string list
- val position_properties: string list
- val positionN: string val position: T
- val pathN: string val path: string -> T
- val indentN: string
- val blockN: string val block: int -> T
- val widthN: string
- val breakN: string val break: int -> T
- val fbreakN: string val fbreak: T
- val hiddenN: string val hidden: T
- val classN: string
- val typeN: string
- val constantN: string
- val fixedN: string val fixed: string -> T
- val dynamic_factN: string val dynamic_fact: string -> T
- val tfreeN: string val tfree: T
- val tvarN: string val tvar: T
- val freeN: string val free: T
- val skolemN: string val skolem: T
- val boundN: string val bound: T
- val varN: string val var: T
- val numeralN: string val numeral: T
- val literalN: string val literal: T
- val delimiterN: string val delimiter: T
- val inner_stringN: string val inner_string: T
- val inner_commentN: string val inner_comment: T
- val token_rangeN: string val token_range: T
- val sortN: string val sort: T
- val typN: string val typ: T
- val termN: string val term: T
- val propN: string val prop: T
- val typingN: string val typing: T
- val ML_keywordN: string val ML_keyword: T
- val ML_delimiterN: string val ML_delimiter: T
- val ML_tvarN: string val ML_tvar: T
- val ML_numeralN: string val ML_numeral: T
- val ML_charN: string val ML_char: T
- val ML_stringN: string val ML_string: T
- val ML_commentN: string val ML_comment: T
- val ML_malformedN: string val ML_malformed: T
- val ML_defN: string
- val ML_openN: string
- val ML_structN: string
- val ML_typingN: string val ML_typing: T
- val ML_sourceN: string val ML_source: T
- val doc_sourceN: string val doc_source: T
- val antiqN: string val antiq: T
- val ML_antiquotationN: string
- val doc_antiquotationN: string
- val doc_antiquotation_optionN: string
- val keyword_declN: string val keyword_decl: string -> T
- val command_declN: string val command_decl: string -> string -> T
- val keywordN: string val keyword: T
- val operatorN: string val operator: T
- val commandN: string val command: T
- val stringN: string val string: T
- val altstringN: string val altstring: T
- val verbatimN: string val verbatim: T
- val commentN: string val comment: T
- val controlN: string val control: T
- val malformedN: string val malformed: T
- val tokenN: string val token: Properties.T -> T
- val command_spanN: string val command_span: string -> T
- val ignored_spanN: string val ignored_span: T
- val malformed_spanN: string val malformed_span: T
- val loaded_theoryN: string val loaded_theory: string -> T
val elapsedN: string
val cpuN: string
val gcN: string
val timingN: string val timing: Timing.timing -> T
- val subgoalsN: string
- val proof_stateN: string val proof_state: int -> T
- val stateN: string val state: T
- val subgoalN: string val subgoal: T
- val sendbackN: string val sendback: T
- val hiliteN: string val hilite: T
- val taskN: string
- val forkedN: string val forked: T
- val joinedN: string val joined: T
- val failedN: string val failed: T
- val finishedN: string val finished: T
- val serialN: string
- val legacyN: string val legacy: T
- val promptN: string val prompt: T
- val readyN: string val ready: T
- val reportN: string val report: T
- val no_reportN: string val no_report: T
- val badN: string val bad: T
- val functionN: string
- val assign_execs: Properties.T
- val removed_versions: Properties.T
- val invoke_scala: string -> string -> Properties.T
- val cancel_scala: string -> Properties.T
val no_output: Output.output * Output.output
val default_output: T -> Output.output * Output.output
val add_mode: string -> (T -> Output.output * Output.output) -> unit
@@ -157,10 +58,6 @@
fun properties more_props ((elem, props): T) =
(elem, fold_rev Properties.put more_props props);
-fun markup_elem elem = (elem, (elem, []): T);
-fun markup_string elem prop = (elem, fn s => (elem, [(prop, s)]): T);
-fun markup_int elem prop = (elem, fn i => (elem, [(prop, print_int i)]): T);
-
(* misc properties *)
@@ -170,148 +67,6 @@
val kindN = "kind";
-(* formal entities *)
-
-val (bindingN, binding) = markup_elem "binding";
-
-val entityN = "entity";
-fun entity kind name = (entityN, [(nameN, name), (kindN, kind)]);
-
-fun get_entity_kind (name, props) =
- if name = entityN then AList.lookup (op =) props kindN
- else NONE;
-
-val defN = "def";
-val refN = "ref";
-
-
-(* position *)
-
-val lineN = "line";
-val offsetN = "offset";
-val end_offsetN = "end_offset";
-val fileN = "file";
-val idN = "id";
-
-val position_properties' = [fileN, idN];
-val position_properties = [lineN, offsetN, end_offsetN] @ position_properties';
-
-val (positionN, position) = markup_elem "position";
-
-
-(* path *)
-
-val (pathN, path) = markup_string "path" nameN;
-
-
-(* pretty printing *)
-
-val indentN = "indent";
-val (blockN, block) = markup_int "block" indentN;
-
-val widthN = "width";
-val (breakN, break) = markup_int "break" widthN;
-
-val (fbreakN, fbreak) = markup_elem "fbreak";
-
-
-(* hidden text *)
-
-val (hiddenN, hidden) = markup_elem "hidden";
-
-
-(* logical entities *)
-
-val classN = "class";
-val typeN = "type";
-val constantN = "constant";
-
-val (fixedN, fixed) = markup_string "fixed" nameN;
-val (dynamic_factN, dynamic_fact) = markup_string "dynamic_fact" nameN;
-
-
-(* inner syntax *)
-
-val (tfreeN, tfree) = markup_elem "tfree";
-val (tvarN, tvar) = markup_elem "tvar";
-val (freeN, free) = markup_elem "free";
-val (skolemN, skolem) = markup_elem "skolem";
-val (boundN, bound) = markup_elem "bound";
-val (varN, var) = markup_elem "var";
-val (numeralN, numeral) = markup_elem "numeral";
-val (literalN, literal) = markup_elem "literal";
-val (delimiterN, delimiter) = markup_elem "delimiter";
-val (inner_stringN, inner_string) = markup_elem "inner_string";
-val (inner_commentN, inner_comment) = markup_elem "inner_comment";
-
-val (token_rangeN, token_range) = markup_elem "token_range";
-
-val (sortN, sort) = markup_elem "sort";
-val (typN, typ) = markup_elem "typ";
-val (termN, term) = markup_elem "term";
-val (propN, prop) = markup_elem "prop";
-
-val (typingN, typing) = markup_elem "typing";
-
-
-(* ML syntax *)
-
-val (ML_keywordN, ML_keyword) = markup_elem "ML_keyword";
-val (ML_delimiterN, ML_delimiter) = markup_elem "ML_delimiter";
-val (ML_tvarN, ML_tvar) = markup_elem "ML_tvar";
-val (ML_numeralN, ML_numeral) = markup_elem "ML_numeral";
-val (ML_charN, ML_char) = markup_elem "ML_char";
-val (ML_stringN, ML_string) = markup_elem "ML_string";
-val (ML_commentN, ML_comment) = markup_elem "ML_comment";
-val (ML_malformedN, ML_malformed) = markup_elem "ML_malformed";
-
-val ML_defN = "ML_def";
-val ML_openN = "ML_open";
-val ML_structN = "ML_struct";
-val (ML_typingN, ML_typing) = markup_elem "ML_typing";
-
-
-(* embedded source text *)
-
-val (ML_sourceN, ML_source) = markup_elem "ML_source";
-val (doc_sourceN, doc_source) = markup_elem "doc_source";
-
-val (antiqN, antiq) = markup_elem "antiq";
-val ML_antiquotationN = "ML antiquotation";
-val doc_antiquotationN = "document antiquotation";
-val doc_antiquotation_optionN = "document antiquotation option";
-
-
-(* outer syntax *)
-
-val (keyword_declN, keyword_decl) = markup_string "keyword_decl" nameN;
-
-val command_declN = "command_decl";
-fun command_decl name kind : T = (command_declN, [(nameN, name), (kindN, kind)]);
-
-val (keywordN, keyword) = markup_elem "keyword";
-val (operatorN, operator) = markup_elem "operator";
-val (commandN, command) = markup_elem "command";
-val (stringN, string) = markup_elem "string";
-val (altstringN, altstring) = markup_elem "altstring";
-val (verbatimN, verbatim) = markup_elem "verbatim";
-val (commentN, comment) = markup_elem "comment";
-val (controlN, control) = markup_elem "control";
-val (malformedN, malformed) = markup_elem "malformed";
-
-val tokenN = "token";
-fun token props = (tokenN, props);
-
-val (command_spanN, command_span) = markup_string "command_span" nameN;
-val (ignored_spanN, ignored_span) = markup_elem "ignored_span";
-val (malformed_spanN, malformed_span) = markup_elem "malformed_span";
-
-
-(* theory loader *)
-
-val (loaded_theoryN, loaded_theory) = markup_string "loaded_theory" nameN;
-
-
(* timing *)
val timingN = "timing";
@@ -326,53 +81,6 @@
(gcN, Time.toString gc)]);
-(* toplevel *)
-
-val subgoalsN = "subgoals";
-val (proof_stateN, proof_state) = markup_int "proof_state" subgoalsN;
-
-val (stateN, state) = markup_elem "state";
-val (subgoalN, subgoal) = markup_elem "subgoal";
-val (sendbackN, sendback) = markup_elem "sendback";
-val (hiliteN, hilite) = markup_elem "hilite";
-
-
-(* command status *)
-
-val taskN = "task";
-
-val (forkedN, forked) = markup_elem "forked";
-val (joinedN, joined) = markup_elem "joined";
-
-val (failedN, failed) = markup_elem "failed";
-val (finishedN, finished) = markup_elem "finished";
-
-
-(* messages *)
-
-val serialN = "serial";
-
-val (legacyN, legacy) = markup_elem "legacy";
-val (promptN, prompt) = markup_elem "prompt";
-val (readyN, ready) = markup_elem "ready";
-
-val (reportN, report) = markup_elem "report";
-val (no_reportN, no_report) = markup_elem "no_report";
-
-val (badN, bad) = markup_elem "bad";
-
-
-(* raw message functions *)
-
-val functionN = "function"
-
-val assign_execs = [(functionN, "assign_execs")];
-val removed_versions = [(functionN, "removed_versions")];
-
-fun invoke_scala name id = [(functionN, "invoke_scala"), (nameN, name), (idN, id)];
-fun cancel_scala id = [(functionN, "cancel_scala"), (idN, id)];
-
-
(** print mode operations **)
--- a/src/Pure/General/markup.scala Mon Nov 28 20:39:08 2011 +0100
+++ b/src/Pure/General/markup.scala Mon Nov 28 22:05:32 2011 +0100
@@ -1,7 +1,7 @@
/* Title: Pure/General/markup.scala
Author: Makarius
-Common markup elements.
+Generic markup elements.
*/
package isabelle
@@ -9,12 +9,7 @@
object Markup
{
- /* empty */
-
- val Empty = Markup("", Nil)
-
-
- /* misc properties */
+ /* properties */
val NAME = "name"
val Name = new Properties.String(NAME)
@@ -23,163 +18,11 @@
val Kind = new Properties.String(KIND)
- /* formal entities */
-
- val BINDING = "binding"
- val ENTITY = "entity"
- val DEF = "def"
- val REF = "ref"
-
- object Entity
- {
- def unapply(markup: Markup): Option[(String, String)] =
- markup match {
- case Markup(ENTITY, props @ Kind(kind)) =>
- props match {
- case Name(name) => Some(kind, name)
- case _ => None
- }
- case _ => None
- }
- }
-
-
- /* position */
-
- val LINE = "line"
- val OFFSET = "offset"
- val END_OFFSET = "end_offset"
- val FILE = "file"
- val ID = "id"
-
- val DEF_LINE = "def_line"
- val DEF_OFFSET = "def_offset"
- val DEF_END_OFFSET = "def_end_offset"
- val DEF_FILE = "def_file"
- val DEF_ID = "def_id"
-
- val POSITION_PROPERTIES = Set(LINE, OFFSET, END_OFFSET, FILE, ID)
- val POSITION = "position"
-
-
- /* path */
-
- val PATH = "path"
-
- object Path
- {
- def unapply(markup: Markup): Option[String] =
- markup match {
- case Markup(PATH, Name(name)) => Some(name)
- case _ => None
- }
- }
-
-
- /* pretty printing */
-
- val Indent = new Properties.Int("indent")
- val BLOCK = "block"
- val Width = new Properties.Int("width")
- val BREAK = "break"
-
-
- /* hidden text */
-
- val HIDDEN = "hidden"
-
-
- /* logical entities */
-
- val CLASS = "class"
- val TYPE = "type"
- val FIXED = "fixed"
- val CONSTANT = "constant"
-
- val DYNAMIC_FACT = "dynamic_fact"
-
-
- /* inner syntax */
+ /* elements */
- val TFREE = "tfree"
- val TVAR = "tvar"
- val FREE = "free"
- val SKOLEM = "skolem"
- val BOUND = "bound"
- val VAR = "var"
- val NUM = "num"
- val FLOAT = "float"
- val XNUM = "xnum"
- val XSTR = "xstr"
- val LITERAL = "literal"
- val DELIMITER = "delimiter"
- val INNER_STRING = "inner_string"
- val INNER_COMMENT = "inner_comment"
-
- val TOKEN_RANGE = "token_range"
-
- val SORT = "sort"
- val TYP = "typ"
- val TERM = "term"
- val PROP = "prop"
-
- val TYPING = "typing"
-
- val ATTRIBUTE = "attribute"
- val METHOD = "method"
-
-
- /* embedded source text */
-
- val ML_SOURCE = "ML_source"
- val DOC_SOURCE = "doc_source"
-
- val ANTIQ = "antiq"
- val ML_ANTIQUOTATION = "ML antiquotation"
- val DOCUMENT_ANTIQUOTATION = "document antiquotation"
- val DOCUMENT_ANTIQUOTATION_OPTION = "document antiquotation option"
-
-
- /* ML syntax */
-
- val ML_KEYWORD = "ML_keyword"
- val ML_DELIMITER = "ML_delimiter"
- val ML_TVAR = "ML_tvar"
- val ML_NUMERAL = "ML_numeral"
- val ML_CHAR = "ML_char"
- val ML_STRING = "ML_string"
- val ML_COMMENT = "ML_comment"
- val ML_MALFORMED = "ML_malformed"
-
- val ML_DEF = "ML_def"
- val ML_OPEN = "ML_open"
- val ML_STRUCT = "ML_struct"
- val ML_TYPING = "ML_typing"
-
-
- /* outer syntax */
-
- val KEYWORD_DECL = "keyword_decl"
- val COMMAND_DECL = "command_decl"
-
- val KEYWORD = "keyword"
- val OPERATOR = "operator"
- val COMMAND = "command"
- val STRING = "string"
- val ALTSTRING = "altstring"
- val VERBATIM = "verbatim"
- val COMMENT = "comment"
- val CONTROL = "control"
- val MALFORMED = "malformed"
-
- val COMMAND_SPAN = "command_span"
- val IGNORED_SPAN = "ignored_span"
- val MALFORMED_SPAN = "malformed_span"
-
-
- /* theory loader */
-
- val LOADED_THEORY = "loaded_theory"
+ val Empty = Markup("", Nil)
+ val Data = Markup("data", Nil)
+ val Broken = Markup("broken", Nil)
/* timing */
@@ -206,101 +49,8 @@
case _ => None
}
}
-
-
- /* toplevel */
-
- val SUBGOALS = "subgoals"
- val PROOF_STATE = "proof_state"
-
- val STATE = "state"
- val SUBGOAL = "subgoal"
- val SENDBACK = "sendback"
- val HILITE = "hilite"
-
-
- /* command status */
-
- val TASK = "task"
-
- val FORKED = "forked"
- val JOINED = "joined"
- val FAILED = "failed"
- val FINISHED = "finished"
-
-
- /* interactive documents */
-
- val VERSION = "version"
- val ASSIGN = "assign"
-
-
- /* prover process */
-
- val PROVER_COMMAND = "prover_command"
- val PROVER_ARG = "prover_arg"
+}
- /* messages */
-
- val Serial = new Properties.Long("serial")
-
- val MESSAGE = "message"
-
- val INIT = "init"
- val STATUS = "status"
- val REPORT = "report"
- val WRITELN = "writeln"
- val TRACING = "tracing"
- val WARNING = "warning"
- val ERROR = "error"
- val RAW = "raw"
- val SYSTEM = "system"
- val STDOUT = "stdout"
- val STDERR = "stderr"
- val EXIT = "exit"
-
- val LEGACY = "legacy"
-
- val NO_REPORT = "no_report"
-
- val BAD = "bad"
-
- val READY = "ready"
-
-
- /* raw message functions */
+sealed case class Markup(name: String, properties: Properties.T)
- val FUNCTION = "function"
- val Function = new Properties.String(FUNCTION)
-
- val Assign_Execs: Properties.T = List((FUNCTION, "assign_execs"))
- val Removed_Versions: Properties.T = List((FUNCTION, "removed_versions"))
-
- val INVOKE_SCALA = "invoke_scala"
- object Invoke_Scala
- {
- def unapply(props: Properties.T): Option[(String, String)] =
- props match {
- case List((FUNCTION, INVOKE_SCALA), (NAME, name), (ID, id)) => Some((name, id))
- case _ => None
- }
- }
-
- val CANCEL_SCALA = "cancel_scala"
- object Cancel_Scala
- {
- def unapply(props: Properties.T): Option[String] =
- props match {
- case List((FUNCTION, CANCEL_SCALA), (ID, id)) => Some(id)
- case _ => None
- }
- }
-
-
- /* system data */
-
- val Data = Markup("data", Nil)
-}
-
-sealed case class Markup(name: String, properties: Properties.T)
--- a/src/Pure/General/name_space.ML Mon Nov 28 20:39:08 2011 +0100
+++ b/src/Pure/General/name_space.ML Mon Nov 28 22:05:32 2011 +0100
@@ -83,7 +83,7 @@
id: serial};
fun entry_markup def kind (name, {pos, id, ...}: entry) =
- Markup.properties (Position.entity_properties_of def id pos) (Markup.entity kind name);
+ Markup.properties (Position.entity_properties_of def id pos) (Isabelle_Markup.entity kind name);
fun print_entry def kind (name, entry) =
quote (Markup.markup (entry_markup def kind (name, entry)) name);
@@ -126,7 +126,7 @@
fun markup (Name_Space {kind, entries, ...}) name =
(case Symtab.lookup entries name of
- NONE => Markup.hilite
+ NONE => Isabelle_Markup.hilite
| SOME (_, entry) => entry_markup false kind (name, entry));
fun is_concealed space name = #concealed (the_entry space name);
--- a/src/Pure/General/path.ML Mon Nov 28 20:39:08 2011 +0100
+++ b/src/Pure/General/path.ML Mon Nov 28 22:05:32 2011 +0100
@@ -155,7 +155,7 @@
fun pretty path =
let val s = implode_path path
- in Pretty.mark (Markup.path s) (Pretty.str (quote s)) end;
+ in Pretty.mark (Isabelle_Markup.path s) (Pretty.str (quote s)) end;
val print = Pretty.str_of o pretty;
--- a/src/Pure/General/position.ML Mon Nov 28 20:39:08 2011 +0100
+++ b/src/Pure/General/position.ML Mon Nov 28 22:05:32 2011 +0100
@@ -58,7 +58,8 @@
datatype T = Pos of (int * int * int) * Properties.T;
fun norm_props (props: Properties.T) =
- maps (fn a => the_list (find_first (fn (b, _) => a = b) props)) Markup.position_properties';
+ maps (fn a => the_list (find_first (fn (b, _) => a = b) props))
+ Isabelle_Markup.position_properties';
fun make {line = i, offset = j, end_offset = k, props} = Pos ((i, j, k), norm_props props);
fun dest (Pos ((i, j, k), props)) = {line = i, offset = j, end_offset = k, props = props};
@@ -73,7 +74,7 @@
fun offset_of (Pos ((_, j, _), _)) = if valid j then SOME j else NONE;
fun end_offset_of (Pos ((_, _, k), _)) = if valid k then SOME k else NONE;
-fun file_of (Pos (_, props)) = Properties.get props Markup.fileN;
+fun file_of (Pos (_, props)) = Properties.get props Isabelle_Markup.fileN;
(* advance *)
@@ -105,7 +106,7 @@
fun file_name "" = []
- | file_name name = [(Markup.fileN, name)];
+ | file_name name = [(Isabelle_Markup.fileN, name)];
fun file_only name = Pos ((0, 0, 0), file_name name);
fun file name = Pos ((1, 1, 0), file_name name);
@@ -113,11 +114,11 @@
fun line_file i name = Pos ((i, 1, 0), file_name name);
fun line i = line_file i "";
-fun id id = Pos ((0, 1, 0), [(Markup.idN, id)]);
-fun id_only id = Pos ((0, 0, 0), [(Markup.idN, id)]);
+fun id id = Pos ((0, 1, 0), [(Isabelle_Markup.idN, id)]);
+fun id_only id = Pos ((0, 0, 0), [(Isabelle_Markup.idN, id)]);
-fun get_id (Pos (_, props)) = Properties.get props Markup.idN;
-fun put_id id (Pos (count, props)) = Pos (count, Properties.put (Markup.idN, id) props);
+fun get_id (Pos (_, props)) = Properties.get props Isabelle_Markup.idN;
+fun put_id id (Pos (count, props)) = Pos (count, Properties.put (Isabelle_Markup.idN, id) props);
(* markup properties *)
@@ -129,24 +130,26 @@
NONE => 0
| SOME s => the_default 0 (Int.fromString s));
in
- make {line = get Markup.lineN, offset = get Markup.offsetN,
- end_offset = get Markup.end_offsetN, props = props}
+ make {line = get Isabelle_Markup.lineN, offset = get Isabelle_Markup.offsetN,
+ end_offset = get Isabelle_Markup.end_offsetN, props = props}
end;
fun value k i = if valid i then [(k, string_of_int i)] else [];
fun properties_of (Pos ((i, j, k), props)) =
- value Markup.lineN i @ value Markup.offsetN j @ value Markup.end_offsetN k @ props;
+ value Isabelle_Markup.lineN i @
+ value Isabelle_Markup.offsetN j @
+ value Isabelle_Markup.end_offsetN k @ props;
val def_properties_of = properties_of #> (map (fn (x, y) => ("def_" ^ x, y)));
fun entity_properties_of def id pos =
- if def then (Markup.defN, string_of_int id) :: properties_of pos
- else (Markup.refN, string_of_int id) :: def_properties_of pos;
+ if def then (Isabelle_Markup.defN, string_of_int id) :: properties_of pos
+ else (Isabelle_Markup.refN, string_of_int id) :: def_properties_of pos;
fun default_properties default props =
- if exists (member (op =) Markup.position_properties o #1) props then props
+ if exists (member (op =) Isabelle_Markup.position_properties o #1) props then props
else properties_of default @ props;
val markup = Markup.properties o properties_of;
@@ -185,7 +188,9 @@
| _ => "");
in
if null props then ""
- else (if s = "" then "" else " ") ^ Markup.markup (Markup.properties props Markup.position) s
+ else
+ (if s = "" then "" else " ") ^
+ Markup.markup (Markup.properties props Isabelle_Markup.position) s
end;
--- a/src/Pure/General/position.scala Mon Nov 28 20:39:08 2011 +0100
+++ b/src/Pure/General/position.scala Mon Nov 28 22:05:32 2011 +0100
@@ -11,11 +11,11 @@
{
type T = Properties.T
- val Line = new Properties.Int(Markup.LINE)
- val Offset = new Properties.Int(Markup.OFFSET)
- val End_Offset = new Properties.Int(Markup.END_OFFSET)
- val File = new Properties.String(Markup.FILE)
- val Id = new Properties.Long(Markup.ID)
+ val Line = new Properties.Int(Isabelle_Markup.LINE)
+ val Offset = new Properties.Int(Isabelle_Markup.OFFSET)
+ val End_Offset = new Properties.Int(Isabelle_Markup.END_OFFSET)
+ val File = new Properties.String(Isabelle_Markup.FILE)
+ val Id = new Properties.Long(Isabelle_Markup.ID)
object Range
{
@@ -38,13 +38,13 @@
}
private val purge_pos = Map(
- Markup.DEF_LINE -> Markup.LINE,
- Markup.DEF_OFFSET -> Markup.OFFSET,
- Markup.DEF_END_OFFSET -> Markup.END_OFFSET,
- Markup.DEF_FILE -> Markup.FILE,
- Markup.DEF_ID -> Markup.ID)
+ Isabelle_Markup.DEF_LINE -> Isabelle_Markup.LINE,
+ Isabelle_Markup.DEF_OFFSET -> Isabelle_Markup.OFFSET,
+ Isabelle_Markup.DEF_END_OFFSET -> Isabelle_Markup.END_OFFSET,
+ Isabelle_Markup.DEF_FILE -> Isabelle_Markup.FILE,
+ Isabelle_Markup.DEF_ID -> Isabelle_Markup.ID)
def purge(props: T): T =
- for ((x, y) <- props if !Markup.POSITION_PROPERTIES(x))
+ for ((x, y) <- props if !Isabelle_Markup.POSITION_PROPERTIES(x))
yield (if (purge_pos.isDefinedAt(x)) (purge_pos(x), y) else (x, y))
}
--- a/src/Pure/General/pretty.ML Mon Nov 28 20:39:08 2011 +0100
+++ b/src/Pure/General/pretty.ML Mon Nov 28 22:05:32 2011 +0100
@@ -133,8 +133,8 @@
fun mark_str (m, s) = mark m (str s);
fun marks_str (ms, s) = fold_rev mark ms (str s);
-fun keyword name = mark_str (Markup.keyword, name);
-fun command name = mark_str (Markup.command, name);
+fun keyword name = mark_str (Isabelle_Markup.keyword, name);
+fun command name = mark_str (Isabelle_Markup.command, name);
fun markup_chunks m prts = markup m (fbreaks prts);
val chunks = markup_chunks Markup.empty;
@@ -276,9 +276,12 @@
let
fun out (Block ((bg, en), [], _, _)) = Buffer.add bg #> Buffer.add en
| out (Block ((bg, en), prts, indent, _)) =
- Buffer.add bg #> Buffer.markup (Markup.block indent) (fold out prts) #> Buffer.add en
+ Buffer.add bg #>
+ Buffer.markup (Isabelle_Markup.block indent) (fold out prts) #>
+ Buffer.add en
| out (String (s, _)) = Buffer.add s
- | out (Break (false, wd)) = Buffer.markup (Markup.break wd) (Buffer.add (output_spaces wd))
+ | out (Break (false, wd)) =
+ Buffer.markup (Isabelle_Markup.break wd) (Buffer.add (output_spaces wd))
| out (Break (true, _)) = Buffer.add (Output.output "\n");
in out prt Buffer.empty end;
--- a/src/Pure/General/pretty.scala Mon Nov 28 20:39:08 2011 +0100
+++ b/src/Pure/General/pretty.scala Mon Nov 28 22:05:32 2011 +0100
@@ -19,11 +19,12 @@
object Block
{
def apply(i: Int, body: XML.Body): XML.Tree =
- XML.Elem(Markup(Markup.BLOCK, Markup.Indent(i)), body)
+ XML.Elem(Markup(Isabelle_Markup.BLOCK, Isabelle_Markup.Indent(i)), body)
def unapply(tree: XML.Tree): Option[(Int, XML.Body)] =
tree match {
- case XML.Elem(Markup(Markup.BLOCK, Markup.Indent(i)), body) => Some((i, body))
+ case XML.Elem(Markup(Isabelle_Markup.BLOCK, Isabelle_Markup.Indent(i)), body) =>
+ Some((i, body))
case _ => None
}
}
@@ -31,11 +32,12 @@
object Break
{
def apply(w: Int): XML.Tree =
- XML.Elem(Markup(Markup.BREAK, Markup.Width(w)), List(XML.Text(Symbol.spaces(w))))
+ XML.Elem(Markup(Isabelle_Markup.BREAK, Isabelle_Markup.Width(w)),
+ List(XML.Text(Symbol.spaces(w))))
def unapply(tree: XML.Tree): Option[Int] =
tree match {
- case XML.Elem(Markup(Markup.BREAK, Markup.Width(w)), _) => Some(w)
+ case XML.Elem(Markup(Isabelle_Markup.BREAK, Isabelle_Markup.Width(w)), _) => Some(w)
case _ => None
}
}
--- a/src/Pure/IsaMakefile Mon Nov 28 20:39:08 2011 +0100
+++ b/src/Pure/IsaMakefile Mon Nov 28 22:05:32 2011 +0100
@@ -80,6 +80,7 @@
General/graph.ML \
General/heap.ML \
General/integer.ML \
+ General/isabelle_markup.ML \
General/linear_set.ML \
General/long_name.ML \
General/markup.ML \
--- a/src/Pure/Isar/isar_cmd.ML Mon Nov 28 20:39:08 2011 +0100
+++ b/src/Pure/Isar/isar_cmd.ML Mon Nov 28 22:05:32 2011 +0100
@@ -515,7 +515,7 @@
(* markup commands *)
fun check_text (txt, pos) state =
- (Position.report pos Markup.doc_source;
+ (Position.report pos Isabelle_Markup.doc_source;
ignore (Thy_Output.eval_antiquote (#1 (Keyword.get_lexicons ())) state (txt, pos)));
fun header_markup txt = Toplevel.keep (fn state =>
--- a/src/Pure/Isar/keyword.ML Mon Nov 28 20:39:08 2011 +0100
+++ b/src/Pure/Isar/keyword.ML Mon Nov 28 22:05:32 2011 +0100
@@ -156,11 +156,11 @@
(if print_mode_active keyword_statusN then Output.status else writeln) s;
fun keyword_status name =
- status_message (Markup.markup (Markup.keyword_decl name)
+ status_message (Markup.markup (Isabelle_Markup.keyword_decl name)
("Outer syntax keyword: " ^ quote name));
fun command_status (name, kind) =
- status_message (Markup.markup (Markup.command_decl name (kind_of kind))
+ status_message (Markup.markup (Isabelle_Markup.command_decl name (kind_of kind))
("Outer syntax command: " ^ quote name ^ " (" ^ kind_of kind ^ ")"));
fun status () =
--- a/src/Pure/Isar/keyword.scala Mon Nov 28 20:39:08 2011 +0100
+++ b/src/Pure/Isar/keyword.scala Mon Nov 28 22:05:32 2011 +0100
@@ -61,7 +61,8 @@
object Keyword_Decl {
def unapply(msg: XML.Tree): Option[String] =
msg match {
- case XML.Elem(Markup(Markup.KEYWORD_DECL, List((Markup.NAME, name))), _) => Some(name)
+ case XML.Elem(Markup(Isabelle_Markup.KEYWORD_DECL, List((Markup.NAME, name))), _) =>
+ Some(name)
case _ => None
}
}
@@ -69,8 +70,8 @@
object Command_Decl {
def unapply(msg: XML.Tree): Option[(String, String)] =
msg match {
- case XML.Elem(Markup(Markup.COMMAND_DECL, List((Markup.NAME, name), (Markup.KIND, kind))), _) =>
- Some((name, kind))
+ case XML.Elem(Markup(Isabelle_Markup.COMMAND_DECL,
+ List((Markup.NAME, name), (Markup.KIND, kind))), _) => Some((name, kind))
case _ => None
}
}
--- a/src/Pure/Isar/proof.ML Mon Nov 28 20:39:08 2011 +0100
+++ b/src/Pure/Isar/proof.ML Mon Nov 28 22:05:32 2011 +0100
@@ -522,7 +522,7 @@
fun status_markup state =
(case try goal state of
- SOME {goal, ...} => Markup.proof_state (Thm.nprems_of goal)
+ SOME {goal, ...} => Isabelle_Markup.proof_state (Thm.nprems_of goal)
| NONE => Markup.empty);
@@ -998,7 +998,8 @@
fun print_rule ctxt th =
if ! testing then rule := SOME th
else if int then
- writeln (Markup.markup Markup.state (Proof_Display.string_of_rule ctxt "Successful" th))
+ writeln
+ (Markup.markup Isabelle_Markup.state (Proof_Display.string_of_rule ctxt "Successful" th))
else ();
val test_proof =
try (local_skip_proof true)
--- a/src/Pure/Isar/proof_context.ML Mon Nov 28 20:39:08 2011 +0100
+++ b/src/Pure/Isar/proof_context.ML Mon Nov 28 22:05:32 2011 +0100
@@ -463,7 +463,7 @@
val (c, pos) = token_content text;
in
if Lexicon.is_tid c then
- (Context_Position.report ctxt pos Markup.tfree;
+ (Context_Position.report ctxt pos Isabelle_Markup.tfree;
TFree (c, default_sort ctxt (c, ~1)))
else
let
@@ -495,7 +495,8 @@
(case (Variable.lookup_fixed ctxt c, Variable.is_const ctxt c) of
(SOME x, false) =>
(Context_Position.report ctxt pos
- (Markup.name x (if can Name.dest_skolem x then Markup.skolem else Markup.free));
+ (Markup.name x
+ (if can Name.dest_skolem x then Isabelle_Markup.skolem else Isabelle_Markup.free));
Free (x, infer_type ctxt (x, ty)))
| _ => prep_const_proper ctxt strict (c, pos))
end;
--- a/src/Pure/Isar/runtime.ML Mon Nov 28 20:39:08 2011 +0100
+++ b/src/Pure/Isar/runtime.ML Mon Nov 28 22:05:32 2011 +0100
@@ -65,7 +65,7 @@
fun exn_msgs (context, (i, exn)) =
(case exn of
EXCURSION_FAIL (exn, loc) =>
- map (apsnd (fn msg => msg ^ Markup.markup Markup.no_report ("\n" ^ loc)))
+ map (apsnd (fn msg => msg ^ Markup.markup Isabelle_Markup.no_report ("\n" ^ loc)))
(sorted_msgs context exn)
| _ =>
let
--- a/src/Pure/Isar/token.ML Mon Nov 28 20:39:08 2011 +0100
+++ b/src/Pure/Isar/token.ML Mon Nov 28 22:05:32 2011 +0100
@@ -189,7 +189,9 @@
fun source_of (Token ((source, (pos, _)), (_, x), _)) =
if YXML.detect x then x
- else YXML.string_of (XML.Elem (Markup.token (Position.properties_of pos), [XML.Text source]));
+ else
+ YXML.string_of
+ (XML.Elem (Isabelle_Markup.token (Position.properties_of pos), [XML.Text source]));
fun source_position_of (Token ((source, (pos, _)), _, _)) = (source, pos);
--- a/src/Pure/Isar/toplevel.ML Mon Nov 28 20:39:08 2011 +0100
+++ b/src/Pure/Isar/toplevel.ML Mon Nov 28 22:05:32 2011 +0100
@@ -210,7 +210,7 @@
| SOME (Proof (prf, _)) =>
Proof.pretty_state (Proof_Node.position prf) (Proof_Node.current prf)
| SOME (SkipProof (d, _)) => [Pretty.str ("skipped proof: depth " ^ string_of_int d)])
- |> Pretty.markup_chunks Markup.state |> Pretty.writeln;
+ |> Pretty.markup_chunks Isabelle_Markup.state |> Pretty.writeln;
fun pretty_abstract state = Pretty.str ("<Isar " ^ str_of_state state ^ ">");
--- a/src/Pure/ML/ml_compiler_polyml-5.3.ML Mon Nov 28 20:39:08 2011 +0100
+++ b/src/Pure/ML/ml_compiler_polyml-5.3.ML Mon Nov 28 22:05:32 2011 +0100
@@ -15,7 +15,7 @@
endLine = _, endPosition = end_offset} = loc;
val props =
(case YXML.parse text of
- XML.Elem ((e, atts), _) => if e = Markup.positionN then atts else []
+ XML.Elem ((e, atts), _) => if e = Isabelle_Markup.positionN then atts else []
| XML.Text s => Position.file_name s);
in
Position.make {line = line, offset = offset, end_offset = end_offset, props = props}
@@ -41,19 +41,20 @@
fun reported_entity kind loc decl =
reported_text (position_of loc)
- (Markup.entityN, (Markup.kindN, kind) :: Position.def_properties_of (position_of decl)) "";
+ (Isabelle_Markup.entityN,
+ (Markup.kindN, kind) :: Position.def_properties_of (position_of decl)) "";
fun reported loc (PolyML.PTtype types) =
cons
(PolyML.NameSpace.displayTypeExpression (types, depth, space)
|> pretty_ml |> Pretty.from_ML |> Pretty.string_of
- |> reported_text (position_of loc) Markup.ML_typing)
+ |> reported_text (position_of loc) Isabelle_Markup.ML_typing)
| reported loc (PolyML.PTdeclaredAt decl) =
- cons (reported_entity Markup.ML_defN loc decl)
+ cons (reported_entity Isabelle_Markup.ML_defN loc decl)
| reported loc (PolyML.PTopenedAt decl) =
- cons (reported_entity Markup.ML_openN loc decl)
+ cons (reported_entity Isabelle_Markup.ML_openN loc decl)
| reported loc (PolyML.PTstructureAt decl) =
- cons (reported_entity Markup.ML_structN loc decl)
+ cons (reported_entity Isabelle_Markup.ML_structN loc decl)
| reported _ (PolyML.PTnextSibling tree) = reported_tree (tree ())
| reported _ (PolyML.PTfirstChild tree) = reported_tree (tree ())
| reported _ _ = I
@@ -72,8 +73,9 @@
(* input *)
val location_props =
- op ^ (YXML.output_markup (Markup.position |> Markup.properties
- (filter (member (op =) [Markup.idN, Markup.fileN] o #1) (Position.properties_of pos))));
+ op ^ (YXML.output_markup (Isabelle_Markup.position |> Markup.properties
+ (filter (member (op =)
+ [Isabelle_Markup.idN, Isabelle_Markup.fileN] o #1) (Position.properties_of pos))));
val input_buffer =
Unsynchronized.ref (toks |> map
@@ -111,10 +113,10 @@
let
val pos = position_of loc;
val txt =
- (Position.is_reported pos ? Markup.markup Markup.no_report)
+ (Position.is_reported pos ? Markup.markup Isabelle_Markup.no_report)
((if hard then "Error" else "Warning") ^ Position.str_of pos ^ ":\n") ^
Pretty.string_of (Pretty.from_ML (pretty_ml msg)) ^
- Position.reported_text pos Markup.report "";
+ Position.reported_text pos Isabelle_Markup.report "";
in if hard then err txt else warn txt end;
--- a/src/Pure/ML/ml_context.ML Mon Nov 28 20:39:08 2011 +0100
+++ b/src/Pure/ML/ml_context.ML Mon Nov 28 22:05:32 2011 +0100
@@ -103,7 +103,7 @@
structure Antiq_Parsers = Theory_Data
(
type T = (Position.T -> antiq context_parser) Name_Space.table;
- val empty : T = Name_Space.empty_table Markup.ML_antiquotationN;
+ val empty : T = Name_Space.empty_table Isabelle_Markup.ML_antiquotationN;
val extend = I;
fun merge data : T = Name_Space.merge_tables data;
);
@@ -121,7 +121,7 @@
val thy = Proof_Context.theory_of ctxt;
val ((xname, _), pos) = Args.dest_src src;
val (_, scan) = Name_Space.check ctxt (Antiq_Parsers.get thy) (xname, pos);
- in Args.context_syntax Markup.ML_antiquotationN (scan pos) src ctxt end;
+ in Args.context_syntax Isabelle_Markup.ML_antiquotationN (scan pos) src ctxt end;
(* parsing and evaluation *)
--- a/src/Pure/ML/ml_lex.ML Mon Nov 28 20:39:08 2011 +0100
+++ b/src/Pure/ML/ml_lex.ML Mon Nov 28 22:05:32 2011 +0100
@@ -104,23 +104,23 @@
local
val token_kind_markup =
- fn Keyword => Markup.ML_keyword
+ fn Keyword => Isabelle_Markup.ML_keyword
| Ident => Markup.empty
| LongIdent => Markup.empty
- | TypeVar => Markup.ML_tvar
- | Word => Markup.ML_numeral
- | Int => Markup.ML_numeral
- | Real => Markup.ML_numeral
- | Char => Markup.ML_char
- | String => Markup.ML_string
+ | TypeVar => Isabelle_Markup.ML_tvar
+ | Word => Isabelle_Markup.ML_numeral
+ | Int => Isabelle_Markup.ML_numeral
+ | Real => Isabelle_Markup.ML_numeral
+ | Char => Isabelle_Markup.ML_char
+ | String => Isabelle_Markup.ML_string
| Space => Markup.empty
- | Comment => Markup.ML_comment
- | Error _ => Markup.ML_malformed
+ | Comment => Isabelle_Markup.ML_comment
+ | Error _ => Isabelle_Markup.ML_malformed
| EOF => Markup.empty;
fun token_markup kind x =
if kind = Keyword andalso exists_string (not o Symbol.is_ascii_letter) x
- then Markup.ML_delimiter
+ then Isabelle_Markup.ML_delimiter
else token_kind_markup kind;
in
@@ -278,7 +278,7 @@
fun read pos txt =
let
- val _ = Position.report pos Markup.ML_source;
+ val _ = Position.report pos Isabelle_Markup.ML_source;
val syms = Symbol_Pos.explode (txt, pos);
val termination =
if null syms then []
--- a/src/Pure/PIDE/command.scala Mon Nov 28 20:39:08 2011 +0100
+++ b/src/Pure/PIDE/command.scala Mon Nov 28 22:05:32 2011 +0100
@@ -32,7 +32,7 @@
def root_info: Text.Markup =
Text.Info(command.range,
- XML.Elem(Markup(Markup.STATUS, Nil), status.reverse.map(XML.Elem(_, Nil))))
+ XML.Elem(Markup(Isabelle_Markup.STATUS, Nil), status.reverse.map(XML.Elem(_, Nil))))
def root_markup: Markup_Tree = markup + root_info
@@ -40,14 +40,14 @@
def accumulate(message: XML.Elem): Command.State =
message match {
- case XML.Elem(Markup(Markup.STATUS, _), msgs) =>
+ case XML.Elem(Markup(Isabelle_Markup.STATUS, _), msgs) =>
(this /: msgs)((state, msg) =>
msg match {
case XML.Elem(markup, Nil) => state.add_status(markup)
case _ => System.err.println("Ignored status message: " + msg); state
})
- case XML.Elem(Markup(Markup.REPORT, _), msgs) =>
+ case XML.Elem(Markup(Isabelle_Markup.REPORT, _), msgs) =>
(this /: msgs)((state, msg) =>
msg match {
case XML.Elem(Markup(name, atts @ Position.Id_Range(id, raw_range)), args)
@@ -62,7 +62,7 @@
})
case XML.Elem(Markup(name, atts), body) =>
atts match {
- case Markup.Serial(i) =>
+ case Isabelle_Markup.Serial(i) =>
val result = XML.Elem(Markup(name, Position.purge(atts)), body)
val st0 = add_result(i, result)
val st1 =
--- a/src/Pure/PIDE/document.ML Mon Nov 28 20:39:08 2011 +0100
+++ b/src/Pure/PIDE/document.ML Mon Nov 28 22:05:32 2011 +0100
@@ -333,22 +333,22 @@
val is_proof = Keyword.is_proof (Toplevel.name_of tr);
val _ = Multithreading.interrupted ();
- val _ = Toplevel.status tr Markup.forked;
+ val _ = Toplevel.status tr Isabelle_Markup.forked;
val start = Timing.start ();
val (errs, result) = run (is_init orelse is_proof) (Toplevel.set_print false tr) st;
val _ = timing tr (Timing.result start);
- val _ = Toplevel.status tr Markup.joined;
+ val _ = Toplevel.status tr Isabelle_Markup.joined;
val _ = List.app (Toplevel.error_msg tr) errs;
in
(case result of
NONE =>
let
val _ = if null errs then Exn.interrupt () else ();
- val _ = Toplevel.status tr Markup.failed;
+ val _ = Toplevel.status tr Isabelle_Markup.failed;
in (st, no_print) end
| SOME st' =>
let
- val _ = Toplevel.status tr Markup.finished;
+ val _ = Toplevel.status tr Isabelle_Markup.finished;
val _ = proof_status tr st';
val do_print =
not is_init andalso
--- a/src/Pure/PIDE/isar_document.ML Mon Nov 28 20:39:08 2011 +0100
+++ b/src/Pure/PIDE/isar_document.ML Mon Nov 28 22:05:32 2011 +0100
@@ -57,7 +57,7 @@
val (assignment, state1) = Document.update old_id new_id edits state;
val _ = Future.join_tasks running;
val _ =
- Output.raw_message Markup.assign_execs
+ Output.raw_message Isabelle_Markup.assign_execs
((new_id, assignment) |>
let open XML.Encode
in pair int (pair (list (pair int (option int))) (list (pair string (option int)))) end
@@ -73,7 +73,7 @@
YXML.parse_body versions_yxml |>
let open XML.Decode in list int end;
val state1 = Document.remove_versions versions state;
- val _ = Output.raw_message Markup.removed_versions versions_yxml;
+ val _ = Output.raw_message Isabelle_Markup.removed_versions versions_yxml;
in state1 end));
val _ =
--- a/src/Pure/PIDE/isar_document.scala Mon Nov 28 20:39:08 2011 +0100
+++ b/src/Pure/PIDE/isar_document.scala Mon Nov 28 22:05:32 2011 +0100
@@ -52,13 +52,13 @@
def command_status(markup: List[Markup]): Status =
{
val forks = (0 /: markup) {
- case (i, Markup(Markup.FORKED, _)) => i + 1
- case (i, Markup(Markup.JOINED, _)) => i - 1
+ case (i, Markup(Isabelle_Markup.FORKED, _)) => i + 1
+ case (i, Markup(Isabelle_Markup.JOINED, _)) => i - 1
case (i, _) => i
}
if (forks != 0) Forked(forks)
- else if (markup.exists(_.name == Markup.FAILED)) Failed
- else if (markup.exists(_.name == Markup.FINISHED)) Finished
+ else if (markup.exists(_.name == Isabelle_Markup.FAILED)) Failed
+ else if (markup.exists(_.name == Isabelle_Markup.FINISHED)) Finished
else Unprocessed
}
@@ -88,12 +88,12 @@
/* result messages */
def clean_message(body: XML.Body): XML.Body =
- body filter { case XML.Elem(Markup(Markup.NO_REPORT, _), _) => false case _ => true } map
+ body filter { case XML.Elem(Markup(Isabelle_Markup.NO_REPORT, _), _) => false case _ => true } map
{ case XML.Elem(markup, ts) => XML.Elem(markup, clean_message(ts)) case t => t }
def message_reports(msg: XML.Tree): List[XML.Elem] =
msg match {
- case elem @ XML.Elem(Markup(Markup.REPORT, _), _) => List(elem)
+ case elem @ XML.Elem(Markup(Isabelle_Markup.REPORT, _), _) => List(elem)
case XML.Elem(_, body) => body.flatMap(message_reports)
case XML.Text(_) => Nil
}
@@ -103,33 +103,33 @@
def is_ready(msg: XML.Tree): Boolean =
msg match {
- case XML.Elem(Markup(Markup.STATUS, _),
- List(XML.Elem(Markup(Markup.READY, _), _))) => true
+ case XML.Elem(Markup(Isabelle_Markup.STATUS, _),
+ List(XML.Elem(Markup(Isabelle_Markup.READY, _), _))) => true
case _ => false
}
def is_tracing(msg: XML.Tree): Boolean =
msg match {
- case XML.Elem(Markup(Markup.TRACING, _), _) => true
+ case XML.Elem(Markup(Isabelle_Markup.TRACING, _), _) => true
case _ => false
}
def is_warning(msg: XML.Tree): Boolean =
msg match {
- case XML.Elem(Markup(Markup.WARNING, _), _) => true
+ case XML.Elem(Markup(Isabelle_Markup.WARNING, _), _) => true
case _ => false
}
def is_error(msg: XML.Tree): Boolean =
msg match {
- case XML.Elem(Markup(Markup.ERROR, _), _) => true
+ case XML.Elem(Markup(Isabelle_Markup.ERROR, _), _) => true
case _ => false
}
def is_state(msg: XML.Tree): Boolean =
msg match {
- case XML.Elem(Markup(Markup.WRITELN, _),
- List(XML.Elem(Markup(Markup.STATE, _), _))) => true
+ case XML.Elem(Markup(Isabelle_Markup.WRITELN, _),
+ List(XML.Elem(Markup(Isabelle_Markup.STATE, _), _))) => true
case _ => false
}
@@ -137,7 +137,8 @@
/* reported positions */
private val include_pos =
- Set(Markup.BINDING, Markup.ENTITY, Markup.REPORT, Markup.POSITION)
+ Set(Isabelle_Markup.BINDING, Isabelle_Markup.ENTITY, Isabelle_Markup.REPORT,
+ Isabelle_Markup.POSITION)
def message_positions(command: Command, message: XML.Elem): Set[Text.Range] =
{
--- a/src/Pure/PIDE/yxml.scala Mon Nov 28 20:39:08 2011 +0100
+++ b/src/Pure/PIDE/yxml.scala Mon Nov 28 22:05:32 2011 +0100
@@ -118,18 +118,18 @@
/* failsafe parsing */
- private def markup_malformed(source: CharSequence) =
- XML.elem(Markup.MALFORMED, List(XML.Text(source.toString)))
+ private def markup_broken(source: CharSequence) =
+ XML.elem(Markup.Broken.name, List(XML.Text(source.toString)))
def parse_body_failsafe(source: CharSequence): XML.Body =
{
try { parse_body(source) }
- catch { case ERROR(_) => List(markup_malformed(source)) }
+ catch { case ERROR(_) => List(markup_broken(source)) }
}
def parse_failsafe(source: CharSequence): XML.Tree =
{
try { parse(source) }
- catch { case ERROR(_) => markup_malformed(source) }
+ catch { case ERROR(_) => markup_broken(source) }
}
}
--- a/src/Pure/ProofGeneral/proof_general_emacs.ML Mon Nov 28 20:39:08 2011 +0100
+++ b/src/Pure/ProofGeneral/proof_general_emacs.ML Mon Nov 28 22:05:32 2011 +0100
@@ -34,24 +34,24 @@
| render_tree (XML.Elem ((name, props), ts)) =
let
val (bg1, en1) =
- if name <> Markup.promptN andalso print_mode_active test_markupN
+ if name <> Isabelle_Markup.promptN andalso print_mode_active test_markupN
then XML.output_markup (name, props)
else Markup.no_output;
val (bg2, en2) =
if null ts then Markup.no_output
- else if name = Markup.stateN then (special "O" ^ "\n", "\n" ^ special "P")
- else if name = Markup.sendbackN then (special "W", special "X")
- else if name = Markup.hiliteN then (special "0", special "1")
- else if name = Markup.tfreeN then (special "C", special "A")
- else if name = Markup.tvarN then (special "D", special "A")
- else if name = Markup.freeN then (special "E", special "A")
- else if name = Markup.boundN then (special "F", special "A")
- else if name = Markup.varN then (special "G", special "A")
- else if name = Markup.skolemN then (special "H", special "A")
+ else if name = Isabelle_Markup.stateN then (special "O" ^ "\n", "\n" ^ special "P")
+ else if name = Isabelle_Markup.sendbackN then (special "W", special "X")
+ else if name = Isabelle_Markup.hiliteN then (special "0", special "1")
+ else if name = Isabelle_Markup.tfreeN then (special "C", special "A")
+ else if name = Isabelle_Markup.tvarN then (special "D", special "A")
+ else if name = Isabelle_Markup.freeN then (special "E", special "A")
+ else if name = Isabelle_Markup.boundN then (special "F", special "A")
+ else if name = Isabelle_Markup.varN then (special "G", special "A")
+ else if name = Isabelle_Markup.skolemN then (special "H", special "A")
else
- (case Markup.get_entity_kind (name, props) of
+ (case Isabelle_Markup.get_entity_kind (name, props) of
SOME kind =>
- if kind = Markup.classN then (special "B", special "A")
+ if kind = Isabelle_Markup.classN then (special "B", special "A")
else Markup.no_output
| NONE => Markup.no_output);
in
@@ -108,7 +108,7 @@
emacs_notify ("Proof General, you can unlock the file " ^ quote (File.platform_path path));
fun sendback heading prts =
- Pretty.writeln (Pretty.big_list heading [Pretty.markup Markup.sendback prts]);
+ Pretty.writeln (Pretty.big_list heading [Pretty.markup Isabelle_Markup.sendback prts]);
(* theory loader actions *)
--- a/src/Pure/ProofGeneral/proof_general_pgip.ML Mon Nov 28 20:39:08 2011 +0100
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML Mon Nov 28 22:05:32 2011 +0100
@@ -101,8 +101,8 @@
val pgml_syms = map pgml_sym o Symbol.explode;
val token_markups =
- [Markup.tfreeN, Markup.tvarN, Markup.freeN,
- Markup.boundN, Markup.varN, Markup.skolemN];
+ [Isabelle_Markup.tfreeN, Isabelle_Markup.tvarN, Isabelle_Markup.freeN,
+ Isabelle_Markup.boundN, Isabelle_Markup.varN, Isabelle_Markup.skolemN];
in
@@ -112,10 +112,11 @@
in [Pgml.Atoms {kind = SOME name, content = content}] end
else
let val content = maps pgml_terms body in
- if name = Markup.blockN then
- [Pgml.Box {orient = NONE, indent = Properties.get_int atts Markup.indentN, content = content}]
- else if name = Markup.breakN then
- [Pgml.Break {mandatory = NONE, indent = Properties.get_int atts Markup.widthN}]
+ if name = Isabelle_Markup.blockN then
+ [Pgml.Box {orient = NONE,
+ indent = Properties.get_int atts Isabelle_Markup.indentN, content = content}]
+ else if name = Isabelle_Markup.breakN then
+ [Pgml.Break {mandatory = NONE, indent = Properties.get_int atts Isabelle_Markup.widthN}]
else content
end
| pgml_terms (XML.Text text) = map (Pgml.Raw o Pgml.atom_to_xml) (pgml_syms text);
@@ -134,7 +135,7 @@
val area =
(case body of
[XML.Elem ((name, _), _)] =>
- if name = Markup.stateN then PgipTypes.Display else default_area
+ if name = Isabelle_Markup.stateN then PgipTypes.Display else default_area
| _ => default_area);
in Pgml.pgml_to_xml (pgml area (maps pgml_terms body)) end;
--- a/src/Pure/ROOT.ML Mon Nov 28 20:39:08 2011 +0100
+++ b/src/Pure/ROOT.ML Mon Nov 28 22:05:32 2011 +0100
@@ -31,7 +31,8 @@
use "General/output.ML";
use "General/timing.ML";
use "General/markup.ML";
-fun legacy_feature s = warning (Markup.markup Markup.legacy ("Legacy feature! " ^ s));
+use "General/isabelle_markup.ML";
+fun legacy_feature s = warning (Markup.markup Isabelle_Markup.legacy ("Legacy feature! " ^ s));
use "General/scan.ML";
use "General/source.ML";
use "General/symbol.ML";
--- a/src/Pure/Syntax/lexicon.ML Mon Nov 28 20:39:08 2011 +0100
+++ b/src/Pure/Syntax/lexicon.ML Mon Nov 28 22:05:32 2011 +0100
@@ -189,29 +189,29 @@
(* markup *)
val token_kind_markup =
- fn Literal => Markup.literal
+ fn Literal => Isabelle_Markup.literal
| IdentSy => Markup.empty
| LongIdentSy => Markup.empty
- | VarSy => Markup.var
- | TFreeSy => Markup.tfree
- | TVarSy => Markup.tvar
- | NumSy => Markup.numeral
- | FloatSy => Markup.numeral
- | XNumSy => Markup.numeral
- | StrSy => Markup.inner_string
+ | VarSy => Isabelle_Markup.var
+ | TFreeSy => Isabelle_Markup.tfree
+ | TVarSy => Isabelle_Markup.tvar
+ | NumSy => Isabelle_Markup.numeral
+ | FloatSy => Isabelle_Markup.numeral
+ | XNumSy => Isabelle_Markup.numeral
+ | StrSy => Isabelle_Markup.inner_string
| Space => Markup.empty
- | Comment => Markup.inner_comment
+ | Comment => Isabelle_Markup.inner_comment
| EOF => Markup.empty;
fun report_of_token (Token (kind, s, (pos, _))) =
let val markup =
- if kind = Literal andalso not (is_ascii_identifier s) then Markup.delimiter
+ if kind = Literal andalso not (is_ascii_identifier s) then Isabelle_Markup.delimiter
else token_kind_markup kind
in (pos, markup) end;
fun reported_token_range ctxt tok =
if is_proper tok
- then Context_Position.reported_text ctxt (pos_of_token tok) Markup.token_range ""
+ then Context_Position.reported_text ctxt (pos_of_token tok) Isabelle_Markup.token_range ""
else "";
--- a/src/Pure/Syntax/syntax.ML Mon Nov 28 20:39:08 2011 +0100
+++ b/src/Pure/Syntax/syntax.ML Mon Nov 28 22:05:32 2011 +0100
@@ -185,7 +185,7 @@
val pos =
(case tree of
XML.Elem ((name, props), _) =>
- if name = Markup.tokenN then Position.of_properties props
+ if name = Isabelle_Markup.tokenN then Position.of_properties props
else Position.none
| XML.Text _ => Position.none);
in (Symbol_Pos.explode (text, pos), pos) end;
@@ -202,7 +202,7 @@
in
(case YXML.parse_body str handle Fail msg => error msg of
body as [tree as XML.Elem ((name, _), _)] =>
- if name = Markup.tokenN then parse_tree tree else decode body
+ if name = Isabelle_Markup.tokenN then parse_tree tree else decode body
| [tree as XML.Text _] => parse_tree tree
| body => decode body)
end;
--- a/src/Pure/Syntax/syntax_phases.ML Mon Nov 28 20:39:08 2011 +0100
+++ b/src/Pure/Syntax/syntax_phases.ML Mon Nov 28 22:05:32 2011 +0100
@@ -51,16 +51,16 @@
[Name_Space.markup (Consts.space_of (Proof_Context.consts_of ctxt)) c];
fun markup_free ctxt x =
- [if can Name.dest_skolem x then Markup.skolem else Markup.free] @
+ [if can Name.dest_skolem x then Isabelle_Markup.skolem else Isabelle_Markup.free] @
(if Variable.is_body ctxt orelse Variable.is_fixed ctxt x
then [Variable.markup_fixed ctxt x]
else []);
-fun markup_var xi = [Markup.name (Term.string_of_vname xi) Markup.var];
+fun markup_var xi = [Markup.name (Term.string_of_vname xi) Isabelle_Markup.var];
fun markup_bound def ps (name, id) =
- let val entity = Markup.entity Markup.boundN name in
- Markup.bound ::
+ let val entity = Isabelle_Markup.entity Isabelle_Markup.boundN name in
+ Isabelle_Markup.bound ::
map (fn pos => Markup.properties (Position.entity_properties_of def id pos) entity) ps
end;
@@ -284,7 +284,8 @@
val pts = Syntax.parse syn root (filter Lexicon.is_proper toks)
handle ERROR msg =>
error (msg ^
- implode (map (Markup.markup Markup.report o Lexicon.reported_token_range ctxt) toks));
+ implode
+ (map (Markup.markup Isabelle_Markup.report o Lexicon.reported_token_range ctxt) toks));
val len = length pts;
val limit = Config.get ctxt Syntax.ambiguity_limit;
@@ -320,10 +321,11 @@
fun parse_failed ctxt pos msg kind =
cat_error msg ("Failed to parse " ^ kind ^
- Markup.markup Markup.report (Context_Position.reported_text ctxt pos Markup.bad ""));
+ Markup.markup Isabelle_Markup.report
+ (Context_Position.reported_text ctxt pos Isabelle_Markup.bad ""));
fun parse_sort ctxt =
- Syntax.parse_token ctxt Term_XML.Decode.sort Markup.sort
+ Syntax.parse_token ctxt Term_XML.Decode.sort Isabelle_Markup.sort
(fn (syms, pos) =>
parse_raw ctxt "sort" (syms, pos)
|> report_result ctxt pos
@@ -332,7 +334,7 @@
handle ERROR msg => parse_failed ctxt pos msg "sort");
fun parse_typ ctxt =
- Syntax.parse_token ctxt Term_XML.Decode.typ Markup.typ
+ Syntax.parse_token ctxt Term_XML.Decode.typ Isabelle_Markup.typ
(fn (syms, pos) =>
parse_raw ctxt "type" (syms, pos)
|> report_result ctxt pos
@@ -343,8 +345,8 @@
let
val (markup, kind, root, constrain) =
if is_prop
- then (Markup.prop, "proposition", "prop", Type.constraint propT)
- else (Markup.term, "term", Config.get ctxt Syntax.root, I);
+ then (Isabelle_Markup.prop, "proposition", "prop", Type.constraint propT)
+ else (Isabelle_Markup.term, "term", Config.get ctxt Syntax.root, I);
val decode = constrain o Term_XML.Decode.term;
in
Syntax.parse_token ctxt decode markup
@@ -592,34 +594,34 @@
let
val m =
if Variable.is_fixed ctxt x orelse Syntax.is_pretty_global ctxt
- then Markup.fixed x
- else Markup.hilite;
+ then Isabelle_Markup.fixed x
+ else Isabelle_Markup.hilite;
in
if can Name.dest_skolem x
- then ([m, Markup.skolem], Variable.revert_fixed ctxt x)
- else ([m, Markup.free], x)
+ then ([m, Isabelle_Markup.skolem], Variable.revert_fixed ctxt x)
+ else ([m, Isabelle_Markup.free], x)
end;
fun var_or_skolem s =
(case Lexicon.read_variable s of
SOME (x, i) =>
(case try Name.dest_skolem x of
- NONE => (Markup.var, s)
- | SOME x' => (Markup.skolem, Term.string_of_vname (x', i)))
- | NONE => (Markup.var, s));
+ NONE => (Isabelle_Markup.var, s)
+ | SOME x' => (Isabelle_Markup.skolem, Term.string_of_vname (x', i)))
+ | NONE => (Isabelle_Markup.var, s));
fun unparse_t t_to_ast prt_t markup ctxt t =
let
val syn = Proof_Context.syn_of ctxt;
- fun token_trans "_tfree" x = SOME (Pretty.mark_str (Markup.tfree, x))
- | token_trans "_tvar" x = SOME (Pretty.mark_str (Markup.tvar, x))
+ fun token_trans "_tfree" x = SOME (Pretty.mark_str (Isabelle_Markup.tfree, x))
+ | token_trans "_tvar" x = SOME (Pretty.mark_str (Isabelle_Markup.tvar, x))
| token_trans "_free" x = SOME (Pretty.marks_str (free_or_skolem ctxt x))
- | token_trans "_bound" x = SOME (Pretty.mark_str (Markup.bound, x))
- | token_trans "_loose" x = SOME (Pretty.mark_str (Markup.malformed, x))
+ | token_trans "_bound" x = SOME (Pretty.mark_str (Isabelle_Markup.bound, x))
+ | token_trans "_loose" x = SOME (Pretty.mark_str (Isabelle_Markup.malformed, x))
| token_trans "_var" x = SOME (Pretty.mark_str (var_or_skolem x))
- | token_trans "_numeral" x = SOME (Pretty.mark_str (Markup.numeral, x))
- | token_trans "_inner_string" x = SOME (Pretty.mark_str (Markup.inner_string, x))
+ | token_trans "_numeral" x = SOME (Pretty.mark_str (Isabelle_Markup.numeral, x))
+ | token_trans "_inner_string" x = SOME (Pretty.mark_str (Isabelle_Markup.inner_string, x))
| token_trans _ _ = NONE;
fun markup_extern c =
@@ -641,8 +643,8 @@
in
-val unparse_sort = unparse_t sort_to_ast Printer.pretty_typ_ast Markup.sort;
-val unparse_typ = unparse_t typ_to_ast Printer.pretty_typ_ast Markup.typ;
+val unparse_sort = unparse_t sort_to_ast Printer.pretty_typ_ast Isabelle_Markup.sort;
+val unparse_typ = unparse_t typ_to_ast Printer.pretty_typ_ast Isabelle_Markup.typ;
fun unparse_term ctxt =
let
@@ -652,7 +654,7 @@
in
unparse_t (term_to_ast idents (is_some o Syntax.lookup_const syn))
(Printer.pretty_term_ast (not (Pure_Thy.old_appl_syntax thy)))
- Markup.term ctxt
+ Isabelle_Markup.term ctxt
end;
end;
@@ -813,7 +815,7 @@
val _ =
map2 (fn (pos, _) => fn ty =>
if Position.is_reported pos then
- Markup.markup (Position.markup pos Markup.typing)
+ Markup.markup (Position.markup pos Isabelle_Markup.typing)
(Syntax.string_of_typ ctxt (Logic.dest_type ty))
else "") ps tys'
|> implode |> Output.report
--- a/src/Pure/Syntax/term_position.ML Mon Nov 28 20:39:08 2011 +0100
+++ b/src/Pure/Syntax/term_position.ML Mon Nov 28 22:05:32 2011 +0100
@@ -25,15 +25,15 @@
val position_text = XML.Text position_dummy;
fun pretty pos =
- Pretty.markup (Position.markup pos Markup.position) [Pretty.str position_dummy];
+ Pretty.markup (Position.markup pos Isabelle_Markup.position) [Pretty.str position_dummy];
fun encode pos =
- YXML.string_of (XML.Elem (Position.markup pos Markup.position, [position_text]));
+ YXML.string_of (XML.Elem (Position.markup pos Isabelle_Markup.position, [position_text]));
fun decode str =
(case YXML.parse_body str handle Fail msg => error msg of
[XML.Elem ((name, props), [arg])] =>
- if name = Markup.positionN andalso arg = position_text
+ if name = Isabelle_Markup.positionN andalso arg = position_text
then SOME (Position.of_properties props)
else NONE
| _ => NONE);
--- a/src/Pure/System/invoke_scala.ML Mon Nov 28 20:39:08 2011 +0100
+++ b/src/Pure/System/invoke_scala.ML Mon Nov 28 22:05:32 2011 +0100
@@ -33,10 +33,10 @@
fun promise_method name arg =
let
val id = new_id ();
- fun abort () = Output.raw_message (Markup.cancel_scala id) "";
+ fun abort () = Output.raw_message (Isabelle_Markup.cancel_scala id) "";
val promise = Future.promise abort : string future;
val _ = Synchronized.change promises (Symtab.update (id, promise));
- val _ = Output.raw_message (Markup.invoke_scala name id) arg;
+ val _ = Output.raw_message (Isabelle_Markup.invoke_scala name id) arg;
in promise end;
fun method name arg = Future.join (promise_method name arg);
--- a/src/Pure/System/isabelle_process.ML Mon Nov 28 20:39:08 2011 +0100
+++ b/src/Pure/System/isabelle_process.ML Mon Nov 28 22:05:32 2011 +0100
@@ -77,7 +77,7 @@
if body = "" then ()
else
message false mbox ch
- ((case opt_serial of SOME i => cons (Markup.serialN, string_of_int i) | _ => I)
+ ((case opt_serial of SOME i => cons (Isabelle_Markup.serialN, string_of_int i) | _ => I)
(Position.properties_of (Position.thread_data ()))) body;
fun message_output mbox channel =
@@ -189,7 +189,7 @@
val _ = Keyword.status ();
val _ = Thy_Info.status ();
- val _ = Output.status (Markup.markup Markup.ready "process ready");
+ val _ = Output.status (Markup.markup Isabelle_Markup.ready "process ready");
in loop channel end));
fun init_fifos fifo1 fifo2 = init (fn () => System_Channel.fifo_rendezvous fifo1 fifo2);
--- a/src/Pure/System/isabelle_process.scala Mon Nov 28 20:39:08 2011 +0100
+++ b/src/Pure/System/isabelle_process.scala Mon Nov 28 22:05:32 2011 +0100
@@ -23,14 +23,14 @@
object Kind
{
val message_markup = Map(
- ('A' : Int) -> Markup.INIT,
- ('B' : Int) -> Markup.STATUS,
- ('C' : Int) -> Markup.REPORT,
- ('D' : Int) -> Markup.WRITELN,
- ('E' : Int) -> Markup.TRACING,
- ('F' : Int) -> Markup.WARNING,
- ('G' : Int) -> Markup.ERROR,
- ('H' : Int) -> Markup.RAW)
+ ('A' : Int) -> Isabelle_Markup.INIT,
+ ('B' : Int) -> Isabelle_Markup.STATUS,
+ ('C' : Int) -> Isabelle_Markup.REPORT,
+ ('D' : Int) -> Isabelle_Markup.WRITELN,
+ ('E' : Int) -> Isabelle_Markup.TRACING,
+ ('F' : Int) -> Isabelle_Markup.WARNING,
+ ('G' : Int) -> Isabelle_Markup.ERROR,
+ ('H' : Int) -> Isabelle_Markup.RAW)
}
sealed abstract class Message
@@ -38,9 +38,10 @@
class Input(name: String, args: List[String]) extends Message
{
override def toString: String =
- XML.Elem(Markup(Markup.PROVER_COMMAND, List((Markup.NAME, name))),
+ XML.Elem(Markup(Isabelle_Markup.PROVER_COMMAND, List((Markup.NAME, name))),
args.map(s =>
- List(XML.Text("\n"), XML.elem(Markup.PROVER_ARG, YXML.parse_body(s)))).flatten).toString
+ List(XML.Text("\n"),
+ XML.elem(Isabelle_Markup.PROVER_ARG, YXML.parse_body(s)))).flatten).toString
}
class Result(val message: XML.Elem) extends Message
@@ -49,14 +50,14 @@
def properties: Properties.T = message.markup.properties
def body: XML.Body = message.body
- def is_init = kind == Markup.INIT
- def is_exit = kind == Markup.EXIT
- def is_stdout = kind == Markup.STDOUT
- def is_stderr = kind == Markup.STDERR
- def is_system = kind == Markup.SYSTEM
- def is_status = kind == Markup.STATUS
- def is_report = kind == Markup.REPORT
- def is_raw = kind == Markup.RAW
+ def is_init = kind == Isabelle_Markup.INIT
+ def is_exit = kind == Isabelle_Markup.EXIT
+ def is_stdout = kind == Isabelle_Markup.STDOUT
+ def is_stderr = kind == Isabelle_Markup.STDERR
+ def is_system = kind == Isabelle_Markup.SYSTEM
+ def is_status = kind == Isabelle_Markup.STATUS
+ def is_report = kind == Isabelle_Markup.REPORT
+ def is_raw = kind == Isabelle_Markup.RAW
def is_ready = Isar_Document.is_ready(message)
def is_syslog = is_init || is_exit || is_system || is_ready || is_stderr
@@ -88,15 +89,15 @@
private def system_result(text: String)
{
- receiver(new Result(XML.Elem(Markup(Markup.SYSTEM, Nil), List(XML.Text(text)))))
+ receiver(new Result(XML.Elem(Markup(Isabelle_Markup.SYSTEM, Nil), List(XML.Text(text)))))
}
private val xml_cache = new XML.Cache()
private def put_result(kind: String, props: Properties.T, body: XML.Body)
{
- if (kind == Markup.INIT) system_channel.accepted()
- if (kind == Markup.RAW)
+ if (kind == Isabelle_Markup.INIT) system_channel.accepted()
+ if (kind == Isabelle_Markup.RAW)
receiver(new Result(XML.Elem(Markup(kind, props), body)))
else {
val msg = XML.Elem(Markup(kind, props), Isar_Document.clean_message(body))
@@ -172,7 +173,7 @@
system_result(startup_output)
if (startup_failed) {
- put_result(Markup.EXIT, "Return code: 127")
+ put_result(Isabelle_Markup.EXIT, "Return code: 127")
process.stdin.close
Thread.sleep(300)
terminate_process()
@@ -192,7 +193,7 @@
for ((thread, _) <- List(standard_input, stdout, stderr, command_input, message))
thread.join
system_result("process_manager terminated")
- put_result(Markup.EXIT, "Return code: " + rc.toString)
+ put_result(Isabelle_Markup.EXIT, "Return code: " + rc.toString)
}
system_channel.accepted()
}
@@ -246,8 +247,8 @@
private def raw_output_actor(err: Boolean): (Thread, Actor) =
{
val (name, reader, markup) =
- if (err) ("standard_error", process.stderr, Markup.STDERR)
- else ("standard_output", process.stdout, Markup.STDOUT)
+ if (err) ("standard_error", process.stderr, Isabelle_Markup.STDERR)
+ else ("standard_output", process.stdout, Isabelle_Markup.STDOUT)
Simple_Thread.actor(name) {
var result = new StringBuilder(100)
@@ -363,7 +364,7 @@
case List(XML.Elem(Markup(name, props), Nil))
if name.size == 1 && Kind.message_markup.isDefinedAt(name(0)) =>
val kind = Kind.message_markup(name(0))
- val body = read_chunk(kind != Markup.RAW)
+ val body = read_chunk(kind != Isabelle_Markup.RAW)
put_result(kind, props, body)
case _ =>
read_chunk(false)
--- a/src/Pure/System/session.scala Mon Nov 28 20:39:08 2011 +0100
+++ b/src/Pure/System/session.scala Mon Nov 28 22:05:32 2011 +0100
@@ -363,7 +363,7 @@
catch {
case _: Document.State.Fail => bad_result(result)
}
- case Markup.Assign_Execs if result.is_raw =>
+ case Isabelle_Markup.Assign_Execs if result.is_raw =>
XML.content(result.body).mkString match {
case Isar_Document.Assign(id, assign) =>
try { handle_assign(id, assign) }
@@ -376,20 +376,20 @@
if (!old_versions.isEmpty) prover.get.remove_versions(old_versions)
prune_next = System.currentTimeMillis() + prune_delay.ms
}
- case Markup.Removed_Versions if result.is_raw =>
+ case Isabelle_Markup.Removed_Versions if result.is_raw =>
XML.content(result.body).mkString match {
case Isar_Document.Removed(removed) =>
try { handle_removed(removed) }
catch { case _: Document.State.Fail => bad_result(result) }
case _ => bad_result(result)
}
- case Markup.Invoke_Scala(name, id) if result.is_raw =>
+ case Isabelle_Markup.Invoke_Scala(name, id) if result.is_raw =>
Future.fork {
val arg = XML.content(result.body).mkString
val (tag, res) = Invoke_Scala.method(name, arg)
prover.get.invoke_scala(id, tag, res)
}
- case Markup.Cancel_Scala(id) =>
+ case Isabelle_Markup.Cancel_Scala(id) =>
System.err.println("cancel_scala " + id) // FIXME cancel JVM task
case _ =>
if (result.is_syslog) {
--- a/src/Pure/Thy/html.ML Mon Nov 28 20:39:08 2011 +0100
+++ b/src/Pure/Thy/html.ML Mon Nov 28 22:05:32 2011 +0100
@@ -49,8 +49,8 @@
fun span class = ("<span class=" ^ quote (XML.text class) ^ ">", "</span>");
fun span_class (name, props) =
- (case Markup.get_entity_kind (name, props) of
- SOME kind => Markup.entityN ^ "_" ^ name
+ (case Isabelle_Markup.get_entity_kind (name, props) of
+ SOME kind => Isabelle_Markup.entityN ^ "_" ^ name
| NONE => name);
val _ = Markup.add_mode htmlN (span o span_class);
@@ -59,7 +59,7 @@
(* symbol output *)
local
- val hidden = span Markup.hiddenN |-> enclose;
+ val hidden = span Isabelle_Markup.hiddenN |-> enclose;
(* FIXME proper unicode -- produced on Scala side *)
val html_syms = Symtab.make
--- a/src/Pure/Thy/html.scala Mon Nov 28 20:39:08 2011 +0100
+++ b/src/Pure/Thy/html.scala Mon Nov 28 22:05:32 2011 +0100
@@ -49,7 +49,7 @@
XML.Elem(Markup(SPAN, List((STYLE, "font-family: " + font))), List(XML.Text(txt)))
def hidden(txt: String): XML.Elem =
- span(Markup.HIDDEN, List(XML.Text(txt)))
+ span(Isabelle_Markup.HIDDEN, List(XML.Text(txt)))
def sub(txt: String): XML.Elem = XML.elem("sub", List(XML.Text(txt)))
def sup(txt: String): XML.Elem = XML.elem("sup", List(XML.Text(txt)))
@@ -61,7 +61,7 @@
tree match {
case XML.Elem(m @ Markup(name, props), ts) =>
val span_class =
- m match { case Markup.Entity(kind, _) => name + "_" + kind case _ => name }
+ m match { case Isabelle_Markup.Entity(kind, _) => name + "_" + kind case _ => name }
val html_span = span(span_class, ts.flatMap(html_spans))
if (original_data) List(XML.Elem(Markup.Data, List(tree, html_span)))
else List(html_span)
--- a/src/Pure/Thy/latex.ML Mon Nov 28 20:39:08 2011 +0100
+++ b/src/Pure/Thy/latex.ML Mon Nov 28 22:05:32 2011 +0100
@@ -203,8 +203,8 @@
in (output_symbols syms, Symbol.length syms) end;
fun latex_markup (s, _) =
- if s = Markup.keywordN then ("\\isakeyword{", "}")
- else if s = Markup.commandN then ("\\isacommand{", "}")
+ if s = Isabelle_Markup.keywordN then ("\\isakeyword{", "}")
+ else if s = Isabelle_Markup.commandN then ("\\isacommand{", "}")
else Markup.no_output;
fun latex_indent "" _ = ""
--- a/src/Pure/Thy/thy_info.ML Mon Nov 28 20:39:08 2011 +0100
+++ b/src/Pure/Thy/thy_info.ML Mon Nov 28 22:05:32 2011 +0100
@@ -89,7 +89,7 @@
fun get_names () = Graph.topological_order (get_thys ());
fun status () =
- List.app (Output.status o Markup.markup_only o Markup.loaded_theory) (get_names ());
+ List.app (Output.status o Markup.markup_only o Isabelle_Markup.loaded_theory) (get_names ());
(* access thy *)
--- a/src/Pure/Thy/thy_info.scala Mon Nov 28 20:39:08 2011 +0100
+++ b/src/Pure/Thy/thy_info.scala Mon Nov 28 22:05:32 2011 +0100
@@ -14,7 +14,8 @@
object Loaded_Theory {
def unapply(msg: XML.Tree): Option[String] =
msg match {
- case XML.Elem(Markup(Markup.LOADED_THEORY, List((Markup.NAME, name))), _) => Some(name)
+ case XML.Elem(Markup(Isabelle_Markup.LOADED_THEORY, List((Markup.NAME, name))), _) =>
+ Some(name)
case _ => None
}
}
--- a/src/Pure/Thy/thy_output.ML Mon Nov 28 20:39:08 2011 +0100
+++ b/src/Pure/Thy/thy_output.ML Mon Nov 28 22:05:32 2011 +0100
@@ -81,8 +81,8 @@
(Args.src -> Toplevel.state -> Proof.context -> string) Name_Space.table *
(string -> Proof.context -> Proof.context) Name_Space.table;
val empty : T =
- (Name_Space.empty_table Markup.doc_antiquotationN,
- Name_Space.empty_table Markup.doc_antiquotation_optionN);
+ (Name_Space.empty_table Isabelle_Markup.doc_antiquotationN,
+ Name_Space.empty_table Isabelle_Markup.doc_antiquotation_optionN);
val extend = I;
fun merge ((commands1, options1), (commands2, options2)) : T =
(Name_Space.merge_tables (commands1, commands2),
--- a/src/Pure/Thy/thy_syntax.ML Mon Nov 28 20:39:08 2011 +0100
+++ b/src/Pure/Thy/thy_syntax.ML Mon Nov 28 22:05:32 2011 +0100
@@ -43,28 +43,28 @@
local
val token_kind_markup =
- fn Token.Command => Markup.command
- | Token.Keyword => Markup.keyword
+ fn Token.Command => Isabelle_Markup.command
+ | Token.Keyword => Isabelle_Markup.keyword
| Token.Ident => Markup.empty
| Token.LongIdent => Markup.empty
| Token.SymIdent => Markup.empty
- | Token.Var => Markup.var
- | Token.TypeIdent => Markup.tfree
- | Token.TypeVar => Markup.tvar
+ | Token.Var => Isabelle_Markup.var
+ | Token.TypeIdent => Isabelle_Markup.tfree
+ | Token.TypeVar => Isabelle_Markup.tvar
| Token.Nat => Markup.empty
| Token.Float => Markup.empty
- | Token.String => Markup.string
- | Token.AltString => Markup.altstring
- | Token.Verbatim => Markup.verbatim
+ | Token.String => Isabelle_Markup.string
+ | Token.AltString => Isabelle_Markup.altstring
+ | Token.Verbatim => Isabelle_Markup.verbatim
| Token.Space => Markup.empty
- | Token.Comment => Markup.comment
+ | Token.Comment => Isabelle_Markup.comment
| Token.InternalValue => Markup.empty
- | Token.Error _ => Markup.malformed
- | Token.Sync => Markup.control
- | Token.EOF => Markup.control;
+ | Token.Error _ => Isabelle_Markup.malformed
+ | Token.Sync => Isabelle_Markup.control
+ | Token.EOF => Isabelle_Markup.control;
fun token_markup tok =
- if Token.keyword_with (not o Lexicon.is_ascii_identifier) tok then Markup.operator
+ if Token.keyword_with (not o Lexicon.is_ascii_identifier) tok then Isabelle_Markup.operator
else
let
val kind = Token.kind_of tok;
@@ -75,7 +75,7 @@
in props (token_kind_markup kind) end;
fun reports_of_symbol (sym, pos) =
- if Symbol.is_malformed sym then [(pos, Markup.malformed)] else [];
+ if Symbol.is_malformed sym then [(pos, Isabelle_Markup.malformed)] else [];
in
@@ -133,9 +133,9 @@
local
-fun kind_markup (Command name) = Markup.command_span name
- | kind_markup Ignored = Markup.ignored_span
- | kind_markup Malformed = Markup.malformed_span;
+fun kind_markup (Command name) = Isabelle_Markup.command_span name
+ | kind_markup Ignored = Isabelle_Markup.ignored_span
+ | kind_markup Malformed = Isabelle_Markup.malformed_span;
in
--- a/src/Pure/build-jars Mon Nov 28 20:39:08 2011 +0100
+++ b/src/Pure/build-jars Mon Nov 28 22:05:32 2011 +0100
@@ -14,7 +14,7 @@
Concurrent/simple_thread.scala
Concurrent/volatile.scala
General/exn.scala
- General/timing.scala
+ General/isabelle_markup.scala
General/linear_set.scala
General/markup.scala
General/path.scala
@@ -24,6 +24,7 @@
General/scan.scala
General/sha1.scala
General/symbol.scala
+ General/timing.scala
Isar/keyword.scala
Isar/outer_syntax.scala
Isar/parse.scala
--- a/src/Pure/consts.ML Mon Nov 28 20:39:08 2011 +0100
+++ b/src/Pure/consts.ML Mon Nov 28 22:05:32 2011 +0100
@@ -311,7 +311,8 @@
(* empty and merge *)
-val empty = make_consts (Name_Space.empty_table Markup.constantN, Symtab.empty, Symtab.empty);
+val empty =
+ make_consts (Name_Space.empty_table Isabelle_Markup.constantN, Symtab.empty, Symtab.empty);
fun merge
(Consts {decls = decls1, constraints = constraints1, rev_abbrevs = rev_abbrevs1},
--- a/src/Pure/global_theory.ML Mon Nov 28 20:39:08 2011 +0100
+++ b/src/Pure/global_theory.ML Mon Nov 28 22:05:32 2011 +0100
@@ -108,7 +108,8 @@
NONE => error ("Unknown fact " ^ quote name ^ Position.str_of pos)
| SOME (static, ths) =>
(Context_Position.report ctxt pos (Name_Space.markup (Facts.space_of facts) name);
- if static then () else Context_Position.report ctxt pos (Markup.dynamic_fact name);
+ if static then ()
+ else Context_Position.report ctxt pos (Isabelle_Markup.dynamic_fact name);
Facts.select xthmref (map (Thm.transfer thy) ths)))
end;
--- a/src/Pure/goal_display.ML Mon Nov 28 20:39:08 2011 +0100
+++ b/src/Pure/goal_display.ML Mon Nov 28 22:05:32 2011 +0100
@@ -114,8 +114,9 @@
fun pretty_list _ _ [] = []
| pretty_list name prt lst = [Pretty.big_list name (map prt lst)];
- fun pretty_subgoal (n, A) = Pretty.markup Markup.subgoal
- [Pretty.str (" " ^ string_of_int n ^ ". "), prt_term A];
+ fun pretty_subgoal (n, A) =
+ Pretty.markup Isabelle_Markup.subgoal
+ [Pretty.str (" " ^ string_of_int n ^ ". "), prt_term A];
fun pretty_subgoals As = map pretty_subgoal (1 upto length As ~~ As);
val pretty_ffpairs = pretty_list "flex-flex pairs:" (pretty_flexpair ctxt);
--- a/src/Pure/type.ML Mon Nov 28 20:39:08 2011 +0100
+++ b/src/Pure/type.ML Mon Nov 28 22:05:32 2011 +0100
@@ -186,8 +186,8 @@
build_tsig (f (classes, default, types));
val empty_tsig =
- build_tsig ((Name_Space.empty Markup.classN, Sorts.empty_algebra), [],
- Name_Space.empty_table Markup.typeN);
+ build_tsig ((Name_Space.empty Isabelle_Markup.classN, Sorts.empty_algebra), [],
+ Name_Space.empty_table Isabelle_Markup.typeN);
(* classes and sorts *)
--- a/src/Pure/variable.ML Mon Nov 28 20:39:08 2011 +0100
+++ b/src/Pure/variable.ML Mon Nov 28 22:05:32 2011 +0100
@@ -81,7 +81,7 @@
(** local context data **)
type fixes = string Name_Space.table;
-val empty_fixes: fixes = Name_Space.empty_table Markup.fixedN;
+val empty_fixes: fixes = Name_Space.empty_table Isabelle_Markup.fixedN;
datatype data = Data of
{is_body: bool, (*inner body mode*)
--- a/src/Tools/jEdit/src/html_panel.scala Mon Nov 28 20:39:08 2011 +0100
+++ b/src/Tools/jEdit/src/html_panel.scala Mon Nov 28 22:05:32 2011 +0100
@@ -164,7 +164,8 @@
current_body.flatMap(div =>
Pretty.formatted(List(div), current_margin, Pretty.font_metric(current_font_metrics))
.map(t =>
- XML.Elem(Markup(HTML.PRE, List((HTML.CLASS, Markup.MESSAGE))), HTML.spans(t, true))))
+ XML.Elem(Markup(HTML.PRE, List((HTML.CLASS, Isabelle_Markup.MESSAGE))),
+ HTML.spans(t, true))))
val doc =
builder.parse(
new InputSourceImpl(
--- a/src/Tools/jEdit/src/isabelle_hyperlinks.scala Mon Nov 28 20:39:08 2011 +0100
+++ b/src/Tools/jEdit/src/isabelle_hyperlinks.scala Mon Nov 28 22:05:32 2011 +0100
@@ -62,10 +62,10 @@
{
// FIXME Isar_Document.Hyperlink extractor
case Text.Info(info_range,
- XML.Elem(Markup(Markup.ENTITY, props), _))
+ XML.Elem(Markup(Isabelle_Markup.ENTITY, props), _))
if (props.find(
- { case (Markup.KIND, Markup.ML_OPEN) => true
- case (Markup.KIND, Markup.ML_STRUCT) => true
+ { case (Markup.KIND, Isabelle_Markup.ML_OPEN) => true
+ case (Markup.KIND, Isabelle_Markup.ML_STRUCT) => true
case _ => false }).isEmpty) =>
val Text.Range(begin, end) = info_range
val line = buffer.getLineOfOffset(begin)
@@ -90,7 +90,7 @@
case _ => null
}
},
- Some(Set(Markup.ENTITY))))
+ Some(Set(Isabelle_Markup.ENTITY))))
markup match {
case Text.Info(_, Some(link)) #:: _ => link
case _ => null
--- a/src/Tools/jEdit/src/isabelle_rendering.scala Mon Nov 28 20:39:08 2011 +0100
+++ b/src/Tools/jEdit/src/isabelle_rendering.scala Mon Nov 28 22:05:32 2011 +0100
@@ -90,82 +90,84 @@
val message =
Markup_Tree.Select[Color](
{
- case Text.Info(_, XML.Elem(Markup(Markup.WRITELN, _), _)) => regular_color
- case Text.Info(_, XML.Elem(Markup(Markup.WARNING, _), _)) => warning_color
- case Text.Info(_, XML.Elem(Markup(Markup.ERROR, _), _)) => error_color
+ case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.WRITELN, _), _)) => regular_color
+ case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.WARNING, _), _)) => warning_color
+ case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.ERROR, _), _)) => error_color
},
- Some(Set(Markup.WRITELN, Markup.WARNING, Markup.ERROR)))
+ Some(Set(Isabelle_Markup.WRITELN, Isabelle_Markup.WARNING, Isabelle_Markup.ERROR)))
val tooltip_message =
Markup_Tree.Cumulate[SortedMap[Long, String]](SortedMap.empty,
{
- case (msgs, Text.Info(_, msg @ XML.Elem(Markup(markup, Markup.Serial(serial)), _)))
- if markup == Markup.WRITELN || markup == Markup.WARNING || markup == Markup.ERROR =>
+ case (msgs, Text.Info(_, msg @ XML.Elem(Markup(markup, Isabelle_Markup.Serial(serial)), _)))
+ if markup == Isabelle_Markup.WRITELN ||
+ markup == Isabelle_Markup.WARNING ||
+ markup == Isabelle_Markup.ERROR =>
msgs + (serial ->
Pretty.string_of(List(msg), margin = Isabelle.Int_Property("tooltip-margin")))
},
- Some(Set(Markup.WRITELN, Markup.WARNING, Markup.ERROR)))
+ Some(Set(Isabelle_Markup.WRITELN, Isabelle_Markup.WARNING, Isabelle_Markup.ERROR)))
val gutter_message =
Markup_Tree.Select[Icon](
{
- case Text.Info(_, XML.Elem(Markup(Markup.WARNING, _), body)) =>
+ case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.WARNING, _), body)) =>
body match {
- case List(XML.Elem(Markup(Markup.LEGACY, _), _)) => legacy_icon
+ case List(XML.Elem(Markup(Isabelle_Markup.LEGACY, _), _)) => legacy_icon
case _ => warning_icon
}
- case Text.Info(_, XML.Elem(Markup(Markup.ERROR, _), _)) => error_icon
+ case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.ERROR, _), _)) => error_icon
},
- Some(Set(Markup.WARNING, Markup.ERROR)))
+ Some(Set(Isabelle_Markup.WARNING, Isabelle_Markup.ERROR)))
val background1 =
Markup_Tree.Select[Color](
{
- case Text.Info(_, XML.Elem(Markup(Markup.BAD, _), _)) => bad_color
- case Text.Info(_, XML.Elem(Markup(Markup.HILITE, _), _)) => hilite_color
+ case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.BAD, _), _)) => bad_color
+ case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.HILITE, _), _)) => hilite_color
},
- Some(Set(Markup.BAD, Markup.HILITE)))
+ Some(Set(Isabelle_Markup.BAD, Isabelle_Markup.HILITE)))
val background2 =
Markup_Tree.Select[Color](
{
- case Text.Info(_, XML.Elem(Markup(Markup.TOKEN_RANGE, _), _)) => light_color
+ case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.TOKEN_RANGE, _), _)) => light_color
},
- Some(Set(Markup.TOKEN_RANGE)))
+ Some(Set(Isabelle_Markup.TOKEN_RANGE)))
val foreground =
Markup_Tree.Select[Color](
{
- case Text.Info(_, XML.Elem(Markup(Markup.STRING, _), _)) => quoted_color
- case Text.Info(_, XML.Elem(Markup(Markup.ALTSTRING, _), _)) => quoted_color
- case Text.Info(_, XML.Elem(Markup(Markup.VERBATIM, _), _)) => quoted_color
+ case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.STRING, _), _)) => quoted_color
+ case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.ALTSTRING, _), _)) => quoted_color
+ case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.VERBATIM, _), _)) => quoted_color
},
- Some(Set(Markup.STRING, Markup.ALTSTRING, Markup.VERBATIM)))
+ Some(Set(Isabelle_Markup.STRING, Isabelle_Markup.ALTSTRING, Isabelle_Markup.VERBATIM)))
private val text_colors: Map[String, Color] =
Map(
- Markup.STRING -> get_color("black"),
- Markup.ALTSTRING -> get_color("black"),
- Markup.VERBATIM -> get_color("black"),
- Markup.LITERAL -> keyword1_color,
- Markup.DELIMITER -> get_color("black"),
- Markup.TFREE -> get_color("#A020F0"),
- Markup.TVAR -> get_color("#A020F0"),
- Markup.FREE -> get_color("blue"),
- Markup.SKOLEM -> get_color("#D2691E"),
- Markup.BOUND -> get_color("green"),
- Markup.VAR -> get_color("#00009B"),
- Markup.INNER_STRING -> get_color("#D2691E"),
- Markup.INNER_COMMENT -> get_color("#8B0000"),
- Markup.DYNAMIC_FACT -> get_color("#7BA428"),
- Markup.ML_KEYWORD -> keyword1_color,
- Markup.ML_DELIMITER -> get_color("black"),
- Markup.ML_NUMERAL -> get_color("red"),
- Markup.ML_CHAR -> get_color("#D2691E"),
- Markup.ML_STRING -> get_color("#D2691E"),
- Markup.ML_COMMENT -> get_color("#8B0000"),
- Markup.ML_MALFORMED -> get_color("#FF6A6A"),
- Markup.ANTIQ -> get_color("blue"))
+ Isabelle_Markup.STRING -> get_color("black"),
+ Isabelle_Markup.ALTSTRING -> get_color("black"),
+ Isabelle_Markup.VERBATIM -> get_color("black"),
+ Isabelle_Markup.LITERAL -> keyword1_color,
+ Isabelle_Markup.DELIMITER -> get_color("black"),
+ Isabelle_Markup.TFREE -> get_color("#A020F0"),
+ Isabelle_Markup.TVAR -> get_color("#A020F0"),
+ Isabelle_Markup.FREE -> get_color("blue"),
+ Isabelle_Markup.SKOLEM -> get_color("#D2691E"),
+ Isabelle_Markup.BOUND -> get_color("green"),
+ Isabelle_Markup.VAR -> get_color("#00009B"),
+ Isabelle_Markup.INNER_STRING -> get_color("#D2691E"),
+ Isabelle_Markup.INNER_COMMENT -> get_color("#8B0000"),
+ Isabelle_Markup.DYNAMIC_FACT -> get_color("#7BA428"),
+ Isabelle_Markup.ML_KEYWORD -> keyword1_color,
+ Isabelle_Markup.ML_DELIMITER -> get_color("black"),
+ Isabelle_Markup.ML_NUMERAL -> get_color("red"),
+ Isabelle_Markup.ML_CHAR -> get_color("#D2691E"),
+ Isabelle_Markup.ML_STRING -> get_color("#D2691E"),
+ Isabelle_Markup.ML_COMMENT -> get_color("#8B0000"),
+ Isabelle_Markup.ML_MALFORMED -> get_color("#FF6A6A"),
+ Isabelle_Markup.ANTIQ -> get_color("blue"))
val text_color =
Markup_Tree.Select[Color](
@@ -177,19 +179,19 @@
private val tooltips: Map[String, String] =
Map(
- Markup.SORT -> "sort",
- Markup.TYP -> "type",
- Markup.TERM -> "term",
- Markup.PROP -> "proposition",
- Markup.TOKEN_RANGE -> "inner syntax token",
- Markup.FREE -> "free variable",
- Markup.SKOLEM -> "skolem variable",
- Markup.BOUND -> "bound variable",
- Markup.VAR -> "schematic variable",
- Markup.TFREE -> "free type variable",
- Markup.TVAR -> "schematic type variable",
- Markup.ML_SOURCE -> "ML source",
- Markup.DOC_SOURCE -> "document source")
+ Isabelle_Markup.SORT -> "sort",
+ Isabelle_Markup.TYP -> "type",
+ Isabelle_Markup.TERM -> "term",
+ Isabelle_Markup.PROP -> "proposition",
+ Isabelle_Markup.TOKEN_RANGE -> "inner syntax token",
+ Isabelle_Markup.FREE -> "free variable",
+ Isabelle_Markup.SKOLEM -> "skolem variable",
+ Isabelle_Markup.BOUND -> "bound variable",
+ Isabelle_Markup.VAR -> "schematic variable",
+ Isabelle_Markup.TFREE -> "free type variable",
+ Isabelle_Markup.TVAR -> "schematic type variable",
+ Isabelle_Markup.ML_SOURCE -> "ML source",
+ Isabelle_Markup.DOC_SOURCE -> "document source")
private def string_of_typing(kind: String, body: XML.Body): String =
Pretty.string_of(List(Pretty.block(XML.Text(kind) :: Pretty.Break(1) :: body)),
@@ -198,25 +200,28 @@
val tooltip1 =
Markup_Tree.Select[String](
{
- case Text.Info(_, XML.Elem(Markup.Entity(kind, name), _)) => kind + " " + quote(name)
- case Text.Info(_, XML.Elem(Markup(Markup.ML_TYPING, _), body)) =>
+ case Text.Info(_, XML.Elem(Isabelle_Markup.Entity(kind, name), _)) => kind + " " + quote(name)
+ case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.ML_TYPING, _), body)) =>
string_of_typing("ML:", body)
case Text.Info(_, XML.Elem(Markup(name, _), _))
if tooltips.isDefinedAt(name) => tooltips(name)
},
- Some(Set(Markup.ENTITY, Markup.ML_TYPING) ++ tooltips.keys))
+ Some(Set(Isabelle_Markup.ENTITY, Isabelle_Markup.ML_TYPING) ++ tooltips.keys))
val tooltip2 =
Markup_Tree.Select[String](
{
- case Text.Info(_, XML.Elem(Markup(Markup.TYPING, _), body)) => string_of_typing("::", body)
+ case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.TYPING, _), body)) =>
+ string_of_typing("::", body)
},
- Some(Set(Markup.TYPING)))
+ Some(Set(Isabelle_Markup.TYPING)))
private val subexp_include =
- Set(Markup.SORT, Markup.TYP, Markup.TERM, Markup.PROP, Markup.ML_TYPING, Markup.TOKEN_RANGE,
- Markup.ENTITY, Markup.TYPING, Markup.FREE, Markup.SKOLEM, Markup.BOUND, Markup.VAR,
- Markup.TFREE, Markup.TVAR, Markup.ML_SOURCE, Markup.DOC_SOURCE)
+ Set(Isabelle_Markup.SORT, Isabelle_Markup.TYP, Isabelle_Markup.TERM, Isabelle_Markup.PROP,
+ Isabelle_Markup.ML_TYPING, Isabelle_Markup.TOKEN_RANGE, Isabelle_Markup.ENTITY,
+ Isabelle_Markup.TYPING, Isabelle_Markup.FREE, Isabelle_Markup.SKOLEM, Isabelle_Markup.BOUND,
+ Isabelle_Markup.VAR, Isabelle_Markup.TFREE, Isabelle_Markup.TVAR, Isabelle_Markup.ML_SOURCE,
+ Isabelle_Markup.DOC_SOURCE)
val subexp =
Markup_Tree.Select[(Text.Range, Color)](
--- a/src/Tools/jEdit/src/output_dockable.scala Mon Nov 28 20:39:08 2011 +0100
+++ b/src/Tools/jEdit/src/output_dockable.scala Mon Nov 28 22:05:32 2011 +0100
@@ -87,7 +87,7 @@
val snapshot = doc_view.update_snapshot()
val filtered_results =
snapshot.command_state(cmd).results.iterator.map(_._2) filter {
- case XML.Elem(Markup(Markup.TRACING, _), _) => show_tracing // FIXME not scalable
+ case XML.Elem(Markup(Isabelle_Markup.TRACING, _), _) => show_tracing // FIXME not scalable
case _ => true
}
html_panel.render(filtered_results.toList)
--- a/src/Tools/quickcheck.ML Mon Nov 28 20:39:08 2011 +0100
+++ b/src/Tools/quickcheck.ML Mon Nov 28 22:05:32 2011 +0100
@@ -502,7 +502,7 @@
state
|> (if auto then
Proof.goal_message (K (Pretty.chunks [Pretty.str "",
- Pretty.mark Markup.hilite msg]))
+ Pretty.mark Isabelle_Markup.hilite msg]))
else
tap (fn _ => Output.urgent_message (Pretty.string_of msg))))
else
--- a/src/Tools/solve_direct.ML Mon Nov 28 20:39:08 2011 +0100
+++ b/src/Tools/solve_direct.ML Mon Nov 28 22:05:32 2011 +0100
@@ -89,7 +89,7 @@
Proof.goal_message
(fn () =>
Pretty.chunks
- [Pretty.str "", Pretty.markup Markup.hilite (message results)])
+ [Pretty.str "", Pretty.markup Isabelle_Markup.hilite (message results)])
else
tap (fn _ =>
Output.urgent_message (Pretty.string_of (Pretty.chunks (message results))))))