# HG changeset patch # User wenzelm # Date 1322592576 -3600 # Node ID b84170538043afe6c1010a9f7d429aae3e9a7e8a # Parent 06e259492f6b26a7c3f4ce068ceac28afb739cd7 rearranged files; diff -r 06e259492f6b -r b84170538043 src/Pure/General/isabelle_markup.ML --- 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; diff -r 06e259492f6b -r b84170538043 src/Pure/General/isabelle_markup.scala --- 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 - } - } -} - diff -r 06e259492f6b -r b84170538043 src/Pure/General/markup.ML --- 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; diff -r 06e259492f6b -r b84170538043 src/Pure/General/markup.scala --- 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) - diff -r 06e259492f6b -r b84170538043 src/Pure/IsaMakefile --- 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 \ diff -r 06e259492f6b -r b84170538043 src/Pure/PIDE/isabelle_markup.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; diff -r 06e259492f6b -r b84170538043 src/Pure/PIDE/isabelle_markup.scala --- /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 + } + } +} + diff -r 06e259492f6b -r b84170538043 src/Pure/PIDE/markup.ML --- /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; diff -r 06e259492f6b -r b84170538043 src/Pure/PIDE/markup.scala --- /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) + diff -r 06e259492f6b -r b84170538043 src/Pure/ROOT.ML --- 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"; diff -r 06e259492f6b -r b84170538043 src/Pure/build-jars --- 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