# HG changeset patch # User huffman # Date 1322543381 -3600 # Node ID 06e259492f6b26a7c3f4ce068ceac28afb739cd7 # Parent 0ea1c705eebbbe26f95270cd2dfa73f2168a1b82# Parent 546d78f0d81f2f1b5baa12309c8d685a12352633 merged diff -r 0ea1c705eebb -r 06e259492f6b src/HOL/Library/Sum_of_Squares/sos_wrapper.ML --- a/src/HOL/Library/Sum_of_Squares/sos_wrapper.ML Mon Nov 28 21:28:01 2011 +0100 +++ b/src/HOL/Library/Sum_of_Squares/sos_wrapper.ML Tue Nov 29 06:09:41 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 diff -r 0ea1c705eebb -r 06e259492f6b src/HOL/Product_Type.thy --- a/src/HOL/Product_Type.thy Mon Nov 28 21:28:01 2011 +0100 +++ b/src/HOL/Product_Type.thy Tue Nov 29 06:09:41 2011 +0100 @@ -897,6 +897,8 @@ notation (HTML output) Times (infixr "\" 80) +hide_const (open) Times + syntax "_Sigma" :: "[pttrn, 'a set, 'b set] => ('a * 'b) set" ("(3SIGMA _:_./ _)" [0, 0, 10] 10) translations diff -r 0ea1c705eebb -r 06e259492f6b src/HOL/Statespace/StateSpaceEx.thy --- a/src/HOL/Statespace/StateSpaceEx.thy Mon Nov 28 21:28:01 2011 +0100 +++ b/src/HOL/Statespace/StateSpaceEx.thy Tue Nov 29 06:09:41 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))))); *} diff -r 0ea1c705eebb -r 06e259492f6b src/HOL/Tools/ATP/atp_reconstruct.ML --- a/src/HOL/Tools/ATP/atp_reconstruct.ML Mon Nov 28 21:28:01 2011 +0100 +++ b/src/HOL/Tools/ATP/atp_reconstruct.ML Tue Nov 29 06:09:41 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 () diff -r 0ea1c705eebb -r 06e259492f6b src/HOL/Tools/Nitpick/nitpick.ML --- a/src/HOL/Tools/Nitpick/nitpick.ML Mon Nov 28 21:28:01 2011 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick.ML Tue Nov 29 06:09:41 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 () diff -r 0ea1c705eebb -r 06e259492f6b src/HOL/Tools/Sledgehammer/sledgehammer_run.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Mon Nov 28 21:28:01 2011 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Tue Nov 29 06:09:41 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 diff -r 0ea1c705eebb -r 06e259492f6b src/HOL/Tools/try_methods.ML --- a/src/HOL/Tools/try_methods.ML Mon Nov 28 21:28:01 2011 +0100 +++ b/src/HOL/Tools/try_methods.ML Tue Nov 29 06:09:41 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)))) diff -r 0ea1c705eebb -r 06e259492f6b src/Pure/Concurrent/counter.scala --- a/src/Pure/Concurrent/counter.scala Mon Nov 28 21:28:01 2011 +0100 +++ b/src/Pure/Concurrent/counter.scala Tue Nov 29 06:09:41 2011 +0100 @@ -1,4 +1,5 @@ /* Title: Pure/Concurrent/counter.scala + Module: Library Author: Makarius Synchronized counter for unique identifiers < 0. diff -r 0ea1c705eebb -r 06e259492f6b src/Pure/Concurrent/future.ML --- a/src/Pure/Concurrent/future.ML Mon Nov 28 21:28:01 2011 +0100 +++ b/src/Pure/Concurrent/future.ML Tue Nov 29 06:09:41 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; diff -r 0ea1c705eebb -r 06e259492f6b src/Pure/Concurrent/future.scala --- a/src/Pure/Concurrent/future.scala Mon Nov 28 21:28:01 2011 +0100 +++ b/src/Pure/Concurrent/future.scala Tue Nov 29 06:09:41 2011 +0100 @@ -1,4 +1,5 @@ /* Title: Pure/Concurrent/future.scala + Module: Library Author: Makarius Future values. diff -r 0ea1c705eebb -r 06e259492f6b src/Pure/Concurrent/simple_thread.scala --- a/src/Pure/Concurrent/simple_thread.scala Mon Nov 28 21:28:01 2011 +0100 +++ b/src/Pure/Concurrent/simple_thread.scala Tue Nov 29 06:09:41 2011 +0100 @@ -1,4 +1,5 @@ /* Title: Pure/Concurrent/simple_thread.scala + Module: Library Author: Makarius Simplified thread operations. diff -r 0ea1c705eebb -r 06e259492f6b src/Pure/Concurrent/volatile.scala --- a/src/Pure/Concurrent/volatile.scala Mon Nov 28 21:28:01 2011 +0100 +++ b/src/Pure/Concurrent/volatile.scala Tue Nov 29 06:09:41 2011 +0100 @@ -1,4 +1,5 @@ /* Title: Pure/Concurrent/volatile.scala + Module: Library Author: Makarius Volatile variables. diff -r 0ea1c705eebb -r 06e259492f6b src/Pure/General/antiquote.ML --- a/src/Pure/General/antiquote.ML Mon Nov 28 21:28:01 2011 +0100 +++ b/src/Pure/General/antiquote.ML Tue Nov 29 06:09:41 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 *) diff -r 0ea1c705eebb -r 06e259492f6b src/Pure/General/binding.ML --- a/src/Pure/General/binding.ML Mon Nov 28 21:28:01 2011 +0100 +++ b/src/Pure/General/binding.ML Tue Nov 29 06:09:41 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; diff -r 0ea1c705eebb -r 06e259492f6b src/Pure/General/exn.scala --- a/src/Pure/General/exn.scala Mon Nov 28 21:28:01 2011 +0100 +++ b/src/Pure/General/exn.scala Tue Nov 29 06:09:41 2011 +0100 @@ -1,4 +1,5 @@ /* Title: Pure/General/exn.scala + Module: Library Author: Makarius Support for exceptions (arbitrary throwables). diff -r 0ea1c705eebb -r 06e259492f6b src/Pure/General/isabelle_markup.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/General/isabelle_markup.ML Tue Nov 29 06:09:41 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; diff -r 0ea1c705eebb -r 06e259492f6b src/Pure/General/isabelle_markup.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/General/isabelle_markup.scala Tue Nov 29 06:09:41 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 + } + } +} + diff -r 0ea1c705eebb -r 06e259492f6b src/Pure/General/markup.ML --- a/src/Pure/General/markup.ML Mon Nov 28 21:28:01 2011 +0100 +++ b/src/Pure/General/markup.ML Tue Nov 29 06:09:41 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 **) diff -r 0ea1c705eebb -r 06e259492f6b src/Pure/General/markup.scala --- a/src/Pure/General/markup.scala Mon Nov 28 21:28:01 2011 +0100 +++ b/src/Pure/General/markup.scala Tue Nov 29 06:09:41 2011 +0100 @@ -1,7 +1,8 @@ /* Title: Pure/General/markup.scala + Module: Library Author: Makarius -Common markup elements. +Generic markup elements. */ package isabelle @@ -9,12 +10,7 @@ object Markup { - /* empty */ - - val Empty = Markup("", Nil) - - - /* misc properties */ + /* properties */ val NAME = "name" val Name = new Properties.String(NAME) @@ -23,163 +19,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 +50,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) diff -r 0ea1c705eebb -r 06e259492f6b src/Pure/General/name_space.ML --- a/src/Pure/General/name_space.ML Mon Nov 28 21:28:01 2011 +0100 +++ b/src/Pure/General/name_space.ML Tue Nov 29 06:09:41 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); diff -r 0ea1c705eebb -r 06e259492f6b src/Pure/General/path.ML --- a/src/Pure/General/path.ML Mon Nov 28 21:28:01 2011 +0100 +++ b/src/Pure/General/path.ML Tue Nov 29 06:09:41 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; diff -r 0ea1c705eebb -r 06e259492f6b src/Pure/General/position.ML --- a/src/Pure/General/position.ML Mon Nov 28 21:28:01 2011 +0100 +++ b/src/Pure/General/position.ML Tue Nov 29 06:09:41 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; diff -r 0ea1c705eebb -r 06e259492f6b src/Pure/General/position.scala --- a/src/Pure/General/position.scala Mon Nov 28 21:28:01 2011 +0100 +++ b/src/Pure/General/position.scala Tue Nov 29 06:09:41 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)) } diff -r 0ea1c705eebb -r 06e259492f6b src/Pure/General/pretty.ML --- a/src/Pure/General/pretty.ML Mon Nov 28 21:28:01 2011 +0100 +++ b/src/Pure/General/pretty.ML Tue Nov 29 06:09:41 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; diff -r 0ea1c705eebb -r 06e259492f6b src/Pure/General/pretty.scala --- a/src/Pure/General/pretty.scala Mon Nov 28 21:28:01 2011 +0100 +++ b/src/Pure/General/pretty.scala Tue Nov 29 06:09:41 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 } } diff -r 0ea1c705eebb -r 06e259492f6b src/Pure/General/properties.scala --- a/src/Pure/General/properties.scala Mon Nov 28 21:28:01 2011 +0100 +++ b/src/Pure/General/properties.scala Tue Nov 29 06:09:41 2011 +0100 @@ -1,4 +1,5 @@ /* Title: Pure/General/properties.scala + Module: Library Author: Makarius Property lists. diff -r 0ea1c705eebb -r 06e259492f6b src/Pure/General/sha1.scala --- a/src/Pure/General/sha1.scala Mon Nov 28 21:28:01 2011 +0100 +++ b/src/Pure/General/sha1.scala Tue Nov 29 06:09:41 2011 +0100 @@ -1,4 +1,5 @@ /* Title: Pure/General/sha1.scala + Module: Library Author: Makarius Digest strings according to SHA-1 (see RFC 3174). diff -r 0ea1c705eebb -r 06e259492f6b src/Pure/General/timing.scala --- a/src/Pure/General/timing.scala Mon Nov 28 21:28:01 2011 +0100 +++ b/src/Pure/General/timing.scala Tue Nov 29 06:09:41 2011 +0100 @@ -1,4 +1,5 @@ /* Title: Pure/General/timing.scala + Module: Library Author: Makarius Basic support for time measurement. @@ -6,6 +7,7 @@ package isabelle + object Time { def seconds(s: Double): Time = new Time((s * 1000.0) round) @@ -24,6 +26,21 @@ def message: String = toString + "s" } + +object Timing +{ + def timeit[A](message: String)(e: => A) = + { + val start = java.lang.System.currentTimeMillis() + val result = Exn.capture(e) + val stop = java.lang.System.currentTimeMillis() + java.lang.System.err.println( + (if (message == null || message.isEmpty) "" else message + ": ") + + Time.ms(stop - start).message + " elapsed time") + Exn.release(result) + } +} + class Timing(val elapsed: Time, val cpu: Time, val gc: Time) { def message: String = diff -r 0ea1c705eebb -r 06e259492f6b src/Pure/IsaMakefile --- a/src/Pure/IsaMakefile Mon Nov 28 21:28:01 2011 +0100 +++ b/src/Pure/IsaMakefile Tue Nov 29 06:09:41 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 \ diff -r 0ea1c705eebb -r 06e259492f6b src/Pure/Isar/isar_cmd.ML --- a/src/Pure/Isar/isar_cmd.ML Mon Nov 28 21:28:01 2011 +0100 +++ b/src/Pure/Isar/isar_cmd.ML Tue Nov 29 06:09:41 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 => diff -r 0ea1c705eebb -r 06e259492f6b src/Pure/Isar/keyword.ML --- a/src/Pure/Isar/keyword.ML Mon Nov 28 21:28:01 2011 +0100 +++ b/src/Pure/Isar/keyword.ML Tue Nov 29 06:09:41 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 () = diff -r 0ea1c705eebb -r 06e259492f6b src/Pure/Isar/keyword.scala --- a/src/Pure/Isar/keyword.scala Mon Nov 28 21:28:01 2011 +0100 +++ b/src/Pure/Isar/keyword.scala Tue Nov 29 06:09:41 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 } } diff -r 0ea1c705eebb -r 06e259492f6b src/Pure/Isar/proof.ML --- a/src/Pure/Isar/proof.ML Mon Nov 28 21:28:01 2011 +0100 +++ b/src/Pure/Isar/proof.ML Tue Nov 29 06:09:41 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) diff -r 0ea1c705eebb -r 06e259492f6b src/Pure/Isar/proof_context.ML --- a/src/Pure/Isar/proof_context.ML Mon Nov 28 21:28:01 2011 +0100 +++ b/src/Pure/Isar/proof_context.ML Tue Nov 29 06:09:41 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; diff -r 0ea1c705eebb -r 06e259492f6b src/Pure/Isar/runtime.ML --- a/src/Pure/Isar/runtime.ML Mon Nov 28 21:28:01 2011 +0100 +++ b/src/Pure/Isar/runtime.ML Tue Nov 29 06:09:41 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 diff -r 0ea1c705eebb -r 06e259492f6b src/Pure/Isar/token.ML --- a/src/Pure/Isar/token.ML Mon Nov 28 21:28:01 2011 +0100 +++ b/src/Pure/Isar/token.ML Tue Nov 29 06:09:41 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); diff -r 0ea1c705eebb -r 06e259492f6b src/Pure/Isar/toplevel.ML --- a/src/Pure/Isar/toplevel.ML Mon Nov 28 21:28:01 2011 +0100 +++ b/src/Pure/Isar/toplevel.ML Tue Nov 29 06:09:41 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 (""); diff -r 0ea1c705eebb -r 06e259492f6b src/Pure/ML/ml_compiler_polyml-5.3.ML --- a/src/Pure/ML/ml_compiler_polyml-5.3.ML Mon Nov 28 21:28:01 2011 +0100 +++ b/src/Pure/ML/ml_compiler_polyml-5.3.ML Tue Nov 29 06:09:41 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; diff -r 0ea1c705eebb -r 06e259492f6b src/Pure/ML/ml_context.ML --- a/src/Pure/ML/ml_context.ML Mon Nov 28 21:28:01 2011 +0100 +++ b/src/Pure/ML/ml_context.ML Tue Nov 29 06:09:41 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 *) diff -r 0ea1c705eebb -r 06e259492f6b src/Pure/ML/ml_lex.ML --- a/src/Pure/ML/ml_lex.ML Mon Nov 28 21:28:01 2011 +0100 +++ b/src/Pure/ML/ml_lex.ML Tue Nov 29 06:09:41 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 [] diff -r 0ea1c705eebb -r 06e259492f6b src/Pure/PIDE/command.scala --- a/src/Pure/PIDE/command.scala Mon Nov 28 21:28:01 2011 +0100 +++ b/src/Pure/PIDE/command.scala Tue Nov 29 06:09:41 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 = diff -r 0ea1c705eebb -r 06e259492f6b src/Pure/PIDE/document.ML --- a/src/Pure/PIDE/document.ML Mon Nov 28 21:28:01 2011 +0100 +++ b/src/Pure/PIDE/document.ML Tue Nov 29 06:09:41 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 diff -r 0ea1c705eebb -r 06e259492f6b src/Pure/PIDE/isar_document.ML --- a/src/Pure/PIDE/isar_document.ML Mon Nov 28 21:28:01 2011 +0100 +++ b/src/Pure/PIDE/isar_document.ML Tue Nov 29 06:09:41 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 _ = diff -r 0ea1c705eebb -r 06e259492f6b src/Pure/PIDE/isar_document.scala --- a/src/Pure/PIDE/isar_document.scala Mon Nov 28 21:28:01 2011 +0100 +++ b/src/Pure/PIDE/isar_document.scala Tue Nov 29 06:09:41 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] = { diff -r 0ea1c705eebb -r 06e259492f6b src/Pure/PIDE/markup_tree.scala --- a/src/Pure/PIDE/markup_tree.scala Mon Nov 28 21:28:01 2011 +0100 +++ b/src/Pure/PIDE/markup_tree.scala Tue Nov 29 06:09:41 2011 +0100 @@ -1,4 +1,5 @@ /* Title: Pure/PIDE/markup_tree.scala + Module: Library Author: Fabian Immler, TU Munich Author: Makarius diff -r 0ea1c705eebb -r 06e259492f6b src/Pure/PIDE/text.scala --- a/src/Pure/PIDE/text.scala Mon Nov 28 21:28:01 2011 +0100 +++ b/src/Pure/PIDE/text.scala Tue Nov 29 06:09:41 2011 +0100 @@ -1,4 +1,5 @@ /* Title: Pure/PIDE/text.scala + Module: Library Author: Fabian Immler, TU Munich Author: Makarius diff -r 0ea1c705eebb -r 06e259492f6b src/Pure/PIDE/xml.scala --- a/src/Pure/PIDE/xml.scala Mon Nov 28 21:28:01 2011 +0100 +++ b/src/Pure/PIDE/xml.scala Tue Nov 29 06:09:41 2011 +0100 @@ -1,4 +1,5 @@ /* Title: Pure/PIDE/xml.scala + Module: Library Author: Makarius Untyped XML trees and basic data representation. diff -r 0ea1c705eebb -r 06e259492f6b src/Pure/PIDE/yxml.scala --- a/src/Pure/PIDE/yxml.scala Mon Nov 28 21:28:01 2011 +0100 +++ b/src/Pure/PIDE/yxml.scala Tue Nov 29 06:09:41 2011 +0100 @@ -1,4 +1,5 @@ /* Title: Pure/PIDE/yxml.scala + Module: Library Author: Makarius Efficient text representation of XML trees. Suitable for direct @@ -118,18 +119,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) } } } diff -r 0ea1c705eebb -r 06e259492f6b src/Pure/ProofGeneral/proof_general_emacs.ML --- a/src/Pure/ProofGeneral/proof_general_emacs.ML Mon Nov 28 21:28:01 2011 +0100 +++ b/src/Pure/ProofGeneral/proof_general_emacs.ML Tue Nov 29 06:09:41 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 *) diff -r 0ea1c705eebb -r 06e259492f6b src/Pure/ProofGeneral/proof_general_pgip.ML --- a/src/Pure/ProofGeneral/proof_general_pgip.ML Mon Nov 28 21:28:01 2011 +0100 +++ b/src/Pure/ProofGeneral/proof_general_pgip.ML Tue Nov 29 06:09:41 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; diff -r 0ea1c705eebb -r 06e259492f6b src/Pure/ROOT.ML --- a/src/Pure/ROOT.ML Mon Nov 28 21:28:01 2011 +0100 +++ b/src/Pure/ROOT.ML Tue Nov 29 06:09:41 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"; diff -r 0ea1c705eebb -r 06e259492f6b src/Pure/Syntax/lexicon.ML --- a/src/Pure/Syntax/lexicon.ML Mon Nov 28 21:28:01 2011 +0100 +++ b/src/Pure/Syntax/lexicon.ML Tue Nov 29 06:09:41 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 ""; diff -r 0ea1c705eebb -r 06e259492f6b src/Pure/Syntax/syntax.ML --- a/src/Pure/Syntax/syntax.ML Mon Nov 28 21:28:01 2011 +0100 +++ b/src/Pure/Syntax/syntax.ML Tue Nov 29 06:09:41 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; diff -r 0ea1c705eebb -r 06e259492f6b src/Pure/Syntax/syntax_phases.ML --- a/src/Pure/Syntax/syntax_phases.ML Mon Nov 28 21:28:01 2011 +0100 +++ b/src/Pure/Syntax/syntax_phases.ML Tue Nov 29 06:09:41 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 diff -r 0ea1c705eebb -r 06e259492f6b src/Pure/Syntax/term_position.ML --- a/src/Pure/Syntax/term_position.ML Mon Nov 28 21:28:01 2011 +0100 +++ b/src/Pure/Syntax/term_position.ML Tue Nov 29 06:09:41 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); diff -r 0ea1c705eebb -r 06e259492f6b src/Pure/System/cygwin.scala --- a/src/Pure/System/cygwin.scala Mon Nov 28 21:28:01 2011 +0100 +++ b/src/Pure/System/cygwin.scala Tue Nov 29 06:09:41 2011 +0100 @@ -1,4 +1,5 @@ /* Title: Pure/System/cygwin.scala + Module: Library Author: Makarius Accessing the Cygwin installation. diff -r 0ea1c705eebb -r 06e259492f6b src/Pure/System/download.scala --- a/src/Pure/System/download.scala Mon Nov 28 21:28:01 2011 +0100 +++ b/src/Pure/System/download.scala Tue Nov 29 06:09:41 2011 +0100 @@ -1,4 +1,5 @@ /* Title: Pure/System/download.scala + Module: Library Author: Makarius Download URLs -- with progress monitor. diff -r 0ea1c705eebb -r 06e259492f6b src/Pure/System/event_bus.scala --- a/src/Pure/System/event_bus.scala Mon Nov 28 21:28:01 2011 +0100 +++ b/src/Pure/System/event_bus.scala Tue Nov 29 06:09:41 2011 +0100 @@ -1,4 +1,5 @@ /* Title: Pure/System/event_bus.scala + Module: Library Author: Makarius Generic event bus with multiple receiving actors. diff -r 0ea1c705eebb -r 06e259492f6b src/Pure/System/invoke_scala.ML --- a/src/Pure/System/invoke_scala.ML Mon Nov 28 21:28:01 2011 +0100 +++ b/src/Pure/System/invoke_scala.ML Tue Nov 29 06:09:41 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); diff -r 0ea1c705eebb -r 06e259492f6b src/Pure/System/isabelle_process.ML --- a/src/Pure/System/isabelle_process.ML Mon Nov 28 21:28:01 2011 +0100 +++ b/src/Pure/System/isabelle_process.ML Tue Nov 29 06:09:41 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); diff -r 0ea1c705eebb -r 06e259492f6b src/Pure/System/isabelle_process.scala --- a/src/Pure/System/isabelle_process.scala Mon Nov 28 21:28:01 2011 +0100 +++ b/src/Pure/System/isabelle_process.scala Tue Nov 29 06:09:41 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) diff -r 0ea1c705eebb -r 06e259492f6b src/Pure/System/platform.scala --- a/src/Pure/System/platform.scala Mon Nov 28 21:28:01 2011 +0100 +++ b/src/Pure/System/platform.scala Tue Nov 29 06:09:41 2011 +0100 @@ -1,4 +1,5 @@ /* Title: Pure/System/platform.scala + Module: Library Author: Makarius Raw platform identification. diff -r 0ea1c705eebb -r 06e259492f6b src/Pure/System/session.scala --- a/src/Pure/System/session.scala Mon Nov 28 21:28:01 2011 +0100 +++ b/src/Pure/System/session.scala Tue Nov 29 06:09:41 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) { diff -r 0ea1c705eebb -r 06e259492f6b src/Pure/System/standard_system.scala --- a/src/Pure/System/standard_system.scala Mon Nov 28 21:28:01 2011 +0100 +++ b/src/Pure/System/standard_system.scala Tue Nov 29 06:09:41 2011 +0100 @@ -1,4 +1,5 @@ /* Title: Pure/System/standard_system.scala + Module: Library Author: Makarius Standard system operations, with basic Cygwin/Posix compatibility. diff -r 0ea1c705eebb -r 06e259492f6b src/Pure/System/swing_thread.scala --- a/src/Pure/System/swing_thread.scala Mon Nov 28 21:28:01 2011 +0100 +++ b/src/Pure/System/swing_thread.scala Tue Nov 29 06:09:41 2011 +0100 @@ -1,4 +1,5 @@ /* Title: Pure/System/swing_thread.scala + Module: Library Author: Makarius Author: Fabian Immler, TU Munich diff -r 0ea1c705eebb -r 06e259492f6b src/Pure/Thy/html.ML --- a/src/Pure/Thy/html.ML Mon Nov 28 21:28:01 2011 +0100 +++ b/src/Pure/Thy/html.ML Tue Nov 29 06:09:41 2011 +0100 @@ -49,8 +49,8 @@ fun span class = ("", ""); 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 diff -r 0ea1c705eebb -r 06e259492f6b src/Pure/Thy/html.scala --- a/src/Pure/Thy/html.scala Mon Nov 28 21:28:01 2011 +0100 +++ b/src/Pure/Thy/html.scala Tue Nov 29 06:09:41 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) diff -r 0ea1c705eebb -r 06e259492f6b src/Pure/Thy/latex.ML --- a/src/Pure/Thy/latex.ML Mon Nov 28 21:28:01 2011 +0100 +++ b/src/Pure/Thy/latex.ML Tue Nov 29 06:09:41 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 "" _ = "" diff -r 0ea1c705eebb -r 06e259492f6b src/Pure/Thy/thy_info.ML --- a/src/Pure/Thy/thy_info.ML Mon Nov 28 21:28:01 2011 +0100 +++ b/src/Pure/Thy/thy_info.ML Tue Nov 29 06:09:41 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 *) diff -r 0ea1c705eebb -r 06e259492f6b src/Pure/Thy/thy_info.scala --- a/src/Pure/Thy/thy_info.scala Mon Nov 28 21:28:01 2011 +0100 +++ b/src/Pure/Thy/thy_info.scala Tue Nov 29 06:09:41 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 } } diff -r 0ea1c705eebb -r 06e259492f6b src/Pure/Thy/thy_output.ML --- a/src/Pure/Thy/thy_output.ML Mon Nov 28 21:28:01 2011 +0100 +++ b/src/Pure/Thy/thy_output.ML Tue Nov 29 06:09:41 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), diff -r 0ea1c705eebb -r 06e259492f6b src/Pure/Thy/thy_syntax.ML --- a/src/Pure/Thy/thy_syntax.ML Mon Nov 28 21:28:01 2011 +0100 +++ b/src/Pure/Thy/thy_syntax.ML Tue Nov 29 06:09:41 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 diff -r 0ea1c705eebb -r 06e259492f6b src/Pure/build-jars --- a/src/Pure/build-jars Mon Nov 28 21:28:01 2011 +0100 +++ b/src/Pure/build-jars Tue Nov 29 06:09:41 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 diff -r 0ea1c705eebb -r 06e259492f6b src/Pure/consts.ML --- a/src/Pure/consts.ML Mon Nov 28 21:28:01 2011 +0100 +++ b/src/Pure/consts.ML Tue Nov 29 06:09:41 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}, diff -r 0ea1c705eebb -r 06e259492f6b src/Pure/global_theory.ML --- a/src/Pure/global_theory.ML Mon Nov 28 21:28:01 2011 +0100 +++ b/src/Pure/global_theory.ML Tue Nov 29 06:09:41 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; diff -r 0ea1c705eebb -r 06e259492f6b src/Pure/goal_display.ML --- a/src/Pure/goal_display.ML Mon Nov 28 21:28:01 2011 +0100 +++ b/src/Pure/goal_display.ML Tue Nov 29 06:09:41 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); diff -r 0ea1c705eebb -r 06e259492f6b src/Pure/library.scala --- a/src/Pure/library.scala Mon Nov 28 21:28:01 2011 +0100 +++ b/src/Pure/library.scala Tue Nov 29 06:09:41 2011 +0100 @@ -1,4 +1,5 @@ /* Title: Pure/library.scala + Module: Library Author: Makarius Basic library. @@ -208,20 +209,6 @@ selection.index = 3 prototypeDisplayValue = Some("00000%") } - - - /* timing */ - - def timeit[A](message: String)(e: => A) = - { - val start = System.currentTimeMillis() - val result = Exn.capture(e) - val stop = System.currentTimeMillis() - System.err.println( - (if (message == null || message.isEmpty) "" else message + ": ") + - Time.ms(stop - start).message + " elapsed time") - Exn.release(result) - } } diff -r 0ea1c705eebb -r 06e259492f6b src/Pure/package.scala --- a/src/Pure/package.scala Mon Nov 28 21:28:01 2011 +0100 +++ b/src/Pure/package.scala Tue Nov 29 06:09:41 2011 +0100 @@ -1,4 +1,5 @@ /* Title: Pure/package.scala + Module: Library Author: Makarius Toplevel isabelle package. diff -r 0ea1c705eebb -r 06e259492f6b src/Pure/type.ML --- a/src/Pure/type.ML Mon Nov 28 21:28:01 2011 +0100 +++ b/src/Pure/type.ML Tue Nov 29 06:09:41 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 *) diff -r 0ea1c705eebb -r 06e259492f6b src/Pure/variable.ML --- a/src/Pure/variable.ML Mon Nov 28 21:28:01 2011 +0100 +++ b/src/Pure/variable.ML Tue Nov 29 06:09:41 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*) diff -r 0ea1c705eebb -r 06e259492f6b src/Tools/jEdit/lib/Tools/jedit --- a/src/Tools/jEdit/lib/Tools/jedit Mon Nov 28 21:28:01 2011 +0100 +++ b/src/Tools/jEdit/lib/Tools/jedit Tue Nov 29 06:09:41 2011 +0100 @@ -14,8 +14,8 @@ "src/html_panel.scala" "src/isabelle_encoding.scala" "src/isabelle_hyperlinks.scala" - "src/isabelle_markup.scala" "src/isabelle_options.scala" + "src/isabelle_rendering.scala" "src/isabelle_sidekick.scala" "src/jedit_thy_load.scala" "src/output_dockable.scala" diff -r 0ea1c705eebb -r 06e259492f6b src/Tools/jEdit/src/document_view.scala --- a/src/Tools/jEdit/src/document_view.scala Mon Nov 28 21:28:01 2011 +0100 +++ b/src/Tools/jEdit/src/document_view.scala Tue Nov 29 06:09:41 2011 +0100 @@ -193,7 +193,7 @@ val p = new Point(x, y); SwingUtilities.convertPointToScreen(p, text_area.getPainter) // FIXME snapshot.cumulate - snapshot.select_markup(Text.Range(offset, offset + 1))(Isabelle_Markup.popup) match { + snapshot.select_markup(Text.Range(offset, offset + 1))(Isabelle_Rendering.popup) match { case Text.Info(_, Some(msg)) #:: _ => val popup = PopupFactory.getSharedInstance().getPopup(text_area, html_panel, p.x, p.y + 60) html_panel.render_sync(List(msg)) @@ -212,7 +212,7 @@ : Option[(Text.Range, Color)] = { val offset = text_area.xyToOffset(x, y) - snapshot.select_markup(Text.Range(offset, offset + 1))(Isabelle_Markup.subexp) match { + snapshot.select_markup(Text.Range(offset, offset + 1))(Isabelle_Rendering.subexp) match { case Text.Info(_, Some((range, color))) #:: _ => Some((snapshot.convert(range), color)) case _ => None } @@ -279,12 +279,12 @@ if (control) { val tooltips = - (snapshot.select_markup(range)(Isabelle_Markup.tooltip1) match + (snapshot.select_markup(range)(Isabelle_Rendering.tooltip1) match { case Text.Info(_, Some(text)) #:: _ => List(text) case _ => Nil }) ::: - (snapshot.select_markup(range)(Isabelle_Markup.tooltip2) match + (snapshot.select_markup(range)(Isabelle_Rendering.tooltip2) match { case Text.Info(_, Some(text)) #:: _ => List(text) case _ => Nil @@ -293,7 +293,7 @@ else Isabelle.tooltip(tooltips.mkString("\n")) } else { - snapshot.cumulate_markup(range)(Isabelle_Markup.tooltip_message) match + snapshot.cumulate_markup(range)(Isabelle_Rendering.tooltip_message) match { case Text.Info(_, msgs) #:: _ if !msgs.isEmpty => Isabelle.tooltip(msgs.iterator.map(_._2).mkString("\n")) @@ -326,7 +326,7 @@ // gutter icons val icons = (for (Text.Info(_, Some(icon)) <- // FIXME snapshot.cumulate - snapshot.select_markup(line_range)(Isabelle_Markup.gutter_message).iterator) + snapshot.select_markup(line_range)(Isabelle_Rendering.gutter_message).iterator) yield icon).toList.sortWith(_ >= _) icons match { case icon :: _ => @@ -432,7 +432,7 @@ (line1, line2) <- line_range(command, start) val y = line_to_y(line1) val height = HEIGHT * (line2 - line1) - color <- Isabelle_Markup.overview_color(snapshot, command) + color <- Isabelle_Rendering.overview_color(snapshot, command) } { gfx.setColor(color) gfx.fillRect(0, y, getWidth - 1, height) diff -r 0ea1c705eebb -r 06e259492f6b src/Tools/jEdit/src/html_panel.scala --- a/src/Tools/jEdit/src/html_panel.scala Mon Nov 28 21:28:01 2011 +0100 +++ b/src/Tools/jEdit/src/html_panel.scala Tue Nov 29 06:09:41 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( diff -r 0ea1c705eebb -r 06e259492f6b src/Tools/jEdit/src/isabelle_hyperlinks.scala --- a/src/Tools/jEdit/src/isabelle_hyperlinks.scala Mon Nov 28 21:28:01 2011 +0100 +++ b/src/Tools/jEdit/src/isabelle_hyperlinks.scala Tue Nov 29 06:09:41 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 diff -r 0ea1c705eebb -r 06e259492f6b src/Tools/jEdit/src/isabelle_markup.scala --- a/src/Tools/jEdit/src/isabelle_markup.scala Mon Nov 28 21:28:01 2011 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,270 +0,0 @@ -/* Title: Tools/jEdit/src/isabelle_markup.scala - Author: Makarius - -Isabelle specific physical rendering and markup selection. -*/ - -package isabelle.jedit - - -import isabelle._ - -import java.awt.Color - -import org.lobobrowser.util.gui.ColorFactory -import org.gjt.sp.jedit.syntax.{Token => JEditToken} - -import scala.collection.immutable.SortedMap - - -object Isabelle_Markup -{ - /* physical rendering */ - - // see http://www.w3schools.com/css/css_colornames.asp - - def get_color(s: String): Color = ColorFactory.getInstance.getColor(s) - - val outdated_color = new Color(238, 227, 227) - val running_color = new Color(97, 0, 97) - val running1_color = new Color(97, 0, 97, 100) - val unprocessed_color = new Color(255, 160, 160) - val unprocessed1_color = new Color(255, 160, 160, 50) - - val light_color = new Color(240, 240, 240) - val regular_color = new Color(192, 192, 192) - val warning_color = new Color(255, 140, 0) - val error_color = new Color(178, 34, 34) - val error1_color = new Color(178, 34, 34, 50) - val bad_color = new Color(255, 106, 106, 100) - val hilite_color = new Color(255, 204, 102, 100) - - val quoted_color = new Color(139, 139, 139, 25) - val subexp_color = new Color(80, 80, 80, 50) - - val keyword1_color = get_color("#006699") - val keyword2_color = get_color("#009966") - - class Icon(val priority: Int, val icon: javax.swing.Icon) - { - def >= (that: Icon): Boolean = this.priority >= that.priority - } - val warning_icon = new Icon(1, Isabelle.load_icon("16x16/status/dialog-information.png")) - val legacy_icon = new Icon(2, Isabelle.load_icon("16x16/status/dialog-warning.png")) - val error_icon = new Icon(3, Isabelle.load_icon("16x16/status/dialog-error.png")) - - - /* command status */ - - def status_color(snapshot: Document.Snapshot, command: Command): Option[Color] = - { - val state = snapshot.command_state(command) - if (snapshot.is_outdated) Some(outdated_color) - else - Isar_Document.command_status(state.status) match { - case Isar_Document.Forked(i) if i > 0 => Some(running1_color) - case Isar_Document.Unprocessed => Some(unprocessed1_color) - case _ => None - } - } - - def overview_color(snapshot: Document.Snapshot, command: Command): Option[Color] = - { - val state = snapshot.command_state(command) - if (snapshot.is_outdated) None - else - Isar_Document.command_status(state.status) match { - case Isar_Document.Forked(i) => if (i > 0) Some(running_color) else None - case Isar_Document.Unprocessed => Some(unprocessed_color) - case Isar_Document.Failed => Some(error_color) - case Isar_Document.Finished => - if (state.results.exists(r => Isar_Document.is_error(r._2))) Some(error_color) - else if (state.results.exists(r => Isar_Document.is_warning(r._2))) Some(warning_color) - else None - } - } - - - /* markup selectors */ - - 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 - }, - Some(Set(Markup.WRITELN, Markup.WARNING, 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 => - msgs + (serial -> - Pretty.string_of(List(msg), margin = Isabelle.Int_Property("tooltip-margin"))) - }, - Some(Set(Markup.WRITELN, Markup.WARNING, Markup.ERROR))) - - val gutter_message = - Markup_Tree.Select[Icon]( - { - case Text.Info(_, XML.Elem(Markup(Markup.WARNING, _), body)) => - body match { - case List(XML.Elem(Markup(Markup.LEGACY, _), _)) => legacy_icon - case _ => warning_icon - } - case Text.Info(_, XML.Elem(Markup(Markup.ERROR, _), _)) => error_icon - }, - Some(Set(Markup.WARNING, 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 - }, - Some(Set(Markup.BAD, Markup.HILITE))) - - val background2 = - Markup_Tree.Select[Color]( - { - case Text.Info(_, XML.Elem(Markup(Markup.TOKEN_RANGE, _), _)) => light_color - }, - Some(Set(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 - }, - Some(Set(Markup.STRING, Markup.ALTSTRING, 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")) - - val text_color = - Markup_Tree.Select[Color]( - { - case Text.Info(_, XML.Elem(Markup(m, _), _)) - if text_colors.isDefinedAt(m) => text_colors(m) - }, - Some(Set() ++ text_colors.keys)) - - 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") - - private def string_of_typing(kind: String, body: XML.Body): String = - Pretty.string_of(List(Pretty.block(XML.Text(kind) :: Pretty.Break(1) :: body)), - margin = Isabelle.Int_Property("tooltip-margin")) - - 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)) => - 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)) - - val tooltip2 = - Markup_Tree.Select[String]( - { - case Text.Info(_, XML.Elem(Markup(Markup.TYPING, _), body)) => string_of_typing("::", body) - }, - Some(Set(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) - - val subexp = - Markup_Tree.Select[(Text.Range, Color)]( - { - case Text.Info(range, XML.Elem(Markup(name, _), _)) if subexp_include(name) => - (range, subexp_color) - }, - Some(subexp_include)) - - - /* token markup -- text styles */ - - private val command_style: Map[String, Byte] = - { - import JEditToken._ - Map[String, Byte]( - Keyword.THY_END -> KEYWORD2, - Keyword.THY_SCRIPT -> LABEL, - Keyword.PRF_SCRIPT -> LABEL, - Keyword.PRF_ASM -> KEYWORD3, - Keyword.PRF_ASM_GOAL -> KEYWORD3 - ).withDefaultValue(KEYWORD1) - } - - private val token_style: Map[Token.Kind.Value, Byte] = - { - import JEditToken._ - Map[Token.Kind.Value, Byte]( - Token.Kind.KEYWORD -> KEYWORD2, - Token.Kind.IDENT -> NULL, - Token.Kind.LONG_IDENT -> NULL, - Token.Kind.SYM_IDENT -> NULL, - Token.Kind.VAR -> NULL, - Token.Kind.TYPE_IDENT -> NULL, - Token.Kind.TYPE_VAR -> NULL, - Token.Kind.NAT -> NULL, - Token.Kind.FLOAT -> NULL, - Token.Kind.STRING -> LITERAL1, - Token.Kind.ALT_STRING -> LITERAL2, - Token.Kind.VERBATIM -> COMMENT3, - Token.Kind.SPACE -> NULL, - Token.Kind.COMMENT -> COMMENT1, - Token.Kind.UNPARSED -> INVALID - ).withDefaultValue(NULL) - } - - def token_markup(syntax: Outer_Syntax, token: Token): Byte = - if (token.is_command) command_style(syntax.keyword_kind(token.content).getOrElse("")) - else if (token.is_operator) JEditToken.OPERATOR - else token_style(token.kind) -} diff -r 0ea1c705eebb -r 06e259492f6b src/Tools/jEdit/src/isabelle_rendering.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/jEdit/src/isabelle_rendering.scala Tue Nov 29 06:09:41 2011 +0100 @@ -0,0 +1,275 @@ +/* Title: Tools/jEdit/src/isabelle_rendering.scala + Author: Makarius + +Isabelle specific physical rendering and markup selection. +*/ + +package isabelle.jedit + + +import isabelle._ + +import java.awt.Color + +import org.lobobrowser.util.gui.ColorFactory +import org.gjt.sp.jedit.syntax.{Token => JEditToken} + +import scala.collection.immutable.SortedMap + + +object Isabelle_Rendering +{ + /* physical rendering */ + + // see http://www.w3schools.com/css/css_colornames.asp + + def get_color(s: String): Color = ColorFactory.getInstance.getColor(s) + + val outdated_color = new Color(238, 227, 227) + val running_color = new Color(97, 0, 97) + val running1_color = new Color(97, 0, 97, 100) + val unprocessed_color = new Color(255, 160, 160) + val unprocessed1_color = new Color(255, 160, 160, 50) + + val light_color = new Color(240, 240, 240) + val regular_color = new Color(192, 192, 192) + val warning_color = new Color(255, 140, 0) + val error_color = new Color(178, 34, 34) + val error1_color = new Color(178, 34, 34, 50) + val bad_color = new Color(255, 106, 106, 100) + val hilite_color = new Color(255, 204, 102, 100) + + val quoted_color = new Color(139, 139, 139, 25) + val subexp_color = new Color(80, 80, 80, 50) + + val keyword1_color = get_color("#006699") + val keyword2_color = get_color("#009966") + + class Icon(val priority: Int, val icon: javax.swing.Icon) + { + def >= (that: Icon): Boolean = this.priority >= that.priority + } + val warning_icon = new Icon(1, Isabelle.load_icon("16x16/status/dialog-information.png")) + val legacy_icon = new Icon(2, Isabelle.load_icon("16x16/status/dialog-warning.png")) + val error_icon = new Icon(3, Isabelle.load_icon("16x16/status/dialog-error.png")) + + + /* command status */ + + def status_color(snapshot: Document.Snapshot, command: Command): Option[Color] = + { + val state = snapshot.command_state(command) + if (snapshot.is_outdated) Some(outdated_color) + else + Isar_Document.command_status(state.status) match { + case Isar_Document.Forked(i) if i > 0 => Some(running1_color) + case Isar_Document.Unprocessed => Some(unprocessed1_color) + case _ => None + } + } + + def overview_color(snapshot: Document.Snapshot, command: Command): Option[Color] = + { + val state = snapshot.command_state(command) + if (snapshot.is_outdated) None + else + Isar_Document.command_status(state.status) match { + case Isar_Document.Forked(i) => if (i > 0) Some(running_color) else None + case Isar_Document.Unprocessed => Some(unprocessed_color) + case Isar_Document.Failed => Some(error_color) + case Isar_Document.Finished => + if (state.results.exists(r => Isar_Document.is_error(r._2))) Some(error_color) + else if (state.results.exists(r => Isar_Document.is_warning(r._2))) Some(warning_color) + else None + } + } + + + /* markup selectors */ + + val message = + Markup_Tree.Select[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(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, 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(Isabelle_Markup.WRITELN, Isabelle_Markup.WARNING, Isabelle_Markup.ERROR))) + + val gutter_message = + Markup_Tree.Select[Icon]( + { + case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.WARNING, _), body)) => + body match { + case List(XML.Elem(Markup(Isabelle_Markup.LEGACY, _), _)) => legacy_icon + case _ => warning_icon + } + case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.ERROR, _), _)) => error_icon + }, + Some(Set(Isabelle_Markup.WARNING, Isabelle_Markup.ERROR))) + + val background1 = + Markup_Tree.Select[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(Isabelle_Markup.BAD, Isabelle_Markup.HILITE))) + + val background2 = + Markup_Tree.Select[Color]( + { + case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.TOKEN_RANGE, _), _)) => light_color + }, + Some(Set(Isabelle_Markup.TOKEN_RANGE))) + + val foreground = + Markup_Tree.Select[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(Isabelle_Markup.STRING, Isabelle_Markup.ALTSTRING, Isabelle_Markup.VERBATIM))) + + private val text_colors: Map[String, Color] = + Map( + 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]( + { + case Text.Info(_, XML.Elem(Markup(m, _), _)) + if text_colors.isDefinedAt(m) => text_colors(m) + }, + Some(Set() ++ text_colors.keys)) + + private val tooltips: Map[String, String] = + Map( + 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)), + margin = Isabelle.Int_Property("tooltip-margin")) + + val tooltip1 = + Markup_Tree.Select[String]( + { + 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(Isabelle_Markup.ENTITY, Isabelle_Markup.ML_TYPING) ++ tooltips.keys)) + + val tooltip2 = + Markup_Tree.Select[String]( + { + case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.TYPING, _), body)) => + string_of_typing("::", body) + }, + Some(Set(Isabelle_Markup.TYPING))) + + private val subexp_include = + 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)]( + { + case Text.Info(range, XML.Elem(Markup(name, _), _)) if subexp_include(name) => + (range, subexp_color) + }, + Some(subexp_include)) + + + /* token markup -- text styles */ + + private val command_style: Map[String, Byte] = + { + import JEditToken._ + Map[String, Byte]( + Keyword.THY_END -> KEYWORD2, + Keyword.THY_SCRIPT -> LABEL, + Keyword.PRF_SCRIPT -> LABEL, + Keyword.PRF_ASM -> KEYWORD3, + Keyword.PRF_ASM_GOAL -> KEYWORD3 + ).withDefaultValue(KEYWORD1) + } + + private val token_style: Map[Token.Kind.Value, Byte] = + { + import JEditToken._ + Map[Token.Kind.Value, Byte]( + Token.Kind.KEYWORD -> KEYWORD2, + Token.Kind.IDENT -> NULL, + Token.Kind.LONG_IDENT -> NULL, + Token.Kind.SYM_IDENT -> NULL, + Token.Kind.VAR -> NULL, + Token.Kind.TYPE_IDENT -> NULL, + Token.Kind.TYPE_VAR -> NULL, + Token.Kind.NAT -> NULL, + Token.Kind.FLOAT -> NULL, + Token.Kind.STRING -> LITERAL1, + Token.Kind.ALT_STRING -> LITERAL2, + Token.Kind.VERBATIM -> COMMENT3, + Token.Kind.SPACE -> NULL, + Token.Kind.COMMENT -> COMMENT1, + Token.Kind.UNPARSED -> INVALID + ).withDefaultValue(NULL) + } + + def token_markup(syntax: Outer_Syntax, token: Token): Byte = + if (token.is_command) command_style(syntax.keyword_kind(token.content).getOrElse("")) + else if (token.is_operator) JEditToken.OPERATOR + else token_style(token.kind) +} diff -r 0ea1c705eebb -r 06e259492f6b src/Tools/jEdit/src/output_dockable.scala --- a/src/Tools/jEdit/src/output_dockable.scala Mon Nov 28 21:28:01 2011 +0100 +++ b/src/Tools/jEdit/src/output_dockable.scala Tue Nov 29 06:09:41 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) diff -r 0ea1c705eebb -r 06e259492f6b src/Tools/jEdit/src/session_dockable.scala --- a/src/Tools/jEdit/src/session_dockable.scala Mon Nov 28 21:28:01 2011 +0100 +++ b/src/Tools/jEdit/src/session_dockable.scala Tue Nov 29 06:09:41 2011 +0100 @@ -114,9 +114,9 @@ var end = size.width - insets.right for { (n, color) <- List( - (st.unprocessed, Isabelle_Markup.unprocessed1_color), - (st.running, Isabelle_Markup.running_color), - (st.failed, Isabelle_Markup.error_color)) } + (st.unprocessed, Isabelle_Rendering.unprocessed1_color), + (st.running, Isabelle_Rendering.running_color), + (st.failed, Isabelle_Rendering.error_color)) } { gfx.setColor(color) val v = (n * w / st.total) max (if (n > 0) 2 else 0) diff -r 0ea1c705eebb -r 06e259492f6b src/Tools/jEdit/src/text_area_painter.scala --- a/src/Tools/jEdit/src/text_area_painter.scala Mon Nov 28 21:28:01 2011 +0100 +++ b/src/Tools/jEdit/src/text_area_painter.scala Tue Nov 29 06:09:41 2011 +0100 @@ -95,7 +95,7 @@ if !command.is_ignored range <- line_range.try_restrict(snapshot.convert(command.range + command_start)) r <- Isabelle.gfx_range(text_area, range) - color <- Isabelle_Markup.status_color(snapshot, command) + color <- Isabelle_Rendering.status_color(snapshot, command) } { gfx.setColor(color) gfx.fillRect(r.x, y + i * line_height, r.length, line_height) @@ -104,7 +104,7 @@ // background color (1): markup for { Text.Info(range, Some(color)) <- - snapshot.select_markup(line_range)(Isabelle_Markup.background1).iterator + snapshot.select_markup(line_range)(Isabelle_Rendering.background1).iterator r <- Isabelle.gfx_range(text_area, range) } { gfx.setColor(color) @@ -114,7 +114,7 @@ // background color (2): markup for { Text.Info(range, Some(color)) <- - snapshot.select_markup(line_range)(Isabelle_Markup.background2).iterator + snapshot.select_markup(line_range)(Isabelle_Rendering.background2).iterator r <- Isabelle.gfx_range(text_area, range) } { gfx.setColor(color) @@ -124,7 +124,7 @@ // squiggly underline for { Text.Info(range, Some(color)) <- - snapshot.select_markup(line_range)(Isabelle_Markup.message).iterator + snapshot.select_markup(line_range)(Isabelle_Rendering.message).iterator r <- Isabelle.gfx_range(text_area, range) } { gfx.setColor(color) @@ -215,7 +215,7 @@ val markup = for { - r1 <- painter_snapshot.select_markup(chunk_range)(Isabelle_Markup.text_color) + r1 <- painter_snapshot.select_markup(chunk_range)(Isabelle_Rendering.text_color) r2 <- r1.try_restrict(chunk_range) } yield r2 @@ -317,7 +317,7 @@ // foreground color for { Text.Info(range, Some(color)) <- - snapshot.select_markup(line_range)(Isabelle_Markup.foreground).iterator + snapshot.select_markup(line_range)(Isabelle_Rendering.foreground).iterator r <- Isabelle.gfx_range(text_area, range) } { gfx.setColor(color) diff -r 0ea1c705eebb -r 06e259492f6b src/Tools/jEdit/src/token_markup.scala --- a/src/Tools/jEdit/src/token_markup.scala Mon Nov 28 21:28:01 2011 +0100 +++ b/src/Tools/jEdit/src/token_markup.scala Tue Nov 29 06:09:41 2011 +0100 @@ -178,7 +178,7 @@ if (line_ctxt.isDefined && Isabelle.session.is_ready) { val syntax = Isabelle.session.current_syntax() val (tokens, ctxt1) = syntax.scan_context(line, line_ctxt.get) - val styled_tokens = tokens.map(tok => (Isabelle_Markup.token_markup(syntax, tok), tok)) + val styled_tokens = tokens.map(tok => (Isabelle_Rendering.token_markup(syntax, tok), tok)) (styled_tokens, new Line_Context(Some(ctxt1))) } else { diff -r 0ea1c705eebb -r 06e259492f6b src/Tools/quickcheck.ML --- a/src/Tools/quickcheck.ML Mon Nov 28 21:28:01 2011 +0100 +++ b/src/Tools/quickcheck.ML Tue Nov 29 06:09:41 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 diff -r 0ea1c705eebb -r 06e259492f6b src/Tools/solve_direct.ML --- a/src/Tools/solve_direct.ML Mon Nov 28 21:28:01 2011 +0100 +++ b/src/Tools/solve_direct.ML Tue Nov 29 06:09:41 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))))))