--- a/src/HOL/Unix/Unix.thy Tue Nov 29 15:52:51 2011 +0100
+++ b/src/HOL/Unix/Unix.thy Tue Nov 29 21:50:00 2011 +0100
@@ -450,7 +450,7 @@
with root' show ?thesis by cases auto
next
case readdir
- with root' show ?thesis by cases fastforce+
+ with root' show ?thesis by cases blast+
qed
text {*
@@ -1028,7 +1028,7 @@
also have "\<dots> \<noteq> None"
proof -
from ys obtain us u where rev_ys: "ys = us @ [u]"
- by (cases ys rule: rev_cases) fastforce+
+ by (cases ys rule: rev_cases) simp
with tr path
have "lookup root ((path @ [y]) @ (us @ [u])) \<noteq> None \<or>
lookup root ((path @ [y]) @ us) \<noteq> None"
--- a/src/Pure/Concurrent/counter.scala Tue Nov 29 15:52:51 2011 +0100
+++ b/src/Pure/Concurrent/counter.scala Tue Nov 29 21:50:00 2011 +0100
@@ -1,5 +1,5 @@
/* Title: Pure/Concurrent/counter.scala
- Module: Library
+ Module: PIDE
Author: Makarius
Synchronized counter for unique identifiers < 0.
--- a/src/Pure/Concurrent/future.scala Tue Nov 29 15:52:51 2011 +0100
+++ b/src/Pure/Concurrent/future.scala Tue Nov 29 21:50:00 2011 +0100
@@ -1,5 +1,5 @@
/* Title: Pure/Concurrent/future.scala
- Module: Library
+ Module: PIDE
Author: Makarius
Future values.
--- a/src/Pure/Concurrent/simple_thread.scala Tue Nov 29 15:52:51 2011 +0100
+++ b/src/Pure/Concurrent/simple_thread.scala Tue Nov 29 21:50:00 2011 +0100
@@ -1,5 +1,5 @@
/* Title: Pure/Concurrent/simple_thread.scala
- Module: Library
+ Module: PIDE
Author: Makarius
Simplified thread operations.
--- a/src/Pure/Concurrent/volatile.scala Tue Nov 29 15:52:51 2011 +0100
+++ b/src/Pure/Concurrent/volatile.scala Tue Nov 29 21:50:00 2011 +0100
@@ -1,5 +1,5 @@
/* Title: Pure/Concurrent/volatile.scala
- Module: Library
+ Module: PIDE
Author: Makarius
Volatile variables.
--- a/src/Pure/General/exn.scala Tue Nov 29 15:52:51 2011 +0100
+++ b/src/Pure/General/exn.scala Tue Nov 29 21:50:00 2011 +0100
@@ -1,5 +1,5 @@
/* Title: Pure/General/exn.scala
- Module: Library
+ Module: PIDE
Author: Makarius
Support for exceptions (arbitrary throwables).
--- a/src/Pure/General/isabelle_markup.ML Tue Nov 29 15:52:51 2011 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,310 +0,0 @@
-(* Title: Pure/General/isabelle_markup.ML
- Author: Makarius
-
-Isabelle markup elements.
-*)
-
-signature ISABELLE_MARKUP =
-sig
- val bindingN: string val binding: Markup.T
- val entityN: string val entity: string -> string -> Markup.T
- val get_entity_kind: Markup.T -> string option
- val defN: string
- val refN: string
- val lineN: string
- val offsetN: string
- val end_offsetN: string
- val fileN: string
- val idN: string
- val position_properties': string list
- val position_properties: string list
- val positionN: string val position: Markup.T
- val pathN: string val path: string -> Markup.T
- val indentN: string
- val blockN: string val block: int -> Markup.T
- val widthN: string
- val breakN: string val break: int -> Markup.T
- val fbreakN: string val fbreak: Markup.T
- val hiddenN: string val hidden: Markup.T
- val classN: string
- val typeN: string
- val constantN: string
- val fixedN: string val fixed: string -> Markup.T
- val dynamic_factN: string val dynamic_fact: string -> Markup.T
- val tfreeN: string val tfree: Markup.T
- val tvarN: string val tvar: Markup.T
- val freeN: string val free: Markup.T
- val skolemN: string val skolem: Markup.T
- val boundN: string val bound: Markup.T
- val varN: string val var: Markup.T
- val numeralN: string val numeral: Markup.T
- val literalN: string val literal: Markup.T
- val delimiterN: string val delimiter: Markup.T
- val inner_stringN: string val inner_string: Markup.T
- val inner_commentN: string val inner_comment: Markup.T
- val token_rangeN: string val token_range: Markup.T
- val sortN: string val sort: Markup.T
- val typN: string val typ: Markup.T
- val termN: string val term: Markup.T
- val propN: string val prop: Markup.T
- val typingN: string val typing: Markup.T
- val ML_keywordN: string val ML_keyword: Markup.T
- val ML_delimiterN: string val ML_delimiter: Markup.T
- val ML_tvarN: string val ML_tvar: Markup.T
- val ML_numeralN: string val ML_numeral: Markup.T
- val ML_charN: string val ML_char: Markup.T
- val ML_stringN: string val ML_string: Markup.T
- val ML_commentN: string val ML_comment: Markup.T
- val ML_malformedN: string val ML_malformed: Markup.T
- val ML_defN: string
- val ML_openN: string
- val ML_structN: string
- val ML_typingN: string val ML_typing: Markup.T
- val ML_sourceN: string val ML_source: Markup.T
- val doc_sourceN: string val doc_source: Markup.T
- val antiqN: string val antiq: Markup.T
- val ML_antiquotationN: string
- val doc_antiquotationN: string
- val doc_antiquotation_optionN: string
- val keyword_declN: string val keyword_decl: string -> Markup.T
- val command_declN: string val command_decl: string -> string -> Markup.T
- val keywordN: string val keyword: Markup.T
- val operatorN: string val operator: Markup.T
- val commandN: string val command: Markup.T
- val stringN: string val string: Markup.T
- val altstringN: string val altstring: Markup.T
- val verbatimN: string val verbatim: Markup.T
- val commentN: string val comment: Markup.T
- val controlN: string val control: Markup.T
- val malformedN: string val malformed: Markup.T
- val tokenN: string val token: Properties.T -> Markup.T
- val command_spanN: string val command_span: string -> Markup.T
- val ignored_spanN: string val ignored_span: Markup.T
- val malformed_spanN: string val malformed_span: Markup.T
- val loaded_theoryN: string val loaded_theory: string -> Markup.T
- val subgoalsN: string
- val proof_stateN: string val proof_state: int -> Markup.T
- val stateN: string val state: Markup.T
- val subgoalN: string val subgoal: Markup.T
- val sendbackN: string val sendback: Markup.T
- val hiliteN: string val hilite: Markup.T
- val taskN: string
- val forkedN: string val forked: Markup.T
- val joinedN: string val joined: Markup.T
- val failedN: string val failed: Markup.T
- val finishedN: string val finished: Markup.T
- val serialN: string
- val legacyN: string val legacy: Markup.T
- val promptN: string val prompt: Markup.T
- val readyN: string val ready: Markup.T
- val reportN: string val report: Markup.T
- val no_reportN: string val no_report: Markup.T
- val badN: string val bad: Markup.T
- val functionN: string
- val assign_execs: Properties.T
- val removed_versions: Properties.T
- val invoke_scala: string -> string -> Properties.T
- val cancel_scala: string -> Properties.T
-end;
-
-structure Isabelle_Markup: ISABELLE_MARKUP =
-struct
-
-(** markup elements **)
-
-fun markup_elem elem = (elem, (elem, []): Markup.T);
-fun markup_string elem prop = (elem, fn s => (elem, [(prop, s)]): Markup.T);
-fun markup_int elem prop = (elem, fn i => (elem, [(prop, Markup.print_int i)]): Markup.T);
-
-
-(* formal entities *)
-
-val (bindingN, binding) = markup_elem "binding";
-
-val entityN = "entity";
-fun entity kind name = (entityN, [(Markup.nameN, name), (Markup.kindN, kind)]);
-
-fun get_entity_kind (name, props) =
- if name = entityN then AList.lookup (op =) props Markup.kindN
- else NONE;
-
-val defN = "def";
-val refN = "ref";
-
-
-(* position *)
-
-val lineN = "line";
-val offsetN = "offset";
-val end_offsetN = "end_offset";
-val fileN = "file";
-val idN = "id";
-
-val position_properties' = [fileN, idN];
-val position_properties = [lineN, offsetN, end_offsetN] @ position_properties';
-
-val (positionN, position) = markup_elem "position";
-
-
-(* path *)
-
-val (pathN, path) = markup_string "path" Markup.nameN;
-
-
-(* pretty printing *)
-
-val indentN = "indent";
-val (blockN, block) = markup_int "block" indentN;
-
-val widthN = "width";
-val (breakN, break) = markup_int "break" widthN;
-
-val (fbreakN, fbreak) = markup_elem "fbreak";
-
-
-(* hidden text *)
-
-val (hiddenN, hidden) = markup_elem "hidden";
-
-
-(* logical entities *)
-
-val classN = "class";
-val typeN = "type";
-val constantN = "constant";
-
-val (fixedN, fixed) = markup_string "fixed" Markup.nameN;
-val (dynamic_factN, dynamic_fact) = markup_string "dynamic_fact" Markup.nameN;
-
-
-(* inner syntax *)
-
-val (tfreeN, tfree) = markup_elem "tfree";
-val (tvarN, tvar) = markup_elem "tvar";
-val (freeN, free) = markup_elem "free";
-val (skolemN, skolem) = markup_elem "skolem";
-val (boundN, bound) = markup_elem "bound";
-val (varN, var) = markup_elem "var";
-val (numeralN, numeral) = markup_elem "numeral";
-val (literalN, literal) = markup_elem "literal";
-val (delimiterN, delimiter) = markup_elem "delimiter";
-val (inner_stringN, inner_string) = markup_elem "inner_string";
-val (inner_commentN, inner_comment) = markup_elem "inner_comment";
-
-val (token_rangeN, token_range) = markup_elem "token_range";
-
-val (sortN, sort) = markup_elem "sort";
-val (typN, typ) = markup_elem "typ";
-val (termN, term) = markup_elem "term";
-val (propN, prop) = markup_elem "prop";
-
-val (typingN, typing) = markup_elem "typing";
-
-
-(* ML syntax *)
-
-val (ML_keywordN, ML_keyword) = markup_elem "ML_keyword";
-val (ML_delimiterN, ML_delimiter) = markup_elem "ML_delimiter";
-val (ML_tvarN, ML_tvar) = markup_elem "ML_tvar";
-val (ML_numeralN, ML_numeral) = markup_elem "ML_numeral";
-val (ML_charN, ML_char) = markup_elem "ML_char";
-val (ML_stringN, ML_string) = markup_elem "ML_string";
-val (ML_commentN, ML_comment) = markup_elem "ML_comment";
-val (ML_malformedN, ML_malformed) = markup_elem "ML_malformed";
-
-val ML_defN = "ML_def";
-val ML_openN = "ML_open";
-val ML_structN = "ML_struct";
-val (ML_typingN, ML_typing) = markup_elem "ML_typing";
-
-
-(* embedded source text *)
-
-val (ML_sourceN, ML_source) = markup_elem "ML_source";
-val (doc_sourceN, doc_source) = markup_elem "doc_source";
-
-val (antiqN, antiq) = markup_elem "antiq";
-val ML_antiquotationN = "ML antiquotation";
-val doc_antiquotationN = "document antiquotation";
-val doc_antiquotation_optionN = "document antiquotation option";
-
-
-(* outer syntax *)
-
-val (keyword_declN, keyword_decl) = markup_string "keyword_decl" Markup.nameN;
-
-val command_declN = "command_decl";
-
-fun command_decl name kind : Markup.T =
- (command_declN, [(Markup.nameN, name), (Markup.kindN, kind)]);
-
-val (keywordN, keyword) = markup_elem "keyword";
-val (operatorN, operator) = markup_elem "operator";
-val (commandN, command) = markup_elem "command";
-val (stringN, string) = markup_elem "string";
-val (altstringN, altstring) = markup_elem "altstring";
-val (verbatimN, verbatim) = markup_elem "verbatim";
-val (commentN, comment) = markup_elem "comment";
-val (controlN, control) = markup_elem "control";
-val (malformedN, malformed) = markup_elem "malformed";
-
-val tokenN = "token";
-fun token props = (tokenN, props);
-
-val (command_spanN, command_span) = markup_string "command_span" Markup.nameN;
-val (ignored_spanN, ignored_span) = markup_elem "ignored_span";
-val (malformed_spanN, malformed_span) = markup_elem "malformed_span";
-
-
-(* theory loader *)
-
-val (loaded_theoryN, loaded_theory) = markup_string "loaded_theory" Markup.nameN;
-
-
-(* toplevel *)
-
-val subgoalsN = "subgoals";
-val (proof_stateN, proof_state) = markup_int "proof_state" subgoalsN;
-
-val (stateN, state) = markup_elem "state";
-val (subgoalN, subgoal) = markup_elem "subgoal";
-val (sendbackN, sendback) = markup_elem "sendback";
-val (hiliteN, hilite) = markup_elem "hilite";
-
-
-(* command status *)
-
-val taskN = "task";
-
-val (forkedN, forked) = markup_elem "forked";
-val (joinedN, joined) = markup_elem "joined";
-
-val (failedN, failed) = markup_elem "failed";
-val (finishedN, finished) = markup_elem "finished";
-
-
-(* messages *)
-
-val serialN = "serial";
-
-val (legacyN, legacy) = markup_elem "legacy";
-val (promptN, prompt) = markup_elem "prompt";
-val (readyN, ready) = markup_elem "ready";
-
-val (reportN, report) = markup_elem "report";
-val (no_reportN, no_report) = markup_elem "no_report";
-
-val (badN, bad) = markup_elem "bad";
-
-
-(* raw message functions *)
-
-val functionN = "function"
-
-val assign_execs = [(functionN, "assign_execs")];
-val removed_versions = [(functionN, "removed_versions")];
-
-fun invoke_scala name id = [(functionN, "invoke_scala"), (Markup.nameN, name), (idN, id)];
-fun cancel_scala id = [(functionN, "cancel_scala"), (idN, id)];
-
-end;
--- a/src/Pure/General/isabelle_markup.scala Tue Nov 29 15:52:51 2011 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,260 +0,0 @@
-/* Title: Pure/General/isabelle_markup.scala
- Author: Makarius
-
-Isabelle markup elements.
-*/
-
-package isabelle
-
-
-object Isabelle_Markup
-{
- /* formal entities */
-
- val BINDING = "binding"
- val ENTITY = "entity"
- val DEF = "def"
- val REF = "ref"
-
- object Entity
- {
- def unapply(markup: Markup): Option[(String, String)] =
- markup match {
- case Markup(ENTITY, props @ Markup.Kind(kind)) =>
- props match {
- case Markup.Name(name) => Some(kind, name)
- case _ => None
- }
- case _ => None
- }
- }
-
-
- /* position */
-
- val LINE = "line"
- val OFFSET = "offset"
- val END_OFFSET = "end_offset"
- val FILE = "file"
- val ID = "id"
-
- val DEF_LINE = "def_line"
- val DEF_OFFSET = "def_offset"
- val DEF_END_OFFSET = "def_end_offset"
- val DEF_FILE = "def_file"
- val DEF_ID = "def_id"
-
- val POSITION_PROPERTIES = Set(LINE, OFFSET, END_OFFSET, FILE, ID)
- val POSITION = "position"
-
-
- /* path */
-
- val PATH = "path"
-
- object Path
- {
- def unapply(markup: Markup): Option[String] =
- markup match {
- case Markup(PATH, Markup.Name(name)) => Some(name)
- case _ => None
- }
- }
-
-
- /* pretty printing */
-
- val Indent = new Properties.Int("indent")
- val BLOCK = "block"
- val Width = new Properties.Int("width")
- val BREAK = "break"
-
-
- /* hidden text */
-
- val HIDDEN = "hidden"
-
-
- /* logical entities */
-
- val CLASS = "class"
- val TYPE = "type"
- val FIXED = "fixed"
- val CONSTANT = "constant"
-
- val DYNAMIC_FACT = "dynamic_fact"
-
-
- /* inner syntax */
-
- val TFREE = "tfree"
- val TVAR = "tvar"
- val FREE = "free"
- val SKOLEM = "skolem"
- val BOUND = "bound"
- val VAR = "var"
- val NUM = "num"
- val FLOAT = "float"
- val XNUM = "xnum"
- val XSTR = "xstr"
- val LITERAL = "literal"
- val DELIMITER = "delimiter"
- val INNER_STRING = "inner_string"
- val INNER_COMMENT = "inner_comment"
-
- val TOKEN_RANGE = "token_range"
-
- val SORT = "sort"
- val TYP = "typ"
- val TERM = "term"
- val PROP = "prop"
-
- val TYPING = "typing"
-
- val ATTRIBUTE = "attribute"
- val METHOD = "method"
-
-
- /* embedded source text */
-
- val ML_SOURCE = "ML_source"
- val DOC_SOURCE = "doc_source"
-
- val ANTIQ = "antiq"
- val ML_ANTIQUOTATION = "ML antiquotation"
- val DOCUMENT_ANTIQUOTATION = "document antiquotation"
- val DOCUMENT_ANTIQUOTATION_OPTION = "document antiquotation option"
-
-
- /* ML syntax */
-
- val ML_KEYWORD = "ML_keyword"
- val ML_DELIMITER = "ML_delimiter"
- val ML_TVAR = "ML_tvar"
- val ML_NUMERAL = "ML_numeral"
- val ML_CHAR = "ML_char"
- val ML_STRING = "ML_string"
- val ML_COMMENT = "ML_comment"
- val ML_MALFORMED = "ML_malformed"
-
- val ML_DEF = "ML_def"
- val ML_OPEN = "ML_open"
- val ML_STRUCT = "ML_struct"
- val ML_TYPING = "ML_typing"
-
-
- /* outer syntax */
-
- val KEYWORD_DECL = "keyword_decl"
- val COMMAND_DECL = "command_decl"
-
- val KEYWORD = "keyword"
- val OPERATOR = "operator"
- val COMMAND = "command"
- val STRING = "string"
- val ALTSTRING = "altstring"
- val VERBATIM = "verbatim"
- val COMMENT = "comment"
- val CONTROL = "control"
- val MALFORMED = "malformed"
-
- val COMMAND_SPAN = "command_span"
- val IGNORED_SPAN = "ignored_span"
- val MALFORMED_SPAN = "malformed_span"
-
-
- /* theory loader */
-
- val LOADED_THEORY = "loaded_theory"
-
-
- /* toplevel */
-
- val SUBGOALS = "subgoals"
- val PROOF_STATE = "proof_state"
-
- val STATE = "state"
- val SUBGOAL = "subgoal"
- val SENDBACK = "sendback"
- val HILITE = "hilite"
-
-
- /* command status */
-
- val TASK = "task"
-
- val FORKED = "forked"
- val JOINED = "joined"
- val FAILED = "failed"
- val FINISHED = "finished"
-
-
- /* interactive documents */
-
- val VERSION = "version"
- val ASSIGN = "assign"
-
-
- /* prover process */
-
- val PROVER_COMMAND = "prover_command"
- val PROVER_ARG = "prover_arg"
-
-
- /* messages */
-
- val Serial = new Properties.Long("serial")
-
- val MESSAGE = "message"
-
- val INIT = "init"
- val STATUS = "status"
- val REPORT = "report"
- val WRITELN = "writeln"
- val TRACING = "tracing"
- val WARNING = "warning"
- val ERROR = "error"
- val RAW = "raw"
- val SYSTEM = "system"
- val STDOUT = "stdout"
- val STDERR = "stderr"
- val EXIT = "exit"
-
- val LEGACY = "legacy"
-
- val NO_REPORT = "no_report"
-
- val BAD = "bad"
-
- val READY = "ready"
-
-
- /* raw message functions */
-
- val FUNCTION = "function"
- val Function = new Properties.String(FUNCTION)
-
- val Assign_Execs: Properties.T = List((FUNCTION, "assign_execs"))
- val Removed_Versions: Properties.T = List((FUNCTION, "removed_versions"))
-
- val INVOKE_SCALA = "invoke_scala"
- object Invoke_Scala
- {
- def unapply(props: Properties.T): Option[(String, String)] =
- props match {
- case List((FUNCTION, INVOKE_SCALA), (Markup.NAME, name), (ID, id)) => Some((name, id))
- case _ => None
- }
- }
-
- val CANCEL_SCALA = "cancel_scala"
- object Cancel_Scala
- {
- def unapply(props: Properties.T): Option[String] =
- props match {
- case List((FUNCTION, CANCEL_SCALA), (ID, id)) => Some(id)
- case _ => None
- }
- }
-}
-
--- a/src/Pure/General/markup.ML Tue Nov 29 15:52:51 2011 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,111 +0,0 @@
-(* Title: Pure/General/markup.ML
- Author: Makarius
-
-Generic markup elements.
-*)
-
-signature MARKUP =
-sig
- val parse_int: string -> int
- val print_int: int -> string
- type T = string * Properties.T
- val empty: T
- val is_empty: T -> bool
- val properties: Properties.T -> T -> T
- val nameN: string
- val name: string -> T -> T
- val kindN: string
- val elapsedN: string
- val cpuN: string
- val gcN: string
- val timingN: string val timing: Timing.timing -> T
- val no_output: Output.output * Output.output
- val default_output: T -> Output.output * Output.output
- val add_mode: string -> (T -> Output.output * Output.output) -> unit
- val output: T -> Output.output * Output.output
- val enclose: T -> Output.output -> Output.output
- val markup: T -> string -> string
- val markup_only: T -> string
-end;
-
-structure Markup: MARKUP =
-struct
-
-(** markup elements **)
-
-(* integers *)
-
-fun parse_int s =
- let val i = Int.fromString s in
- if is_none i orelse String.isPrefix "~" s
- then raise Fail ("Bad integer: " ^ quote s)
- else the i
- end;
-
-val print_int = signed_string_of_int;
-
-
-(* basic markup *)
-
-type T = string * Properties.T;
-
-val empty = ("", []);
-
-fun is_empty ("", _) = true
- | is_empty _ = false;
-
-
-fun properties more_props ((elem, props): T) =
- (elem, fold_rev Properties.put more_props props);
-
-
-(* misc properties *)
-
-val nameN = "name";
-fun name a = properties [(nameN, a)];
-
-val kindN = "kind";
-
-
-(* timing *)
-
-val timingN = "timing";
-val elapsedN = "elapsed";
-val cpuN = "cpu";
-val gcN = "gc";
-
-fun timing {elapsed, cpu, gc} =
- (timingN,
- [(elapsedN, Time.toString elapsed),
- (cpuN, Time.toString cpu),
- (gcN, Time.toString gc)]);
-
-
-
-(** print mode operations **)
-
-val no_output = ("", "");
-fun default_output (_: T) = no_output;
-
-local
- val default = {output = default_output};
- val modes = Synchronized.var "Markup.modes" (Symtab.make [("", default)]);
-in
- fun add_mode name output =
- Synchronized.change modes (Symtab.update_new (name, {output = output}));
- fun get_mode () =
- the_default default
- (Library.get_first (Symtab.lookup (Synchronized.value modes)) (print_mode_value ()));
-end;
-
-fun output m = if is_empty m then no_output else #output (get_mode ()) m;
-
-val enclose = output #-> Library.enclose;
-
-fun markup m =
- let val (bg, en) = output m
- in Library.enclose (Output.escape bg) (Output.escape en) end;
-
-fun markup_only m = markup m "";
-
-end;
--- a/src/Pure/General/markup.scala Tue Nov 29 15:52:51 2011 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,57 +0,0 @@
-/* Title: Pure/General/markup.scala
- Module: Library
- Author: Makarius
-
-Generic markup elements.
-*/
-
-package isabelle
-
-
-object Markup
-{
- /* properties */
-
- val NAME = "name"
- val Name = new Properties.String(NAME)
-
- val KIND = "kind"
- val Kind = new Properties.String(KIND)
-
-
- /* elements */
-
- val Empty = Markup("", Nil)
- val Data = Markup("data", Nil)
- val Broken = Markup("broken", Nil)
-
-
- /* timing */
-
- val TIMING = "timing"
- val ELAPSED = "elapsed"
- val CPU = "cpu"
- val GC = "gc"
-
- object Timing
- {
- def apply(timing: isabelle.Timing): Markup =
- Markup(TIMING, List(
- (ELAPSED, Properties.Value.Double(timing.elapsed.seconds)),
- (CPU, Properties.Value.Double(timing.cpu.seconds)),
- (GC, Properties.Value.Double(timing.gc.seconds))))
- def unapply(markup: Markup): Option[isabelle.Timing] =
- markup match {
- case Markup(TIMING, List(
- (ELAPSED, Properties.Value.Double(elapsed)),
- (CPU, Properties.Value.Double(cpu)),
- (GC, Properties.Value.Double(gc)))) =>
- Some(new isabelle.Timing(Time.seconds(elapsed), Time.seconds(cpu), Time.seconds(gc)))
- case _ => None
- }
- }
-}
-
-
-sealed case class Markup(name: String, properties: Properties.T)
-
--- a/src/Pure/General/properties.scala Tue Nov 29 15:52:51 2011 +0100
+++ b/src/Pure/General/properties.scala Tue Nov 29 21:50:00 2011 +0100
@@ -1,5 +1,5 @@
/* Title: Pure/General/properties.scala
- Module: Library
+ Module: PIDE
Author: Makarius
Property lists.
--- a/src/Pure/General/sha1.scala Tue Nov 29 15:52:51 2011 +0100
+++ b/src/Pure/General/sha1.scala Tue Nov 29 21:50:00 2011 +0100
@@ -1,5 +1,5 @@
/* Title: Pure/General/sha1.scala
- Module: Library
+ Module: PIDE
Author: Makarius
Digest strings according to SHA-1 (see RFC 3174).
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/time.scala Tue Nov 29 21:50:00 2011 +0100
@@ -0,0 +1,28 @@
+/* Title: Pure/General/time.scala
+ Module: PIDE
+ Author: Makarius
+
+Time based on milliseconds.
+*/
+
+package isabelle
+
+
+object Time
+{
+ def seconds(s: Double): Time = new Time((s * 1000.0) round)
+ def ms(m: Long): Time = new Time(m)
+}
+
+class Time private(val ms: Long)
+{
+ def seconds: Double = ms / 1000.0
+
+ def min(t: Time): Time = if (ms < t.ms) this else t
+ def max(t: Time): Time = if (ms > t.ms) this else t
+
+ override def toString =
+ String.format(java.util.Locale.ROOT, "%.3f", seconds.asInstanceOf[AnyRef])
+ def message: String = toString + "s"
+}
+
--- a/src/Pure/General/timing.scala Tue Nov 29 15:52:51 2011 +0100
+++ b/src/Pure/General/timing.scala Tue Nov 29 21:50:00 2011 +0100
@@ -1,5 +1,4 @@
/* Title: Pure/General/timing.scala
- Module: Library
Author: Makarius
Basic support for time measurement.
@@ -8,25 +7,6 @@
package isabelle
-object Time
-{
- def seconds(s: Double): Time = new Time((s * 1000.0) round)
- def ms(m: Long): Time = new Time(m)
-}
-
-class Time private(val ms: Long)
-{
- def seconds: Double = ms / 1000.0
-
- def min(t: Time): Time = if (ms < t.ms) this else t
- def max(t: Time): Time = if (ms > t.ms) this else t
-
- override def toString =
- String.format(java.util.Locale.ROOT, "%.3f", seconds.asInstanceOf[AnyRef])
- def message: String = toString + "s"
-}
-
-
object Timing
{
def timeit[A](message: String)(e: => A) =
--- a/src/Pure/IsaMakefile Tue Nov 29 15:52:51 2011 +0100
+++ b/src/Pure/IsaMakefile Tue Nov 29 21:50:00 2011 +0100
@@ -80,10 +80,8 @@
General/graph.ML \
General/heap.ML \
General/integer.ML \
- General/isabelle_markup.ML \
General/linear_set.ML \
General/long_name.ML \
- General/markup.ML \
General/name_space.ML \
General/ord_list.ML \
General/output.ML \
@@ -156,7 +154,9 @@
ML/ml_syntax.ML \
ML/ml_thms.ML \
PIDE/document.ML \
- PIDE/isar_document.ML \
+ PIDE/isabelle_document.ML \
+ PIDE/isabelle_markup.ML \
+ PIDE/markup.ML \
PIDE/xml.ML \
PIDE/yxml.ML \
Proof/extraction.ML \
--- a/src/Pure/PIDE/command.scala Tue Nov 29 15:52:51 2011 +0100
+++ b/src/Pure/PIDE/command.scala Tue Nov 29 21:50:00 2011 +0100
@@ -66,11 +66,11 @@
val result = XML.Elem(Markup(name, Position.purge(atts)), body)
val st0 = add_result(i, result)
val st1 =
- if (Isar_Document.is_tracing(message)) st0
+ if (Isabelle_Document.is_tracing(message)) st0
else
- (st0 /: Isar_Document.message_positions(command, message))(
+ (st0 /: Isabelle_Document.message_positions(command, message))(
(st, range) => st.add_markup(Text.Info(range, result)))
- val st2 = (st1 /: Isar_Document.message_reports(message))(_ accumulate _)
+ val st2 = (st1 /: Isabelle_Document.message_reports(message))(_ accumulate _)
st2
case _ => System.err.println("Ignored message without serial number: " + message); this
}
--- a/src/Pure/PIDE/document.ML Tue Nov 29 15:52:51 2011 +0100
+++ b/src/Pure/PIDE/document.ML Tue Nov 29 21:50:00 2011 +0100
@@ -308,7 +308,7 @@
local
fun timing tr t =
- if Timing.is_relevant t then Toplevel.status tr (Markup.timing t) else ();
+ if Timing.is_relevant t then Toplevel.status tr (Isabelle_Markup.timing t) else ();
fun proof_status tr st =
(case try Toplevel.proof_of st of
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/PIDE/isabelle_document.ML Tue Nov 29 21:50:00 2011 +0100
@@ -0,0 +1,84 @@
+(* Title: Pure/PIDE/isabelle_document.ML
+ Author: Makarius
+
+Protocol message formats for interactive Isar documents.
+*)
+
+structure Isabelle_Document: sig end =
+struct
+
+val _ =
+ Isabelle_Process.add_command "Isabelle_Document.define_command"
+ (fn [id, name, text] =>
+ Document.change_state (Document.define_command (Document.parse_id id) name text));
+
+val _ =
+ Isabelle_Process.add_command "Isabelle_Document.cancel_execution"
+ (fn [] => ignore (Document.cancel_execution (Document.state ())));
+
+val _ =
+ Isabelle_Process.add_command "Isabelle_Document.update_perspective"
+ (fn [old_id_string, new_id_string, name, ids_yxml] => Document.change_state (fn state =>
+ let
+ val old_id = Document.parse_id old_id_string;
+ val new_id = Document.parse_id new_id_string;
+ val ids = YXML.parse_body ids_yxml
+ |> let open XML.Decode in list int end;
+
+ val _ = Future.join_tasks (Document.cancel_execution state);
+ in
+ state
+ |> Document.update_perspective old_id new_id name ids
+ |> Document.execute new_id
+ end));
+
+val _ =
+ Isabelle_Process.add_command "Isabelle_Document.update"
+ (fn [old_id_string, new_id_string, edits_yxml] => Document.change_state (fn state =>
+ let
+ val old_id = Document.parse_id old_id_string;
+ val new_id = Document.parse_id new_id_string;
+ val edits =
+ YXML.parse_body edits_yxml |>
+ let open XML.Decode in
+ list (pair string
+ (variant
+ [fn ([], []) => Document.Clear,
+ fn ([], a) => Document.Edits (list (pair (option int) (option int)) a),
+ fn ([], a) =>
+ Document.Header
+ (Exn.Res
+ (triple (pair string string) (list string) (list (pair string bool)) a)),
+ fn ([a], []) => Document.Header (Exn.Exn (ERROR a)),
+ fn (a, []) => Document.Perspective (map int_atom a)]))
+ end;
+
+ val running = Document.cancel_execution state;
+ val (assignment, state1) = Document.update old_id new_id edits state;
+ val _ = Future.join_tasks running;
+ val _ =
+ 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
+ |> YXML.string_of_body);
+ val state2 = Document.execute new_id state1;
+ in state2 end));
+
+val _ =
+ Isabelle_Process.add_command "Isabelle_Document.remove_versions"
+ (fn [versions_yxml] => Document.change_state (fn state =>
+ let
+ val versions =
+ YXML.parse_body versions_yxml |>
+ let open XML.Decode in list int end;
+ val state1 = Document.remove_versions versions state;
+ val _ = Output.raw_message Isabelle_Markup.removed_versions versions_yxml;
+ in state1 end));
+
+val _ =
+ Isabelle_Process.add_command "Isabelle_Document.invoke_scala"
+ (fn [id, tag, res] => Invoke_Scala.fulfill_method id tag res);
+
+end;
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/PIDE/isabelle_document.scala Tue Nov 29 21:50:00 2011 +0100
@@ -0,0 +1,231 @@
+/* Title: Pure/PIDE/isabelle_document.scala
+ Author: Makarius
+
+Protocol message formats for interactive Isar documents.
+*/
+
+package isabelle
+
+
+object Isabelle_Document
+{
+ /* document editing */
+
+ object Assign
+ {
+ def unapply(text: String): Option[(Document.Version_ID, Document.Assign)] =
+ try {
+ import XML.Decode._
+ val body = YXML.parse_body(text)
+ Some(pair(long, pair(list(pair(long, option(long))), list(pair(string, option(long)))))(body))
+ }
+ catch {
+ case ERROR(_) => None
+ case _: XML.XML_Atom => None
+ case _: XML.XML_Body => None
+ }
+ }
+
+ object Removed
+ {
+ def unapply(text: String): Option[List[Document.Version_ID]] =
+ try {
+ import XML.Decode._
+ Some(list(long)(YXML.parse_body(text)))
+ }
+ catch {
+ case ERROR(_) => None
+ case _: XML.XML_Atom => None
+ case _: XML.XML_Body => None
+ }
+ }
+
+
+ /* toplevel transactions */
+
+ sealed abstract class Status
+ case object Unprocessed extends Status
+ case class Forked(forks: Int) extends Status
+ case object Finished extends Status
+ case object Failed extends Status
+
+ def command_status(markup: List[Markup]): Status =
+ {
+ val forks = (0 /: markup) {
+ 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 == Isabelle_Markup.FAILED)) Failed
+ else if (markup.exists(_.name == Isabelle_Markup.FINISHED)) Finished
+ else Unprocessed
+ }
+
+ sealed case class Node_Status(unprocessed: Int, running: Int, finished: Int, failed: Int)
+ {
+ def total: Int = unprocessed + running + finished + failed
+ }
+
+ def node_status(
+ state: Document.State, version: Document.Version, node: Document.Node): Node_Status =
+ {
+ var unprocessed = 0
+ var running = 0
+ var finished = 0
+ var failed = 0
+ node.commands.foreach(command =>
+ command_status(state.command_state(version, command).status) match {
+ case Unprocessed => unprocessed += 1
+ case Forked(_) => running += 1
+ case Finished => finished += 1
+ case Failed => failed += 1
+ })
+ Node_Status(unprocessed, running, finished, failed)
+ }
+
+
+ /* result messages */
+
+ def clean_message(body: XML.Body): XML.Body =
+ 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(Isabelle_Markup.REPORT, _), _) => List(elem)
+ case XML.Elem(_, body) => body.flatMap(message_reports)
+ case XML.Text(_) => Nil
+ }
+
+
+ /* specific messages */
+
+ def is_ready(msg: XML.Tree): Boolean =
+ msg match {
+ 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(Isabelle_Markup.TRACING, _), _) => true
+ case _ => false
+ }
+
+ def is_warning(msg: XML.Tree): Boolean =
+ msg match {
+ case XML.Elem(Markup(Isabelle_Markup.WARNING, _), _) => true
+ case _ => false
+ }
+
+ def is_error(msg: XML.Tree): Boolean =
+ msg match {
+ case XML.Elem(Markup(Isabelle_Markup.ERROR, _), _) => true
+ case _ => false
+ }
+
+ def is_state(msg: XML.Tree): Boolean =
+ msg match {
+ case XML.Elem(Markup(Isabelle_Markup.WRITELN, _),
+ List(XML.Elem(Markup(Isabelle_Markup.STATE, _), _))) => true
+ case _ => false
+ }
+
+
+ /* reported positions */
+
+ private val include_pos =
+ Set(Isabelle_Markup.BINDING, Isabelle_Markup.ENTITY, Isabelle_Markup.REPORT,
+ Isabelle_Markup.POSITION)
+
+ def message_positions(command: Command, message: XML.Elem): Set[Text.Range] =
+ {
+ def positions(set: Set[Text.Range], tree: XML.Tree): Set[Text.Range] =
+ tree match {
+ case XML.Elem(Markup(name, Position.Id_Range(id, raw_range)), body)
+ if include_pos(name) && id == command.id =>
+ val range = command.decode(raw_range).restrict(command.range)
+ body.foldLeft(if (range.is_singularity) set else set + range)(positions)
+ case XML.Elem(Markup(name, _), body) => body.foldLeft(set)(positions)
+ case _ => set
+ }
+ val set = positions(Set.empty, message)
+ if (set.isEmpty && !is_state(message))
+ set ++ Position.Range.unapply(message.markup.properties).map(command.decode(_))
+ else set
+ }
+}
+
+
+trait Isabelle_Document extends Isabelle_Process
+{
+ /* commands */
+
+ def define_command(command: Command): Unit =
+ input("Isabelle_Document.define_command",
+ Document.ID(command.id), Symbol.encode(command.name), Symbol.encode(command.source))
+
+
+ /* document versions */
+
+ def cancel_execution()
+ {
+ input("Isabelle_Document.cancel_execution")
+ }
+
+ def update_perspective(old_id: Document.Version_ID, new_id: Document.Version_ID,
+ name: Document.Node.Name, perspective: Command.Perspective)
+ {
+ val ids =
+ { import XML.Encode._
+ list(long)(perspective.commands.map(_.id)) }
+
+ input("Isabelle_Document.update_perspective", Document.ID(old_id), Document.ID(new_id),
+ name.node, YXML.string_of_body(ids))
+ }
+
+ def update(old_id: Document.Version_ID, new_id: Document.Version_ID,
+ edits: List[Document.Edit_Command])
+ {
+ val edits_yxml =
+ { import XML.Encode._
+ def id: T[Command] = (cmd => long(cmd.id))
+ def encode_edit(dir: String)
+ : T[Document.Node.Edit[(Option[Command], Option[Command]), Command.Perspective]] =
+ variant(List(
+ { case Document.Node.Clear() => (Nil, Nil) },
+ { case Document.Node.Edits(a) => (Nil, list(pair(option(id), option(id)))(a)) },
+ { case Document.Node.Header(Exn.Res(Thy_Header(a, b, c))) =>
+ (Nil,
+ triple(pair(string, string), list(string), list(pair(string, bool)))(
+ (dir, a), b, c)) },
+ { case Document.Node.Header(Exn.Exn(e)) => (List(Exn.message(e)), Nil) },
+ { case Document.Node.Perspective(a) => (a.commands.map(c => long_atom(c.id)), Nil) }))
+ def encode: T[List[Document.Edit_Command]] = list((node_edit: Document.Edit_Command) =>
+ {
+ val (name, edit) = node_edit
+ val dir = Isabelle_System.posix_path(name.dir)
+ pair(string, encode_edit(dir))(name.node, edit)
+ })
+ YXML.string_of_body(encode(edits)) }
+ input("Isabelle_Document.update", Document.ID(old_id), Document.ID(new_id), edits_yxml)
+ }
+
+ def remove_versions(versions: List[Document.Version])
+ {
+ val versions_yxml =
+ { import XML.Encode._
+ YXML.string_of_body(list(long)(versions.map(_.id))) }
+ input("Isabelle_Document.remove_versions", versions_yxml)
+ }
+
+
+ /* method invocation service */
+
+ def invoke_scala(id: String, tag: Invoke_Scala.Tag.Value, res: String)
+ {
+ input("Isabelle_Document.invoke_scala", id, tag.toString, res)
+ }
+}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/PIDE/isabelle_markup.ML Tue Nov 29 21:50:00 2011 +0100
@@ -0,0 +1,328 @@
+(* Title: Pure/PIDE/isabelle_markup.ML
+ Author: Makarius
+
+Isabelle markup elements.
+*)
+
+signature ISABELLE_MARKUP =
+sig
+ val bindingN: string val binding: Markup.T
+ val entityN: string val entity: string -> string -> Markup.T
+ val get_entity_kind: Markup.T -> string option
+ val defN: string
+ val refN: string
+ val lineN: string
+ val offsetN: string
+ val end_offsetN: string
+ val fileN: string
+ val idN: string
+ val position_properties': string list
+ val position_properties: string list
+ val positionN: string val position: Markup.T
+ val pathN: string val path: string -> Markup.T
+ val indentN: string
+ val blockN: string val block: int -> Markup.T
+ val widthN: string
+ val breakN: string val break: int -> Markup.T
+ val fbreakN: string val fbreak: Markup.T
+ val hiddenN: string val hidden: Markup.T
+ val classN: string
+ val typeN: string
+ val constantN: string
+ val fixedN: string val fixed: string -> Markup.T
+ val dynamic_factN: string val dynamic_fact: string -> Markup.T
+ val tfreeN: string val tfree: Markup.T
+ val tvarN: string val tvar: Markup.T
+ val freeN: string val free: Markup.T
+ val skolemN: string val skolem: Markup.T
+ val boundN: string val bound: Markup.T
+ val varN: string val var: Markup.T
+ val numeralN: string val numeral: Markup.T
+ val literalN: string val literal: Markup.T
+ val delimiterN: string val delimiter: Markup.T
+ val inner_stringN: string val inner_string: Markup.T
+ val inner_commentN: string val inner_comment: Markup.T
+ val token_rangeN: string val token_range: Markup.T
+ val sortN: string val sort: Markup.T
+ val typN: string val typ: Markup.T
+ val termN: string val term: Markup.T
+ val propN: string val prop: Markup.T
+ val typingN: string val typing: Markup.T
+ val ML_keywordN: string val ML_keyword: Markup.T
+ val ML_delimiterN: string val ML_delimiter: Markup.T
+ val ML_tvarN: string val ML_tvar: Markup.T
+ val ML_numeralN: string val ML_numeral: Markup.T
+ val ML_charN: string val ML_char: Markup.T
+ val ML_stringN: string val ML_string: Markup.T
+ val ML_commentN: string val ML_comment: Markup.T
+ val ML_malformedN: string val ML_malformed: Markup.T
+ val ML_defN: string
+ val ML_openN: string
+ val ML_structN: string
+ val ML_typingN: string val ML_typing: Markup.T
+ val ML_sourceN: string val ML_source: Markup.T
+ val doc_sourceN: string val doc_source: Markup.T
+ val antiqN: string val antiq: Markup.T
+ val ML_antiquotationN: string
+ val doc_antiquotationN: string
+ val doc_antiquotation_optionN: string
+ val keyword_declN: string val keyword_decl: string -> Markup.T
+ val command_declN: string val command_decl: string -> string -> Markup.T
+ val keywordN: string val keyword: Markup.T
+ val operatorN: string val operator: Markup.T
+ val commandN: string val command: Markup.T
+ val stringN: string val string: Markup.T
+ val altstringN: string val altstring: Markup.T
+ val verbatimN: string val verbatim: Markup.T
+ val commentN: string val comment: Markup.T
+ val controlN: string val control: Markup.T
+ val malformedN: string val malformed: Markup.T
+ val tokenN: string val token: Properties.T -> Markup.T
+ val command_spanN: string val command_span: string -> Markup.T
+ val ignored_spanN: string val ignored_span: Markup.T
+ val malformed_spanN: string val malformed_span: Markup.T
+ val loaded_theoryN: string val loaded_theory: string -> Markup.T
+ val elapsedN: string
+ val cpuN: string
+ val gcN: string
+ val timingN: string val timing: Timing.timing -> 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;
+
+
+(* timing *)
+
+val timingN = "timing";
+val elapsedN = "elapsed";
+val cpuN = "cpu";
+val gcN = "gc";
+
+fun timing {elapsed, cpu, gc} =
+ (timingN,
+ [(elapsedN, Time.toString elapsed),
+ (cpuN, Time.toString cpu),
+ (gcN, Time.toString gc)]);
+
+
+(* toplevel *)
+
+val subgoalsN = "subgoals";
+val (proof_stateN, proof_state) = markup_int "proof_state" subgoalsN;
+
+val (stateN, state) = markup_elem "state";
+val (subgoalN, subgoal) = markup_elem "subgoal";
+val (sendbackN, sendback) = markup_elem "sendback";
+val (hiliteN, hilite) = markup_elem "hilite";
+
+
+(* command status *)
+
+val taskN = "task";
+
+val (forkedN, forked) = markup_elem "forked";
+val (joinedN, joined) = markup_elem "joined";
+
+val (failedN, failed) = markup_elem "failed";
+val (finishedN, finished) = markup_elem "finished";
+
+
+(* messages *)
+
+val serialN = "serial";
+
+val (legacyN, legacy) = markup_elem "legacy";
+val (promptN, prompt) = markup_elem "prompt";
+val (readyN, ready) = markup_elem "ready";
+
+val (reportN, report) = markup_elem "report";
+val (no_reportN, no_report) = markup_elem "no_report";
+
+val (badN, bad) = markup_elem "bad";
+
+
+(* raw message functions *)
+
+val functionN = "function"
+
+val assign_execs = [(functionN, "assign_execs")];
+val removed_versions = [(functionN, "removed_versions")];
+
+fun invoke_scala name id = [(functionN, "invoke_scala"), (Markup.nameN, name), (idN, id)];
+fun cancel_scala id = [(functionN, "cancel_scala"), (idN, id)];
+
+end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/PIDE/isabelle_markup.scala Tue Nov 29 21:50:00 2011 +0100
@@ -0,0 +1,286 @@
+/* Title: Pure/PIDE/isabelle_markup.scala
+ Author: Makarius
+
+Isabelle markup elements.
+*/
+
+package isabelle
+
+
+object Isabelle_Markup
+{
+ /* formal entities */
+
+ val BINDING = "binding"
+ val ENTITY = "entity"
+ val DEF = "def"
+ val REF = "ref"
+
+ object Entity
+ {
+ def unapply(markup: Markup): Option[(String, String)] =
+ markup match {
+ case Markup(ENTITY, props @ Markup.Kind(kind)) =>
+ props match {
+ case Markup.Name(name) => Some(kind, name)
+ case _ => None
+ }
+ case _ => None
+ }
+ }
+
+
+ /* position */
+
+ val LINE = "line"
+ val OFFSET = "offset"
+ val END_OFFSET = "end_offset"
+ val FILE = "file"
+ val ID = "id"
+
+ val DEF_LINE = "def_line"
+ val DEF_OFFSET = "def_offset"
+ val DEF_END_OFFSET = "def_end_offset"
+ val DEF_FILE = "def_file"
+ val DEF_ID = "def_id"
+
+ val POSITION_PROPERTIES = Set(LINE, OFFSET, END_OFFSET, FILE, ID)
+ val POSITION = "position"
+
+
+ /* path */
+
+ val PATH = "path"
+
+ object Path
+ {
+ def unapply(markup: Markup): Option[String] =
+ markup match {
+ case Markup(PATH, Markup.Name(name)) => Some(name)
+ case _ => None
+ }
+ }
+
+
+ /* pretty printing */
+
+ val Indent = new Properties.Int("indent")
+ val BLOCK = "block"
+ val Width = new Properties.Int("width")
+ val BREAK = "break"
+
+
+ /* hidden text */
+
+ val HIDDEN = "hidden"
+
+
+ /* logical entities */
+
+ val CLASS = "class"
+ val TYPE = "type"
+ val FIXED = "fixed"
+ val CONSTANT = "constant"
+
+ val DYNAMIC_FACT = "dynamic_fact"
+
+
+ /* inner syntax */
+
+ val TFREE = "tfree"
+ val TVAR = "tvar"
+ val FREE = "free"
+ val SKOLEM = "skolem"
+ val BOUND = "bound"
+ val VAR = "var"
+ val NUM = "num"
+ val FLOAT = "float"
+ val XNUM = "xnum"
+ val XSTR = "xstr"
+ val LITERAL = "literal"
+ val DELIMITER = "delimiter"
+ val INNER_STRING = "inner_string"
+ val INNER_COMMENT = "inner_comment"
+
+ val TOKEN_RANGE = "token_range"
+
+ val SORT = "sort"
+ val TYP = "typ"
+ val TERM = "term"
+ val PROP = "prop"
+
+ val TYPING = "typing"
+
+ val ATTRIBUTE = "attribute"
+ val METHOD = "method"
+
+
+ /* embedded source text */
+
+ val ML_SOURCE = "ML_source"
+ val DOC_SOURCE = "doc_source"
+
+ val ANTIQ = "antiq"
+ val ML_ANTIQUOTATION = "ML antiquotation"
+ val DOCUMENT_ANTIQUOTATION = "document antiquotation"
+ val DOCUMENT_ANTIQUOTATION_OPTION = "document antiquotation option"
+
+
+ /* ML syntax */
+
+ val ML_KEYWORD = "ML_keyword"
+ val ML_DELIMITER = "ML_delimiter"
+ val ML_TVAR = "ML_tvar"
+ val ML_NUMERAL = "ML_numeral"
+ val ML_CHAR = "ML_char"
+ val ML_STRING = "ML_string"
+ val ML_COMMENT = "ML_comment"
+ val ML_MALFORMED = "ML_malformed"
+
+ val ML_DEF = "ML_def"
+ val ML_OPEN = "ML_open"
+ val ML_STRUCT = "ML_struct"
+ val ML_TYPING = "ML_typing"
+
+
+ /* outer syntax */
+
+ val KEYWORD_DECL = "keyword_decl"
+ val COMMAND_DECL = "command_decl"
+
+ val KEYWORD = "keyword"
+ val OPERATOR = "operator"
+ val COMMAND = "command"
+ val STRING = "string"
+ val ALTSTRING = "altstring"
+ val VERBATIM = "verbatim"
+ val COMMENT = "comment"
+ val CONTROL = "control"
+ val MALFORMED = "malformed"
+
+ val COMMAND_SPAN = "command_span"
+ val IGNORED_SPAN = "ignored_span"
+ val MALFORMED_SPAN = "malformed_span"
+
+
+ /* theory loader */
+
+ val LOADED_THEORY = "loaded_theory"
+
+
+ /* timing */
+
+ val TIMING = "timing"
+ val ELAPSED = "elapsed"
+ val CPU = "cpu"
+ val GC = "gc"
+
+ object Timing
+ {
+ def apply(timing: isabelle.Timing): Markup =
+ Markup(TIMING, List(
+ (ELAPSED, Properties.Value.Double(timing.elapsed.seconds)),
+ (CPU, Properties.Value.Double(timing.cpu.seconds)),
+ (GC, Properties.Value.Double(timing.gc.seconds))))
+ def unapply(markup: Markup): Option[isabelle.Timing] =
+ markup match {
+ case Markup(TIMING, List(
+ (ELAPSED, Properties.Value.Double(elapsed)),
+ (CPU, Properties.Value.Double(cpu)),
+ (GC, Properties.Value.Double(gc)))) =>
+ Some(new isabelle.Timing(Time.seconds(elapsed), Time.seconds(cpu), Time.seconds(gc)))
+ case _ => None
+ }
+ }
+
+
+ /* toplevel */
+
+ val SUBGOALS = "subgoals"
+ val PROOF_STATE = "proof_state"
+
+ val STATE = "state"
+ val SUBGOAL = "subgoal"
+ val SENDBACK = "sendback"
+ val HILITE = "hilite"
+
+
+ /* command status */
+
+ val TASK = "task"
+
+ val FORKED = "forked"
+ val JOINED = "joined"
+ val FAILED = "failed"
+ val FINISHED = "finished"
+
+
+ /* interactive documents */
+
+ val VERSION = "version"
+ val ASSIGN = "assign"
+
+
+ /* prover process */
+
+ val PROVER_COMMAND = "prover_command"
+ val PROVER_ARG = "prover_arg"
+
+
+ /* messages */
+
+ val Serial = new Properties.Long("serial")
+
+ val MESSAGE = "message"
+
+ val INIT = "init"
+ val STATUS = "status"
+ val REPORT = "report"
+ val WRITELN = "writeln"
+ val TRACING = "tracing"
+ val WARNING = "warning"
+ val ERROR = "error"
+ val RAW = "raw"
+ val SYSTEM = "system"
+ val STDOUT = "stdout"
+ val STDERR = "stderr"
+ val EXIT = "exit"
+
+ val LEGACY = "legacy"
+
+ val NO_REPORT = "no_report"
+
+ val BAD = "bad"
+
+ val READY = "ready"
+
+
+ /* raw message functions */
+
+ val FUNCTION = "function"
+ val Function = new Properties.String(FUNCTION)
+
+ val Assign_Execs: Properties.T = List((FUNCTION, "assign_execs"))
+ val Removed_Versions: Properties.T = List((FUNCTION, "removed_versions"))
+
+ val INVOKE_SCALA = "invoke_scala"
+ object Invoke_Scala
+ {
+ def unapply(props: Properties.T): Option[(String, String)] =
+ props match {
+ case List((FUNCTION, INVOKE_SCALA), (Markup.NAME, name), (ID, id)) => Some((name, id))
+ case _ => None
+ }
+ }
+
+ val CANCEL_SCALA = "cancel_scala"
+ object Cancel_Scala
+ {
+ def unapply(props: Properties.T): Option[String] =
+ props match {
+ case List((FUNCTION, CANCEL_SCALA), (ID, id)) => Some(id)
+ case _ => None
+ }
+ }
+}
+
--- a/src/Pure/PIDE/isar_document.ML Tue Nov 29 15:52:51 2011 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,84 +0,0 @@
-(* Title: Pure/PIDE/isar_document.ML
- Author: Makarius
-
-Protocol message formats for interactive Isar documents.
-*)
-
-structure Isar_Document: sig end =
-struct
-
-val _ =
- Isabelle_Process.add_command "Isar_Document.define_command"
- (fn [id, name, text] =>
- Document.change_state (Document.define_command (Document.parse_id id) name text));
-
-val _ =
- Isabelle_Process.add_command "Isar_Document.cancel_execution"
- (fn [] => ignore (Document.cancel_execution (Document.state ())));
-
-val _ =
- Isabelle_Process.add_command "Isar_Document.update_perspective"
- (fn [old_id_string, new_id_string, name, ids_yxml] => Document.change_state (fn state =>
- let
- val old_id = Document.parse_id old_id_string;
- val new_id = Document.parse_id new_id_string;
- val ids = YXML.parse_body ids_yxml
- |> let open XML.Decode in list int end;
-
- val _ = Future.join_tasks (Document.cancel_execution state);
- in
- state
- |> Document.update_perspective old_id new_id name ids
- |> Document.execute new_id
- end));
-
-val _ =
- Isabelle_Process.add_command "Isar_Document.update"
- (fn [old_id_string, new_id_string, edits_yxml] => Document.change_state (fn state =>
- let
- val old_id = Document.parse_id old_id_string;
- val new_id = Document.parse_id new_id_string;
- val edits =
- YXML.parse_body edits_yxml |>
- let open XML.Decode in
- list (pair string
- (variant
- [fn ([], []) => Document.Clear,
- fn ([], a) => Document.Edits (list (pair (option int) (option int)) a),
- fn ([], a) =>
- Document.Header
- (Exn.Res
- (triple (pair string string) (list string) (list (pair string bool)) a)),
- fn ([a], []) => Document.Header (Exn.Exn (ERROR a)),
- fn (a, []) => Document.Perspective (map int_atom a)]))
- end;
-
- val running = Document.cancel_execution state;
- val (assignment, state1) = Document.update old_id new_id edits state;
- val _ = Future.join_tasks running;
- val _ =
- 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
- |> YXML.string_of_body);
- val state2 = Document.execute new_id state1;
- in state2 end));
-
-val _ =
- Isabelle_Process.add_command "Isar_Document.remove_versions"
- (fn [versions_yxml] => Document.change_state (fn state =>
- let
- val versions =
- YXML.parse_body versions_yxml |>
- let open XML.Decode in list int end;
- val state1 = Document.remove_versions versions state;
- val _ = Output.raw_message Isabelle_Markup.removed_versions versions_yxml;
- in state1 end));
-
-val _ =
- Isabelle_Process.add_command "Isar_Document.invoke_scala"
- (fn [id, tag, res] => Invoke_Scala.fulfill_method id tag res);
-
-end;
-
--- a/src/Pure/PIDE/isar_document.scala Tue Nov 29 15:52:51 2011 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,231 +0,0 @@
-/* Title: Pure/PIDE/isar_document.scala
- Author: Makarius
-
-Protocol message formats for interactive Isar documents.
-*/
-
-package isabelle
-
-
-object Isar_Document
-{
- /* document editing */
-
- object Assign
- {
- def unapply(text: String): Option[(Document.Version_ID, Document.Assign)] =
- try {
- import XML.Decode._
- val body = YXML.parse_body(text)
- Some(pair(long, pair(list(pair(long, option(long))), list(pair(string, option(long)))))(body))
- }
- catch {
- case ERROR(_) => None
- case _: XML.XML_Atom => None
- case _: XML.XML_Body => None
- }
- }
-
- object Removed
- {
- def unapply(text: String): Option[List[Document.Version_ID]] =
- try {
- import XML.Decode._
- Some(list(long)(YXML.parse_body(text)))
- }
- catch {
- case ERROR(_) => None
- case _: XML.XML_Atom => None
- case _: XML.XML_Body => None
- }
- }
-
-
- /* toplevel transactions */
-
- sealed abstract class Status
- case object Unprocessed extends Status
- case class Forked(forks: Int) extends Status
- case object Finished extends Status
- case object Failed extends Status
-
- def command_status(markup: List[Markup]): Status =
- {
- val forks = (0 /: markup) {
- 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 == Isabelle_Markup.FAILED)) Failed
- else if (markup.exists(_.name == Isabelle_Markup.FINISHED)) Finished
- else Unprocessed
- }
-
- sealed case class Node_Status(unprocessed: Int, running: Int, finished: Int, failed: Int)
- {
- def total: Int = unprocessed + running + finished + failed
- }
-
- def node_status(
- state: Document.State, version: Document.Version, node: Document.Node): Node_Status =
- {
- var unprocessed = 0
- var running = 0
- var finished = 0
- var failed = 0
- node.commands.foreach(command =>
- command_status(state.command_state(version, command).status) match {
- case Unprocessed => unprocessed += 1
- case Forked(_) => running += 1
- case Finished => finished += 1
- case Failed => failed += 1
- })
- Node_Status(unprocessed, running, finished, failed)
- }
-
-
- /* result messages */
-
- def clean_message(body: XML.Body): XML.Body =
- 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(Isabelle_Markup.REPORT, _), _) => List(elem)
- case XML.Elem(_, body) => body.flatMap(message_reports)
- case XML.Text(_) => Nil
- }
-
-
- /* specific messages */
-
- def is_ready(msg: XML.Tree): Boolean =
- msg match {
- 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(Isabelle_Markup.TRACING, _), _) => true
- case _ => false
- }
-
- def is_warning(msg: XML.Tree): Boolean =
- msg match {
- case XML.Elem(Markup(Isabelle_Markup.WARNING, _), _) => true
- case _ => false
- }
-
- def is_error(msg: XML.Tree): Boolean =
- msg match {
- case XML.Elem(Markup(Isabelle_Markup.ERROR, _), _) => true
- case _ => false
- }
-
- def is_state(msg: XML.Tree): Boolean =
- msg match {
- case XML.Elem(Markup(Isabelle_Markup.WRITELN, _),
- List(XML.Elem(Markup(Isabelle_Markup.STATE, _), _))) => true
- case _ => false
- }
-
-
- /* reported positions */
-
- private val include_pos =
- Set(Isabelle_Markup.BINDING, Isabelle_Markup.ENTITY, Isabelle_Markup.REPORT,
- Isabelle_Markup.POSITION)
-
- def message_positions(command: Command, message: XML.Elem): Set[Text.Range] =
- {
- def positions(set: Set[Text.Range], tree: XML.Tree): Set[Text.Range] =
- tree match {
- case XML.Elem(Markup(name, Position.Id_Range(id, raw_range)), body)
- if include_pos(name) && id == command.id =>
- val range = command.decode(raw_range).restrict(command.range)
- body.foldLeft(if (range.is_singularity) set else set + range)(positions)
- case XML.Elem(Markup(name, _), body) => body.foldLeft(set)(positions)
- case _ => set
- }
- val set = positions(Set.empty, message)
- if (set.isEmpty && !is_state(message))
- set ++ Position.Range.unapply(message.markup.properties).map(command.decode(_))
- else set
- }
-}
-
-
-trait Isar_Document extends Isabelle_Process
-{
- /* commands */
-
- def define_command(command: Command): Unit =
- input("Isar_Document.define_command",
- Document.ID(command.id), Symbol.encode(command.name), Symbol.encode(command.source))
-
-
- /* document versions */
-
- def cancel_execution()
- {
- input("Isar_Document.cancel_execution")
- }
-
- def update_perspective(old_id: Document.Version_ID, new_id: Document.Version_ID,
- name: Document.Node.Name, perspective: Command.Perspective)
- {
- val ids =
- { import XML.Encode._
- list(long)(perspective.commands.map(_.id)) }
-
- input("Isar_Document.update_perspective", Document.ID(old_id), Document.ID(new_id),
- name.node, YXML.string_of_body(ids))
- }
-
- def update(old_id: Document.Version_ID, new_id: Document.Version_ID,
- edits: List[Document.Edit_Command])
- {
- val edits_yxml =
- { import XML.Encode._
- def id: T[Command] = (cmd => long(cmd.id))
- def encode_edit(dir: String)
- : T[Document.Node.Edit[(Option[Command], Option[Command]), Command.Perspective]] =
- variant(List(
- { case Document.Node.Clear() => (Nil, Nil) },
- { case Document.Node.Edits(a) => (Nil, list(pair(option(id), option(id)))(a)) },
- { case Document.Node.Header(Exn.Res(Thy_Header(a, b, c))) =>
- (Nil,
- triple(pair(string, string), list(string), list(pair(string, bool)))(
- (dir, a), b, c)) },
- { case Document.Node.Header(Exn.Exn(e)) => (List(Exn.message(e)), Nil) },
- { case Document.Node.Perspective(a) => (a.commands.map(c => long_atom(c.id)), Nil) }))
- def encode: T[List[Document.Edit_Command]] = list((node_edit: Document.Edit_Command) =>
- {
- val (name, edit) = node_edit
- val dir = Isabelle_System.posix_path(name.dir)
- pair(string, encode_edit(dir))(name.node, edit)
- })
- YXML.string_of_body(encode(edits)) }
- input("Isar_Document.update", Document.ID(old_id), Document.ID(new_id), edits_yxml)
- }
-
- def remove_versions(versions: List[Document.Version])
- {
- val versions_yxml =
- { import XML.Encode._
- YXML.string_of_body(list(long)(versions.map(_.id))) }
- input("Isar_Document.remove_versions", versions_yxml)
- }
-
-
- /* method invocation service */
-
- def invoke_scala(id: String, tag: Invoke_Scala.Tag.Value, res: String)
- {
- input("Isar_Document.invoke_scala", id, tag.toString, res)
- }
-}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/PIDE/markup.ML Tue Nov 29 21:50:00 2011 +0100
@@ -0,0 +1,93 @@
+(* Title: Pure/PIDE/markup.ML
+ Author: Makarius
+
+Generic markup elements.
+*)
+
+signature MARKUP =
+sig
+ val parse_int: string -> int
+ val print_int: int -> string
+ type T = string * Properties.T
+ val empty: T
+ val is_empty: T -> bool
+ val properties: Properties.T -> T -> T
+ val nameN: string
+ val name: string -> T -> T
+ val kindN: string
+ val no_output: Output.output * Output.output
+ val default_output: T -> Output.output * Output.output
+ val add_mode: string -> (T -> Output.output * Output.output) -> unit
+ val output: T -> Output.output * Output.output
+ val enclose: T -> Output.output -> Output.output
+ val markup: T -> string -> string
+ val markup_only: T -> string
+end;
+
+structure Markup: MARKUP =
+struct
+
+(** markup elements **)
+
+(* integers *)
+
+fun parse_int s =
+ let val i = Int.fromString s in
+ if is_none i orelse String.isPrefix "~" s
+ then raise Fail ("Bad integer: " ^ quote s)
+ else the i
+ end;
+
+val print_int = signed_string_of_int;
+
+
+(* basic markup *)
+
+type T = string * Properties.T;
+
+val empty = ("", []);
+
+fun is_empty ("", _) = true
+ | is_empty _ = false;
+
+
+fun properties more_props ((elem, props): T) =
+ (elem, fold_rev Properties.put more_props props);
+
+
+(* misc properties *)
+
+val nameN = "name";
+fun name a = properties [(nameN, a)];
+
+val kindN = "kind";
+
+
+
+(** print mode operations **)
+
+val no_output = ("", "");
+fun default_output (_: T) = no_output;
+
+local
+ val default = {output = default_output};
+ val modes = Synchronized.var "Markup.modes" (Symtab.make [("", default)]);
+in
+ fun add_mode name output =
+ Synchronized.change modes (Symtab.update_new (name, {output = output}));
+ fun get_mode () =
+ the_default default
+ (Library.get_first (Symtab.lookup (Synchronized.value modes)) (print_mode_value ()));
+end;
+
+fun output m = if is_empty m then no_output else #output (get_mode ()) m;
+
+val enclose = output #-> Library.enclose;
+
+fun markup m =
+ let val (bg, en) = output m
+ in Library.enclose (Output.escape bg) (Output.escape en) end;
+
+fun markup_only m = markup m "";
+
+end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/PIDE/markup.scala Tue Nov 29 21:50:00 2011 +0100
@@ -0,0 +1,31 @@
+/* Title: Pure/PIDE/markup.scala
+ Module: PIDE
+ Author: Makarius
+
+Generic markup elements.
+*/
+
+package isabelle
+
+
+object Markup
+{
+ /* properties */
+
+ val NAME = "name"
+ val Name = new Properties.String(NAME)
+
+ val KIND = "kind"
+ val Kind = new Properties.String(KIND)
+
+
+ /* elements */
+
+ val Empty = Markup("", Nil)
+ val Data = Markup("data", Nil)
+ val Broken = Markup("broken", Nil)
+}
+
+
+sealed case class Markup(name: String, properties: Properties.T)
+
--- a/src/Pure/PIDE/markup_tree.scala Tue Nov 29 15:52:51 2011 +0100
+++ b/src/Pure/PIDE/markup_tree.scala Tue Nov 29 21:50:00 2011 +0100
@@ -1,5 +1,5 @@
/* Title: Pure/PIDE/markup_tree.scala
- Module: Library
+ Module: PIDE
Author: Fabian Immler, TU Munich
Author: Makarius
--- a/src/Pure/PIDE/text.scala Tue Nov 29 15:52:51 2011 +0100
+++ b/src/Pure/PIDE/text.scala Tue Nov 29 21:50:00 2011 +0100
@@ -1,5 +1,5 @@
/* Title: Pure/PIDE/text.scala
- Module: Library
+ Module: PIDE
Author: Fabian Immler, TU Munich
Author: Makarius
--- a/src/Pure/PIDE/xml.scala Tue Nov 29 15:52:51 2011 +0100
+++ b/src/Pure/PIDE/xml.scala Tue Nov 29 21:50:00 2011 +0100
@@ -1,5 +1,5 @@
/* Title: Pure/PIDE/xml.scala
- Module: Library
+ Module: PIDE
Author: Makarius
Untyped XML trees and basic data representation.
--- a/src/Pure/PIDE/yxml.scala Tue Nov 29 15:52:51 2011 +0100
+++ b/src/Pure/PIDE/yxml.scala Tue Nov 29 21:50:00 2011 +0100
@@ -1,5 +1,5 @@
/* Title: Pure/PIDE/yxml.scala
- Module: Library
+ Module: PIDE
Author: Makarius
Efficient text representation of XML trees. Suitable for direct
--- a/src/Pure/ROOT.ML Tue Nov 29 15:52:51 2011 +0100
+++ b/src/Pure/ROOT.ML Tue Nov 29 21:50:00 2011 +0100
@@ -30,8 +30,8 @@
use "General/properties.ML";
use "General/output.ML";
use "General/timing.ML";
-use "General/markup.ML";
-use "General/isabelle_markup.ML";
+use "PIDE/markup.ML";
+use "PIDE/isabelle_markup.ML";
fun legacy_feature s = warning (Markup.markup Isabelle_Markup.legacy ("Legacy feature! " ^ s));
use "General/scan.ML";
use "General/source.ML";
@@ -270,7 +270,7 @@
use "System/system_channel.ML";
use "System/isabelle_process.ML";
use "System/invoke_scala.ML";
-use "PIDE/isar_document.ML";
+use "PIDE/isabelle_document.ML";
use "System/isar.ML";
--- a/src/Pure/System/cygwin.scala Tue Nov 29 15:52:51 2011 +0100
+++ b/src/Pure/System/cygwin.scala Tue Nov 29 21:50:00 2011 +0100
@@ -1,5 +1,5 @@
/* Title: Pure/System/cygwin.scala
- Module: Library
+ Module: PIDE
Author: Makarius
Accessing the Cygwin installation.
--- a/src/Pure/System/download.scala Tue Nov 29 15:52:51 2011 +0100
+++ b/src/Pure/System/download.scala Tue Nov 29 21:50:00 2011 +0100
@@ -1,5 +1,5 @@
/* Title: Pure/System/download.scala
- Module: Library
+ Module: PIDE
Author: Makarius
Download URLs -- with progress monitor.
--- a/src/Pure/System/event_bus.scala Tue Nov 29 15:52:51 2011 +0100
+++ b/src/Pure/System/event_bus.scala Tue Nov 29 21:50:00 2011 +0100
@@ -1,5 +1,5 @@
/* Title: Pure/System/event_bus.scala
- Module: Library
+ Module: PIDE
Author: Makarius
Generic event bus with multiple receiving actors.
--- a/src/Pure/System/isabelle_process.scala Tue Nov 29 15:52:51 2011 +0100
+++ b/src/Pure/System/isabelle_process.scala Tue Nov 29 21:50:00 2011 +0100
@@ -58,7 +58,7 @@
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_ready = Isabelle_Document.is_ready(message)
def is_syslog = is_init || is_exit || is_system || is_ready || is_stderr
override def toString: String =
@@ -100,7 +100,7 @@
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))
+ val msg = XML.Elem(Markup(kind, props), Isabelle_Document.clean_message(body))
receiver(new Result(xml_cache.cache_tree(msg).asInstanceOf[XML.Elem]))
}
}
--- a/src/Pure/System/platform.scala Tue Nov 29 15:52:51 2011 +0100
+++ b/src/Pure/System/platform.scala Tue Nov 29 21:50:00 2011 +0100
@@ -1,5 +1,5 @@
/* Title: Pure/System/platform.scala
- Module: Library
+ Module: PIDE
Author: Makarius
Raw platform identification.
--- a/src/Pure/System/session.scala Tue Nov 29 15:52:51 2011 +0100
+++ b/src/Pure/System/session.scala Tue Nov 29 21:50:00 2011 +0100
@@ -211,7 +211,7 @@
def cancel() { timer.cancel() }
}
- var prover: Option[Isabelle_Process with Isar_Document] = None
+ var prover: Option[Isabelle_Process with Isabelle_Document] = None
/* delayed command changes */
@@ -365,7 +365,7 @@
}
case Isabelle_Markup.Assign_Execs if result.is_raw =>
XML.content(result.body).mkString match {
- case Isar_Document.Assign(id, assign) =>
+ case Isabelle_Document.Assign(id, assign) =>
try { handle_assign(id, assign) }
catch { case _: Document.State.Fail => bad_result(result) }
case _ => bad_result(result)
@@ -378,7 +378,7 @@
}
case Isabelle_Markup.Removed_Versions if result.is_raw =>
XML.content(result.body).mkString match {
- case Isar_Document.Removed(removed) =>
+ case Isabelle_Document.Removed(removed) =>
try { handle_removed(removed) }
catch { case _: Document.State.Fail => bad_result(result) }
case _ => bad_result(result)
@@ -430,7 +430,7 @@
if (phase == Session.Inactive || phase == Session.Failed) {
phase = Session.Startup
prover =
- Some(new Isabelle_Process(timeout, receiver.invoke _, args) with Isar_Document)
+ Some(new Isabelle_Process(timeout, receiver.invoke _, args) with Isabelle_Document)
}
case Stop =>
--- a/src/Pure/System/standard_system.scala Tue Nov 29 15:52:51 2011 +0100
+++ b/src/Pure/System/standard_system.scala Tue Nov 29 21:50:00 2011 +0100
@@ -1,5 +1,5 @@
/* Title: Pure/System/standard_system.scala
- Module: Library
+ Module: PIDE
Author: Makarius
Standard system operations, with basic Cygwin/Posix compatibility.
--- a/src/Pure/System/swing_thread.scala Tue Nov 29 15:52:51 2011 +0100
+++ b/src/Pure/System/swing_thread.scala Tue Nov 29 21:50:00 2011 +0100
@@ -1,5 +1,5 @@
/* Title: Pure/System/swing_thread.scala
- Module: Library
+ Module: PIDE
Author: Makarius
Author: Fabian Immler, TU Munich
--- a/src/Pure/build-jars Tue Nov 29 15:52:51 2011 +0100
+++ b/src/Pure/build-jars Tue Nov 29 21:50:00 2011 +0100
@@ -14,9 +14,7 @@
Concurrent/simple_thread.scala
Concurrent/volatile.scala
General/exn.scala
- General/isabelle_markup.scala
General/linear_set.scala
- General/markup.scala
General/path.scala
General/position.scala
General/pretty.scala
@@ -24,6 +22,7 @@
General/scan.scala
General/sha1.scala
General/symbol.scala
+ General/time.scala
General/timing.scala
Isar/keyword.scala
Isar/outer_syntax.scala
@@ -32,7 +31,9 @@
PIDE/blob.scala
PIDE/command.scala
PIDE/document.scala
- PIDE/isar_document.scala
+ PIDE/isabelle_document.scala
+ PIDE/isabelle_markup.scala
+ PIDE/markup.scala
PIDE/markup_tree.scala
PIDE/text.scala
PIDE/xml.scala
@@ -121,6 +122,19 @@
TARGET_DIR="$ISABELLE_HOME/lib/classes"
TARGET="$TARGET_DIR/ext/Pure.jar"
+declare -a PIDE_SOURCES=()
+declare -a PURE_SOURCES=()
+
+for DEP in "${SOURCES[@]}"
+do
+ if grep "Module:.*PIDE" "$DEP" >/dev/null
+ then
+ PIDE_SOURCES["${#PIDE_SOURCES[@]}"]="$DEP"
+ else
+ PURE_SOURCES["${#PURE_SOURCES[@]}"]="$DEP"
+ fi
+done
+
declare -a UPDATED=()
if [ -n "$FRESH" ]; then
@@ -154,8 +168,15 @@
}
rm -rf classes && mkdir classes
- "$SCALA_HOME/bin/scalac" -unchecked -deprecation -d classes -target:jvm-1.5 "${SOURCES[@]}" || \
- fail "Failed to compile sources"
+
+ SCALAC_OPTIONS="-unchecked -deprecation -d classes -target:jvm-1.5"
+
+ "$SCALA_HOME/bin/scalac" $SCALAC_OPTIONS "${PIDE_SOURCES[@]}" || \
+ fail "Failed to compile PIDE sources"
+
+ "$SCALA_HOME/bin/scalac" $SCALAC_OPTIONS -classpath classes "${PURE_SOURCES[@]}" || \
+ fail "Failed to compile Pure sources"
+
mkdir -p "$TARGET_DIR/ext" || fail "Failed to create directory $TARGET_DIR/ext"
pushd classes >/dev/null
--- a/src/Pure/library.scala Tue Nov 29 15:52:51 2011 +0100
+++ b/src/Pure/library.scala Tue Nov 29 21:50:00 2011 +0100
@@ -1,5 +1,5 @@
/* Title: Pure/library.scala
- Module: Library
+ Module: PIDE
Author: Makarius
Basic library.
--- a/src/Pure/package.scala Tue Nov 29 15:52:51 2011 +0100
+++ b/src/Pure/package.scala Tue Nov 29 21:50:00 2011 +0100
@@ -1,5 +1,5 @@
/* Title: Pure/package.scala
- Module: Library
+ Module: PIDE
Author: Makarius
Toplevel isabelle package.
--- a/src/Tools/jEdit/src/isabelle_hyperlinks.scala Tue Nov 29 15:52:51 2011 +0100
+++ b/src/Tools/jEdit/src/isabelle_hyperlinks.scala Tue Nov 29 21:50:00 2011 +0100
@@ -60,7 +60,7 @@
snapshot.select_markup(Text.Range(buffer_offset, buffer_offset + 1))(
Markup_Tree.Select[Hyperlink](
{
- // FIXME Isar_Document.Hyperlink extractor
+ // FIXME Isabelle_Document.Hyperlink extractor
case Text.Info(info_range,
XML.Elem(Markup(Isabelle_Markup.ENTITY, props), _))
if (props.find(
--- a/src/Tools/jEdit/src/isabelle_rendering.scala Tue Nov 29 15:52:51 2011 +0100
+++ b/src/Tools/jEdit/src/isabelle_rendering.scala Tue Nov 29 21:50:00 2011 +0100
@@ -61,9 +61,9 @@
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)
+ Isabelle_Document.command_status(state.status) match {
+ case Isabelle_Document.Forked(i) if i > 0 => Some(running1_color)
+ case Isabelle_Document.Unprocessed => Some(unprocessed1_color)
case _ => None
}
}
@@ -73,13 +73,13 @@
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)
+ Isabelle_Document.command_status(state.status) match {
+ case Isabelle_Document.Forked(i) => if (i > 0) Some(running_color) else None
+ case Isabelle_Document.Unprocessed => Some(unprocessed_color)
+ case Isabelle_Document.Failed => Some(error_color)
+ case Isabelle_Document.Finished =>
+ if (state.results.exists(r => Isabelle_Document.is_error(r._2))) Some(error_color)
+ else if (state.results.exists(r => Isabelle_Document.is_warning(r._2))) Some(warning_color)
else None
}
}
--- a/src/Tools/jEdit/src/session_dockable.scala Tue Nov 29 15:52:51 2011 +0100
+++ b/src/Tools/jEdit/src/session_dockable.scala Tue Nov 29 21:50:00 2011 +0100
@@ -94,7 +94,7 @@
/* component state -- owned by Swing thread */
- private var nodes_status: Map[Document.Node.Name, Isar_Document.Node_Status] = Map.empty
+ private var nodes_status: Map[Document.Node.Name, Isabelle_Document.Node_Status] = Map.empty
private object Node_Renderer_Component extends Label
{
@@ -152,7 +152,7 @@
for {
name <- nodes
node <- snapshot.version.nodes.get(name)
- val status = Isar_Document.node_status(snapshot.state, snapshot.version, node)
+ val status = Isabelle_Document.node_status(snapshot.state, snapshot.version, node)
} nodes_status1 += (name -> status)
if (nodes_status != nodes_status1) {