--- a/src/Pure/General/isabelle_markup.ML Tue Nov 29 06:09:41 2011 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,310 +0,0 @@
-(* 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;
--- a/src/Pure/General/isabelle_markup.scala Tue Nov 29 06:09:41 2011 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,260 +0,0 @@
-/* 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 Tue Nov 29 06:09:41 2011 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,111 +0,0 @@
-(* Title: Pure/General/markup.ML
- Author: Makarius
-
-Generic markup elements.
-*)
-
-signature MARKUP =
-sig
- val parse_int: string -> int
- val print_int: int -> string
- type T = string * Properties.T
- val empty: T
- val is_empty: T -> bool
- val properties: Properties.T -> T -> T
- val nameN: string
- val name: string -> T -> T
- val kindN: string
- val elapsedN: string
- val cpuN: string
- val gcN: string
- val timingN: string val timing: Timing.timing -> 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
- val output: T -> Output.output * Output.output
- val enclose: T -> Output.output -> Output.output
- val markup: T -> string -> string
- val markup_only: T -> string
-end;
-
-structure Markup: MARKUP =
-struct
-
-(** markup elements **)
-
-(* integers *)
-
-fun parse_int s =
- let val i = Int.fromString s in
- if is_none i orelse String.isPrefix "~" s
- then raise Fail ("Bad integer: " ^ quote s)
- else the i
- end;
-
-val print_int = signed_string_of_int;
-
-
-(* basic markup *)
-
-type T = string * Properties.T;
-
-val empty = ("", []);
-
-fun is_empty ("", _) = true
- | is_empty _ = false;
-
-
-fun properties more_props ((elem, props): T) =
- (elem, fold_rev Properties.put more_props props);
-
-
-(* misc properties *)
-
-val nameN = "name";
-fun name a = properties [(nameN, a)];
-
-val kindN = "kind";
-
-
-(* timing *)
-
-val timingN = "timing";
-val elapsedN = "elapsed";
-val cpuN = "cpu";
-val gcN = "gc";
-
-fun timing {elapsed, cpu, gc} =
- (timingN,
- [(elapsedN, Time.toString elapsed),
- (cpuN, Time.toString cpu),
- (gcN, Time.toString gc)]);
-
-
-
-(** print mode operations **)
-
-val no_output = ("", "");
-fun default_output (_: T) = no_output;
-
-local
- val default = {output = default_output};
- val modes = Synchronized.var "Markup.modes" (Symtab.make [("", default)]);
-in
- fun add_mode name output =
- Synchronized.change modes (Symtab.update_new (name, {output = output}));
- fun get_mode () =
- the_default default
- (Library.get_first (Symtab.lookup (Synchronized.value modes)) (print_mode_value ()));
-end;
-
-fun output m = if is_empty m then no_output else #output (get_mode ()) m;
-
-val enclose = output #-> Library.enclose;
-
-fun markup m =
- let val (bg, en) = output m
- in Library.enclose (Output.escape bg) (Output.escape en) end;
-
-fun markup_only m = markup m "";
-
-end;
--- a/src/Pure/General/markup.scala Tue Nov 29 06:09:41 2011 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,57 +0,0 @@
-/* Title: Pure/General/markup.scala
- Module: Library
- Author: Makarius
-
-Generic markup elements.
-*/
-
-package isabelle
-
-
-object Markup
-{
- /* properties */
-
- val NAME = "name"
- val Name = new Properties.String(NAME)
-
- val KIND = "kind"
- val Kind = new Properties.String(KIND)
-
-
- /* elements */
-
- val Empty = Markup("", Nil)
- val Data = Markup("data", Nil)
- val Broken = Markup("broken", Nil)
-
-
- /* timing */
-
- val TIMING = "timing"
- val ELAPSED = "elapsed"
- val CPU = "cpu"
- val GC = "gc"
-
- object Timing
- {
- def apply(timing: isabelle.Timing): Markup =
- Markup(TIMING, List(
- (ELAPSED, Properties.Value.Double(timing.elapsed.seconds)),
- (CPU, Properties.Value.Double(timing.cpu.seconds)),
- (GC, Properties.Value.Double(timing.gc.seconds))))
- def unapply(markup: Markup): Option[isabelle.Timing] =
- markup match {
- case Markup(TIMING, List(
- (ELAPSED, Properties.Value.Double(elapsed)),
- (CPU, Properties.Value.Double(cpu)),
- (GC, Properties.Value.Double(gc)))) =>
- Some(new isabelle.Timing(Time.seconds(elapsed), Time.seconds(cpu), Time.seconds(gc)))
- case _ => None
- }
- }
-}
-
-
-sealed case class Markup(name: String, properties: Properties.T)
-
--- a/src/Pure/IsaMakefile Tue Nov 29 06:09:41 2011 +0100
+++ b/src/Pure/IsaMakefile Tue Nov 29 19:49:36 2011 +0100
@@ -80,10 +80,8 @@
General/graph.ML \
General/heap.ML \
General/integer.ML \
- General/isabelle_markup.ML \
General/linear_set.ML \
General/long_name.ML \
- General/markup.ML \
General/name_space.ML \
General/ord_list.ML \
General/output.ML \
@@ -156,7 +154,9 @@
ML/ml_syntax.ML \
ML/ml_thms.ML \
PIDE/document.ML \
+ PIDE/isabelle_markup.ML \
PIDE/isar_document.ML \
+ PIDE/markup.ML \
PIDE/xml.ML \
PIDE/yxml.ML \
Proof/extraction.ML \
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/PIDE/isabelle_markup.ML Tue Nov 29 19:49:36 2011 +0100
@@ -0,0 +1,310 @@
+(* Title: Pure/PIDE/isabelle_markup.ML
+ Author: Makarius
+
+Isabelle markup elements.
+*)
+
+signature ISABELLE_MARKUP =
+sig
+ val bindingN: string val binding: Markup.T
+ val entityN: string val entity: string -> string -> Markup.T
+ val get_entity_kind: Markup.T -> string option
+ val defN: string
+ val refN: string
+ val lineN: string
+ val offsetN: string
+ val end_offsetN: string
+ val fileN: string
+ val idN: string
+ val position_properties': string list
+ val position_properties: string list
+ val positionN: string val position: Markup.T
+ val pathN: string val path: string -> Markup.T
+ val indentN: string
+ val blockN: string val block: int -> Markup.T
+ val widthN: string
+ val breakN: string val break: int -> Markup.T
+ val fbreakN: string val fbreak: Markup.T
+ val hiddenN: string val hidden: Markup.T
+ val 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/PIDE/isabelle_markup.scala Tue Nov 29 19:49:36 2011 +0100
@@ -0,0 +1,260 @@
+/* Title: Pure/PIDE/isabelle_markup.scala
+ Author: Makarius
+
+Isabelle markup elements.
+*/
+
+package isabelle
+
+
+object Isabelle_Markup
+{
+ /* formal entities */
+
+ val BINDING = "binding"
+ val ENTITY = "entity"
+ val DEF = "def"
+ val REF = "ref"
+
+ object Entity
+ {
+ def unapply(markup: Markup): Option[(String, String)] =
+ markup match {
+ case Markup(ENTITY, props @ Markup.Kind(kind)) =>
+ props match {
+ case Markup.Name(name) => Some(kind, name)
+ case _ => None
+ }
+ case _ => None
+ }
+ }
+
+
+ /* position */
+
+ val LINE = "line"
+ val OFFSET = "offset"
+ val END_OFFSET = "end_offset"
+ val FILE = "file"
+ val ID = "id"
+
+ val DEF_LINE = "def_line"
+ val DEF_OFFSET = "def_offset"
+ val DEF_END_OFFSET = "def_end_offset"
+ val DEF_FILE = "def_file"
+ val DEF_ID = "def_id"
+
+ val POSITION_PROPERTIES = Set(LINE, OFFSET, END_OFFSET, FILE, ID)
+ val POSITION = "position"
+
+
+ /* path */
+
+ val PATH = "path"
+
+ object Path
+ {
+ def unapply(markup: Markup): Option[String] =
+ markup match {
+ case Markup(PATH, Markup.Name(name)) => Some(name)
+ case _ => None
+ }
+ }
+
+
+ /* pretty printing */
+
+ val Indent = new Properties.Int("indent")
+ val BLOCK = "block"
+ val Width = new Properties.Int("width")
+ val BREAK = "break"
+
+
+ /* 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
+ }
+ }
+}
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/PIDE/markup.ML Tue Nov 29 19:49:36 2011 +0100
@@ -0,0 +1,111 @@
+(* Title: Pure/PIDE/markup.ML
+ Author: Makarius
+
+Generic markup elements.
+*)
+
+signature MARKUP =
+sig
+ val parse_int: string -> int
+ val print_int: int -> string
+ type T = string * Properties.T
+ val empty: T
+ val is_empty: T -> bool
+ val properties: Properties.T -> T -> T
+ val nameN: string
+ val name: string -> T -> T
+ val kindN: string
+ val elapsedN: string
+ val cpuN: string
+ val gcN: string
+ val timingN: string val timing: Timing.timing -> 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
+ val output: T -> Output.output * Output.output
+ val enclose: T -> Output.output -> Output.output
+ val markup: T -> string -> string
+ val markup_only: T -> string
+end;
+
+structure Markup: MARKUP =
+struct
+
+(** markup elements **)
+
+(* integers *)
+
+fun parse_int s =
+ let val i = Int.fromString s in
+ if is_none i orelse String.isPrefix "~" s
+ then raise Fail ("Bad integer: " ^ quote s)
+ else the i
+ end;
+
+val print_int = signed_string_of_int;
+
+
+(* basic markup *)
+
+type T = string * Properties.T;
+
+val empty = ("", []);
+
+fun is_empty ("", _) = true
+ | is_empty _ = false;
+
+
+fun properties more_props ((elem, props): T) =
+ (elem, fold_rev Properties.put more_props props);
+
+
+(* misc properties *)
+
+val nameN = "name";
+fun name a = properties [(nameN, a)];
+
+val kindN = "kind";
+
+
+(* timing *)
+
+val timingN = "timing";
+val elapsedN = "elapsed";
+val cpuN = "cpu";
+val gcN = "gc";
+
+fun timing {elapsed, cpu, gc} =
+ (timingN,
+ [(elapsedN, Time.toString elapsed),
+ (cpuN, Time.toString cpu),
+ (gcN, Time.toString gc)]);
+
+
+
+(** print mode operations **)
+
+val no_output = ("", "");
+fun default_output (_: T) = no_output;
+
+local
+ val default = {output = default_output};
+ val modes = Synchronized.var "Markup.modes" (Symtab.make [("", default)]);
+in
+ fun add_mode name output =
+ Synchronized.change modes (Symtab.update_new (name, {output = output}));
+ fun get_mode () =
+ the_default default
+ (Library.get_first (Symtab.lookup (Synchronized.value modes)) (print_mode_value ()));
+end;
+
+fun output m = if is_empty m then no_output else #output (get_mode ()) m;
+
+val enclose = output #-> Library.enclose;
+
+fun markup m =
+ let val (bg, en) = output m
+ in Library.enclose (Output.escape bg) (Output.escape en) end;
+
+fun markup_only m = markup m "";
+
+end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/PIDE/markup.scala Tue Nov 29 19:49:36 2011 +0100
@@ -0,0 +1,57 @@
+/* Title: Pure/PIDE/markup.scala
+ Module: Library
+ Author: Makarius
+
+Generic markup elements.
+*/
+
+package isabelle
+
+
+object Markup
+{
+ /* properties */
+
+ val NAME = "name"
+ val Name = new Properties.String(NAME)
+
+ val KIND = "kind"
+ val Kind = new Properties.String(KIND)
+
+
+ /* elements */
+
+ val Empty = Markup("", Nil)
+ val Data = Markup("data", Nil)
+ val Broken = Markup("broken", Nil)
+
+
+ /* timing */
+
+ val TIMING = "timing"
+ val ELAPSED = "elapsed"
+ val CPU = "cpu"
+ val GC = "gc"
+
+ object Timing
+ {
+ def apply(timing: isabelle.Timing): Markup =
+ Markup(TIMING, List(
+ (ELAPSED, Properties.Value.Double(timing.elapsed.seconds)),
+ (CPU, Properties.Value.Double(timing.cpu.seconds)),
+ (GC, Properties.Value.Double(timing.gc.seconds))))
+ def unapply(markup: Markup): Option[isabelle.Timing] =
+ markup match {
+ case Markup(TIMING, List(
+ (ELAPSED, Properties.Value.Double(elapsed)),
+ (CPU, Properties.Value.Double(cpu)),
+ (GC, Properties.Value.Double(gc)))) =>
+ Some(new isabelle.Timing(Time.seconds(elapsed), Time.seconds(cpu), Time.seconds(gc)))
+ case _ => None
+ }
+ }
+}
+
+
+sealed case class Markup(name: String, properties: Properties.T)
+
--- a/src/Pure/ROOT.ML Tue Nov 29 06:09:41 2011 +0100
+++ b/src/Pure/ROOT.ML Tue Nov 29 19:49:36 2011 +0100
@@ -30,8 +30,8 @@
use "General/properties.ML";
use "General/output.ML";
use "General/timing.ML";
-use "General/markup.ML";
-use "General/isabelle_markup.ML";
+use "PIDE/markup.ML";
+use "PIDE/isabelle_markup.ML";
fun legacy_feature s = warning (Markup.markup Isabelle_Markup.legacy ("Legacy feature! " ^ s));
use "General/scan.ML";
use "General/source.ML";
--- a/src/Pure/build-jars Tue Nov 29 06:09:41 2011 +0100
+++ b/src/Pure/build-jars Tue Nov 29 19:49:36 2011 +0100
@@ -14,9 +14,7 @@
Concurrent/simple_thread.scala
Concurrent/volatile.scala
General/exn.scala
- General/isabelle_markup.scala
General/linear_set.scala
- General/markup.scala
General/path.scala
General/position.scala
General/pretty.scala
@@ -32,7 +30,9 @@
PIDE/blob.scala
PIDE/command.scala
PIDE/document.scala
+ PIDE/isabelle_markup.scala
PIDE/isar_document.scala
+ PIDE/markup.scala
PIDE/markup_tree.scala
PIDE/text.scala
PIDE/xml.scala