1.1 --- a/src/Pure/Concurrent/future.ML Tue Jul 05 19:11:29 2011 +0200
1.2 +++ b/src/Pure/Concurrent/future.ML Wed Jul 06 09:54:40 2011 +0200
1.3 @@ -584,9 +584,9 @@
1.4 (case worker_task () of
1.5 NONE => I
1.6 | SOME task => Markup.properties [(Markup.taskN, Task_Queue.str_of_task task)]);
1.7 - val _ = Output.status (Markup.markup (task_props Markup.forked) "");
1.8 + val _ = Output.status (Markup.markup_only (task_props Markup.forked));
1.9 val x = e (); (*sic -- report "joined" only for success*)
1.10 - val _ = Output.status (Markup.markup (task_props Markup.joined) "");
1.11 + val _ = Output.status (Markup.markup_only (task_props Markup.joined));
1.12 in x end;
1.13
1.14
2.1 --- a/src/Pure/General/markup.ML Tue Jul 05 19:11:29 2011 +0200
2.2 +++ b/src/Pure/General/markup.ML Wed Jul 06 09:54:40 2011 +0200
2.3 @@ -92,6 +92,7 @@
2.4 val command_spanN: string val command_span: string -> T
2.5 val ignored_spanN: string val ignored_span: T
2.6 val malformed_spanN: string val malformed_span: T
2.7 + val loaded_theoryN: string val loaded_theory: string -> T
2.8 val elapsedN: string
2.9 val cpuN: string
2.10 val gcN: string
2.11 @@ -110,7 +111,7 @@
2.12 val versionN: string
2.13 val execN: string
2.14 val assignN: string val assign: int -> T
2.15 - val editN: string val edit: int -> int -> T
2.16 + val editN: string val edit: int * int -> T
2.17 val serialN: string
2.18 val promptN: string val prompt: T
2.19 val readyN: string val ready: T
2.20 @@ -123,6 +124,7 @@
2.21 val output: T -> Output.output * Output.output
2.22 val enclose: T -> Output.output -> Output.output
2.23 val markup: T -> string -> string
2.24 + val markup_only: T -> string
2.25 end;
2.26
2.27 structure Markup: MARKUP =
2.28 @@ -304,6 +306,11 @@
2.29 val (malformed_spanN, malformed_span) = markup_elem "malformed_span";
2.30
2.31
2.32 +(* theory loader *)
2.33 +
2.34 +val (loaded_theoryN, loaded_theory) = markup_string "loaded_theory" nameN;
2.35 +
2.36 +
2.37 (* timing *)
2.38
2.39 val timingN = "timing";
2.40 @@ -347,7 +354,7 @@
2.41 val (assignN, assign) = markup_int "assign" versionN;
2.42
2.43 val editN = "edit";
2.44 -fun edit cmd_id exec_id : T = (editN, [(idN, print_int cmd_id), (execN, print_int exec_id)]);
2.45 +fun edit (cmd_id, exec_id) : T = (editN, [(idN, print_int cmd_id), (execN, print_int exec_id)]);
2.46
2.47
2.48 (* messages *)
2.49 @@ -387,4 +394,6 @@
2.50 let val (bg, en) = output m
2.51 in Library.enclose (Output.escape bg) (Output.escape en) end;
2.52
2.53 +fun markup_only m = markup m "";
2.54 +
2.55 end;
3.1 --- a/src/Pure/General/markup.scala Tue Jul 05 19:11:29 2011 +0200
3.2 +++ b/src/Pure/General/markup.scala Wed Jul 06 09:54:40 2011 +0200
3.3 @@ -246,6 +246,11 @@
3.4 val MALFORMED_SPAN = "malformed_span"
3.5
3.6
3.7 + /* theory loader */
3.8 +
3.9 + val LOADED_THEORY = "loaded_theory"
3.10 +
3.11 +
3.12 /* timing */
3.13
3.14 val TIMING = "timing"
4.1 --- a/src/Pure/General/path.scala Tue Jul 05 19:11:29 2011 +0200
4.2 +++ b/src/Pure/General/path.scala Wed Jul 06 09:54:40 2011 +0200
4.3 @@ -82,7 +82,7 @@
4.4
4.5 def explode(str: String): Path =
4.6 {
4.7 - val ss = Library.space_explode('/', str)
4.8 + val ss = space_explode('/', str)
4.9 val r = ss.takeWhile(_.isEmpty).length
4.10 val es = ss.dropWhile(_.isEmpty)
4.11 val (roots, raw_elems) =
4.12 @@ -92,8 +92,12 @@
4.13 else (List(root_elem(es.head)), es.tail)
4.14 Path(norm_elems(explode_elems(raw_elems) ++ roots))
4.15 }
4.16 +
4.17 + def split(str: String): List[Path] =
4.18 + space_explode(':', str).filterNot(_.isEmpty).map(explode)
4.19 }
4.20
4.21 +
4.22 class Path
4.23 {
4.24 protected val elems: List[Path.Elem] = Nil // reversed elements
4.25 @@ -138,11 +142,12 @@
4.26
4.27 /* expand */
4.28
4.29 - def expand(env: String => String): Path =
4.30 + def expand: Path =
4.31 {
4.32 def eval(elem: Path.Elem): List[Path.Elem] =
4.33 elem match {
4.34 - case Path.Variable(s) => Path.explode(env(s)).elems
4.35 + case Path.Variable(s) =>
4.36 + Path.explode(Isabelle_System.getenv_strict(s)).elems
4.37 case x => List(x)
4.38 }
4.39
5.1 --- a/src/Pure/General/symbol.scala Tue Jul 05 19:11:29 2011 +0200
5.2 +++ b/src/Pure/General/symbol.scala Wed Jul 06 09:54:40 2011 +0200
5.3 @@ -64,11 +64,11 @@
5.4
5.5 def is_plain(c: Char): Boolean = !(c == '\r' || c == '\\' || '\ud800' <= c && c <= '\udfff')
5.6
5.7 - def is_physical_newline(s: CharSequence): Boolean =
5.8 - "\n".contentEquals(s) || "\r".contentEquals(s) || "\r\n".contentEquals(s)
5.9 + def is_physical_newline(s: String): Boolean =
5.10 + s == "\n" || s == "\r" || s == "\r\n"
5.11
5.12 - def is_malformed(s: CharSequence): Boolean =
5.13 - !(s.length == 1 && is_plain(s.charAt(0))) && malformed_symbol.pattern.matcher(s).matches
5.14 + def is_malformed(s: String): Boolean =
5.15 + !(s.length == 1 && is_plain(s(0))) && malformed_symbol.pattern.matcher(s).matches
5.16
5.17 class Matcher(text: CharSequence)
5.18 {
5.19 @@ -87,8 +87,11 @@
5.20
5.21 /* efficient iterators */
5.22
5.23 - def iterator(text: CharSequence): Iterator[CharSequence] =
5.24 - new Iterator[CharSequence]
5.25 + private val char_symbols: Array[String] =
5.26 + (0 until 256).iterator.map(i => new String(Array(i.toChar))).toArray
5.27 +
5.28 + def iterator(text: CharSequence): Iterator[String] =
5.29 + new Iterator[String]
5.30 {
5.31 private val matcher = new Matcher(text)
5.32 private var i = 0
5.33 @@ -96,28 +99,19 @@
5.34 def next =
5.35 {
5.36 val n = matcher(i, text.length)
5.37 - val s = text.subSequence(i, i + n)
5.38 + val s =
5.39 + if (n == 0) ""
5.40 + else if (n == 1) {
5.41 + val c = text.charAt(i)
5.42 + if (c < char_symbols.length) char_symbols(c)
5.43 + else text.subSequence(i, i + n).toString
5.44 + }
5.45 + else text.subSequence(i, i + n).toString
5.46 i += n
5.47 s
5.48 }
5.49 }
5.50
5.51 - private val char_symbols: Array[String] =
5.52 - (0 until 128).iterator.map(i => new String(Array(i.toChar))).toArray
5.53 -
5.54 - private def make_string(sym: CharSequence): String =
5.55 - sym.length match {
5.56 - case 0 => ""
5.57 - case 1 =>
5.58 - val c = sym.charAt(0)
5.59 - if (c < char_symbols.length) char_symbols(c)
5.60 - else sym.toString
5.61 - case _ => sym.toString
5.62 - }
5.63 -
5.64 - def iterator_string(text: CharSequence): Iterator[String] =
5.65 - iterator(text).map(make_string)
5.66 -
5.67
5.68 /* decoding offsets */
5.69
6.1 --- a/src/Pure/Isar/toplevel.ML Tue Jul 05 19:11:29 2011 +0200
6.2 +++ b/src/Pure/Isar/toplevel.ML Wed Jul 06 09:54:40 2011 +0200
6.3 @@ -185,8 +185,9 @@
6.4 Proof (prf, _) => Proof_Node.position prf
6.5 | _ => raise UNDEF);
6.6
6.7 -fun end_theory _ (State (NONE, SOME (Theory (Context.Theory thy, _)))) = Theory.end_theory thy
6.8 - | end_theory pos _ = error ("Unfinished theory at end of input" ^ Position.str_of pos);
6.9 +fun end_theory _ (State (NONE, SOME (Theory (Context.Theory thy, _)))) = thy
6.10 + | end_theory pos (State (SOME _, _)) = error ("Unfinished theory " ^ Position.str_of pos)
6.11 + | end_theory pos (State (NONE, NONE)) = error ("Missing theory " ^ Position.str_of pos);
6.12
6.13
6.14 (* print state *)
6.15 @@ -284,6 +285,12 @@
6.16 | SOME exn => raise FAILURE (result', exn))
6.17 end;
6.18
6.19 +val exit_transaction =
6.20 + apply_transaction
6.21 + (fn Theory (Context.Theory thy, _) => Theory (Context.Theory (Theory.end_theory thy), NONE)
6.22 + | node => node) (K ())
6.23 + #> (fn State (node', _) => State (NONE, node'));
6.24 +
6.25 end;
6.26
6.27
6.28 @@ -300,8 +307,8 @@
6.29 fun apply_tr _ (Init (master, _, f)) (State (NONE, _)) =
6.30 State (SOME (Theory (Context.Theory
6.31 (Theory.checkpoint (Runtime.controlled_execution f master)), NONE)), NONE)
6.32 - | apply_tr _ Exit (State (prev as SOME (Theory (Context.Theory _, _)), _)) =
6.33 - State (NONE, prev)
6.34 + | apply_tr _ Exit (State (SOME (state as Theory (Context.Theory _, _)), _)) =
6.35 + exit_transaction state
6.36 | apply_tr int (Keep f) state =
6.37 Runtime.controlled_execution (fn x => tap (f int) x) state
6.38 | apply_tr int (Transaction (f, g)) (State (SOME state, _)) =
6.39 @@ -567,7 +574,7 @@
6.40 Position.setmp_thread_data pos f x;
6.41
6.42 fun status tr m =
6.43 - setmp_thread_position tr (fn () => Output.status (Markup.markup m "")) ();
6.44 + setmp_thread_position tr (fn () => Output.status (Markup.markup_only m)) ();
6.45
6.46 fun error_msg tr msg =
6.47 setmp_thread_position tr (fn () => Output.error_msg msg) ();
7.1 --- a/src/Pure/PIDE/document.ML Tue Jul 05 19:11:29 2011 +0200
7.2 +++ b/src/Pure/PIDE/document.ML Wed Jul 06 09:54:40 2011 +0200
7.3 @@ -18,7 +18,8 @@
7.4 type edit = string * ((command_id option * command_id option) list) option
7.5 type state
7.6 val init_state: state
7.7 - val cancel: state -> unit
7.8 + val get_theory: state -> version_id -> Position.T -> string -> theory
7.9 + val cancel_execution: state -> unit -> unit
7.10 val define_command: command_id -> string -> state -> state
7.11 val edit: version_id -> version_id -> edit list -> state -> (command_id * exec_id) list * state
7.12 val execute: version_id -> state -> state
7.13 @@ -49,16 +50,24 @@
7.14
7.15 structure Entries = Linear_Set(type key = command_id val ord = int_ord);
7.16
7.17 -abstype node = Node of exec_id option Entries.T (*command entries with excecutions*)
7.18 - and version = Version of node Graph.T (*development graph wrt. static imports*)
7.19 +abstype node = Node of
7.20 + {last: exec_id, entries: exec_id option Entries.T} (*command entries with excecutions*)
7.21 +and version = Version of node Graph.T (*development graph wrt. static imports*)
7.22 with
7.23
7.24 -val empty_node = Node Entries.empty;
7.25 +fun make_node (last, entries) =
7.26 + Node {last = last, entries = entries};
7.27 +
7.28 +fun get_last (Node {last, ...}) = last;
7.29 +fun set_last last (Node {entries, ...}) = make_node (last, entries);
7.30 +
7.31 +fun map_entries f (Node {last, entries}) = make_node (last, f entries);
7.32 +fun fold_entries start f (Node {entries, ...}) = Entries.fold start f entries;
7.33 +fun first_entry start P (Node {entries, ...}) = Entries.get_first start P entries;
7.34 +
7.35 +val empty_node = make_node (no_id, Entries.empty);
7.36 val empty_version = Version Graph.empty;
7.37
7.38 -fun fold_entries start f (Node entries) = Entries.fold start f entries;
7.39 -fun first_entry start P (Node entries) = Entries.get_first start P entries;
7.40 -
7.41
7.42 (* node edits and associated executions *)
7.43
7.44 @@ -67,23 +76,22 @@
7.45 (*NONE: remove node, SOME: insert/remove commands*)
7.46 ((command_id option * command_id option) list) option;
7.47
7.48 -fun the_entry (Node entries) id =
7.49 +fun the_entry (Node {entries, ...}) id =
7.50 (case Entries.lookup entries id of
7.51 NONE => err_undef "command entry" id
7.52 | SOME entry => entry);
7.53
7.54 -fun update_entry (id, exec_id) (Node entries) =
7.55 - Node (Entries.update (id, SOME exec_id) entries);
7.56 +fun update_entry (id, exec_id) =
7.57 + map_entries (Entries.update (id, SOME exec_id));
7.58
7.59 fun reset_after id entries =
7.60 (case Entries.get_after entries id of
7.61 NONE => entries
7.62 | SOME next => Entries.update (next, NONE) entries);
7.63
7.64 -fun edit_node (id, SOME id2) (Node entries) =
7.65 - Node (Entries.insert_after id (id2, NONE) entries)
7.66 - | edit_node (id, NONE) (Node entries) =
7.67 - Node (entries |> Entries.delete_after id |> reset_after id);
7.68 +val edit_node = map_entries o fold
7.69 + (fn (id, SOME id2) => Entries.insert_after id (id2, NONE)
7.70 + | (id, NONE) => Entries.delete_after id #> reset_after id);
7.71
7.72
7.73 (* version operations *)
7.74 @@ -97,7 +105,7 @@
7.75 fun edit_nodes (name, SOME edits) (Version nodes) =
7.76 Version (nodes
7.77 |> Graph.default_node (name, empty_node)
7.78 - |> Graph.map_node name (fold edit_node edits))
7.79 + |> Graph.map_node name (edit_node edits))
7.80 | edit_nodes (name, NONE) (Version nodes) =
7.81 Version (perhaps (try (Graph.del_node name)) nodes);
7.82
7.83 @@ -182,14 +190,18 @@
7.84 NONE => err_undef "command execution" id
7.85 | SOME exec => exec);
7.86
7.87 +fun get_theory state version_id pos name =
7.88 + let
7.89 + val last = get_last (get_node (the_version state version_id) name);
7.90 + val st = #2 (Lazy.force (the_exec state last));
7.91 + in Toplevel.end_theory pos st end;
7.92 +
7.93
7.94 (* document execution *)
7.95
7.96 -fun cancel (State {execution, ...}) =
7.97 - List.app Future.cancel execution;
7.98 -
7.99 -fun await_cancellation (State {execution, ...}) =
7.100 - ignore (Future.join_results execution);
7.101 +fun cancel_execution (State {execution, ...}) =
7.102 + (List.app Future.cancel execution;
7.103 + fn () => ignore (Future.join_results execution));
7.104
7.105 end;
7.106
7.107 @@ -311,9 +323,9 @@
7.108 (case prev of
7.109 NONE => no_id
7.110 | SOME prev_id => the_default no_id (the_entry node prev_id));
7.111 - val (_, rev_upds, st') =
7.112 + val (last, rev_upds, st') =
7.113 fold_entries (SOME id) (new_exec name o #2 o #1) node (prev_exec, [], st);
7.114 - val node' = fold update_entry rev_upds node;
7.115 + val node' = node |> fold update_entry rev_upds |> set_last last;
7.116 in (rev_upds @ rev_updates, put_node name node' version, st') end)
7.117 end;
7.118
7.119 @@ -338,20 +350,12 @@
7.120 fun force_exec NONE = ()
7.121 | force_exec (SOME exec_id) = ignore (Lazy.force (the_exec state exec_id));
7.122
7.123 - val _ = cancel state;
7.124 -
7.125 val execution' = (* FIXME proper node deps *)
7.126 Future.forks {name = "Document.execute", group = NONE, deps = [], pri = 1}
7.127 [fn () =>
7.128 - let
7.129 - val _ = await_cancellation state;
7.130 - val _ =
7.131 - node_names_of version |> List.app (fn name =>
7.132 - fold_entries NONE (fn (_, exec) => fn () => force_exec exec)
7.133 - (get_node version name) ());
7.134 - in () end];
7.135 -
7.136 - val _ = await_cancellation state; (* FIXME async!? *)
7.137 + node_names_of version |> List.app (fn name =>
7.138 + fold_entries NONE (fn (_, exec) => fn () => force_exec exec)
7.139 + (get_node version name) ())];
7.140
7.141 in (versions, commands, execs, execution') end);
7.142
8.1 --- a/src/Pure/PIDE/isar_document.ML Tue Jul 05 19:11:29 2011 +0200
8.2 +++ b/src/Pure/PIDE/isar_document.ML Wed Jul 06 09:54:40 2011 +0200
8.3 @@ -4,12 +4,19 @@
8.4 Protocol message formats for interactive Isar documents.
8.5 *)
8.6
8.7 -structure Isar_Document: sig end =
8.8 +signature ISAR_DOCUMENT =
8.9 +sig
8.10 + val state: unit -> Document.state
8.11 +end
8.12 +
8.13 +structure Isar_Document: ISAR_DOCUMENT =
8.14 struct
8.15
8.16 val global_state = Synchronized.var "Isar_Document" Document.init_state;
8.17 val change_state = Synchronized.change global_state;
8.18
8.19 +fun state () = Synchronized.value global_state;
8.20 +
8.21 val _ =
8.22 Isabelle_Process.add_command "Isar_Document.define_command"
8.23 (fn [id, text] => change_state (Document.define_command (Document.parse_id id) text));
8.24 @@ -30,12 +37,12 @@
8.25 (XML_Data.dest_option XML_Data.dest_int)
8.26 (XML_Data.dest_option XML_Data.dest_int))))) (YXML.parse_body edits_yxml);
8.27
8.28 - val _ = Document.cancel state;
8.29 + val await_cancellation = Document.cancel_execution state;
8.30 val (updates, state') = Document.edit old_id new_id edits state;
8.31 + val _ = await_cancellation ();
8.32 val _ =
8.33 - implode (map (fn (id, exec_id) => Markup.markup (Markup.edit id exec_id) "") updates)
8.34 - |> Markup.markup (Markup.assign new_id)
8.35 - |> Output.status;
8.36 + Output.status (Markup.markup (Markup.assign new_id)
8.37 + (implode (map (Markup.markup_only o Markup.edit) updates)));
8.38 val state'' = Document.execute new_id state';
8.39 in state'' end));
8.40
9.1 --- a/src/Pure/System/isabelle_process.ML Tue Jul 05 19:11:29 2011 +0200
9.2 +++ b/src/Pure/System/isabelle_process.ML Wed Jul 06 09:54:40 2011 +0200
9.3 @@ -173,11 +173,14 @@
9.4 val _ = quick_and_dirty := true;
9.5 val _ = Goal.parallel_proofs := 0;
9.6 val _ = Context.set_thread_data NONE;
9.7 - val _ = Unsynchronized.change print_mode
9.8 - (fold (update op =) [isabelle_processN, Keyword.keyword_statusN, Pretty.symbolicN]);
9.9 + val _ =
9.10 + Unsynchronized.change print_mode
9.11 + (fold (update op =)
9.12 + [Symbol.xsymbolsN, isabelle_processN, Keyword.keyword_statusN, Pretty.symbolicN]);
9.13
9.14 val in_stream = setup_channels in_fifo out_fifo;
9.15 val _ = Keyword.status ();
9.16 + val _ = Thy_Info.status ();
9.17 val _ = Output.status (Markup.markup Markup.ready "process ready");
9.18 in loop in_stream end));
9.19
10.1 --- a/src/Pure/System/isabelle_system.scala Tue Jul 05 19:11:29 2011 +0200
10.2 +++ b/src/Pure/System/isabelle_system.scala Wed Jul 06 09:54:40 2011 +0200
10.3 @@ -95,8 +95,8 @@
10.4 val isabelle_symbols = settings.getOrElse("ISABELLE_SYMBOLS", "")
10.5 if (isabelle_symbols == "") error("Undefined environment variable: ISABELLE_SYMBOLS")
10.6 val files =
10.7 - isabelle_symbols.split(":").toList.map(s => new File(standard_system.jvm_path(s)))
10.8 - new Symbol.Interpretation(Standard_System.try_read(files).split("\n").toList)
10.9 + Path.split(isabelle_symbols).map(p => new File(standard_system.jvm_path(p.implode)))
10.10 + new Symbol.Interpretation(split_lines(Standard_System.try_read(files)))
10.11 }
10.12
10.13 _state = Some(State(standard_system, settings, symbols))
10.14 @@ -120,7 +120,7 @@
10.15
10.16 /* path specifications */
10.17
10.18 - def standard_path(path: Path): String = path.expand(getenv_strict).implode
10.19 + def standard_path(path: Path): String = path.expand.implode
10.20
10.21 def platform_path(path: Path): String = standard_system.jvm_path(standard_path(path))
10.22 def platform_file(path: Path) = new File(platform_path(path))
10.23 @@ -265,8 +265,8 @@
10.24
10.25 def isabelle_tool(name: String, args: String*): (String, Int) =
10.26 {
10.27 - getenv_strict("ISABELLE_TOOLS").split(":").find { dir =>
10.28 - val file = platform_file(Path.explode(dir) + Path.basic(name))
10.29 + Path.split(getenv_strict("ISABELLE_TOOLS")).find { dir =>
10.30 + val file = platform_file(dir + Path.basic(name))
10.31 try {
10.32 file.isFile && file.canRead && file.canExecute &&
10.33 !name.endsWith("~") && !name.endsWith(".orig")
10.34 @@ -274,7 +274,7 @@
10.35 catch { case _: SecurityException => false }
10.36 } match {
10.37 case Some(dir) =>
10.38 - val file = standard_path(Path.explode(dir) + Path.basic(name))
10.39 + val file = standard_path(dir + Path.basic(name))
10.40 Standard_System.process_output(execute(true, (List(file) ++ args): _*))
10.41 case None => ("Unknown Isabelle tool: " + name, 2)
10.42 }
10.43 @@ -334,8 +334,8 @@
10.44
10.45 /* components */
10.46
10.47 - def components(): List[String] =
10.48 - getenv_strict("ISABELLE_COMPONENTS").split(":").toList
10.49 + def components(): List[Path] =
10.50 + Path.split(getenv_strict("ISABELLE_COMPONENTS"))
10.51
10.52
10.53 /* find logics */
10.54 @@ -344,8 +344,8 @@
10.55 {
10.56 val ml_ident = getenv_strict("ML_IDENTIFIER")
10.57 val logics = new mutable.ListBuffer[String]
10.58 - for (dir <- getenv_strict("ISABELLE_PATH").split(":")) {
10.59 - val files = platform_file(Path.explode(dir) + Path.explode(ml_ident)).listFiles()
10.60 + for (dir <- Path.split(getenv_strict("ISABELLE_PATH"))) {
10.61 + val files = platform_file(dir + Path.explode(ml_ident)).listFiles()
10.62 if (files != null) {
10.63 for (file <- files if file.isFile) logics += file.getName
10.64 }
10.65 @@ -362,7 +362,7 @@
10.66 def install_fonts()
10.67 {
10.68 val ge = GraphicsEnvironment.getLocalGraphicsEnvironment()
10.69 - for (font <- getenv_strict("ISABELLE_FONTS").split(":"))
10.70 - ge.registerFont(Font.createFont(Font.TRUETYPE_FONT, platform_file(Path.explode(font))))
10.71 + for (font <- Path.split(getenv_strict("ISABELLE_FONTS")))
10.72 + ge.registerFont(Font.createFont(Font.TRUETYPE_FONT, platform_file(font)))
10.73 }
10.74 }
11.1 --- a/src/Pure/System/session.scala Tue Jul 05 19:11:29 2011 +0200
11.2 +++ b/src/Pure/System/session.scala Wed Jul 06 09:54:40 2011 +0200
11.3 @@ -115,6 +115,8 @@
11.4
11.5 /* global state */
11.6
11.7 + @volatile var loaded_theories: Set[String] = Set()
11.8 +
11.9 @volatile private var syntax = new Outer_Syntax(Isabelle_System.symbols)
11.10 def current_syntax(): Outer_Syntax = syntax
11.11
11.12 @@ -138,6 +140,9 @@
11.13
11.14 val thy_load = new Thy_Load
11.15 {
11.16 + override def is_loaded(name: String): Boolean =
11.17 + loaded_theories.contains(name)
11.18 +
11.19 override def check_thy(dir: Path, name: String): (String, Thy_Header.Header) =
11.20 {
11.21 val file = Isabelle_System.platform_file(dir + Thy_Header.thy_path(name))
11.22 @@ -255,6 +260,7 @@
11.23 catch { case _: Document.State.Fail => bad_result(result) }
11.24 case List(Keyword.Command_Decl(name, kind)) => syntax += (name, kind)
11.25 case List(Keyword.Keyword_Decl(name)) => syntax += name
11.26 + case List(Thy_Info.Loaded_Theory(name)) => loaded_theories += name
11.27 case _ => bad_result(result)
11.28 }
11.29 }
12.1 --- a/src/Pure/System/session_manager.scala Tue Jul 05 19:11:29 2011 +0200
12.2 +++ b/src/Pure/System/session_manager.scala Wed Jul 06 09:54:40 2011 +0200
12.3 @@ -42,8 +42,7 @@
12.4 def component_sessions(): List[List[String]] =
12.5 {
12.6 val toplevel_sessions =
12.7 - Isabelle_System.components().map(s =>
12.8 - Isabelle_System.platform_file(Path.explode(s))).filter(is_session_dir)
12.9 + Isabelle_System.components().map(Isabelle_System.platform_file).filter(is_session_dir)
12.10 ((Nil: List[List[String]]) /: toplevel_sessions)(find_sessions(Nil, _, _)).reverse
12.11 }
12.12 }
13.1 --- a/src/Pure/System/standard_system.scala Tue Jul 05 19:11:29 2011 +0200
13.2 +++ b/src/Pure/System/standard_system.scala Wed Jul 06 09:54:40 2011 +0200
13.3 @@ -264,8 +264,9 @@
13.4
13.5 class Standard_System
13.6 {
13.7 + /* platform_root */
13.8 +
13.9 val platform_root = if (Platform.is_windows) Cygwin.check_root() else "/"
13.10 - override def toString = platform_root
13.11
13.12
13.13 /* jvm_path */
13.14 @@ -291,7 +292,7 @@
13.15 path
13.16 case path => path
13.17 }
13.18 - for (p <- rest.split("/") if p != "") {
13.19 + for (p <- space_explode('/', rest) if p != "") {
13.20 val len = result_path.length
13.21 if (len > 0 && result_path(len - 1) != File.separatorChar)
13.22 result_path += File.separatorChar
14.1 --- a/src/Pure/Thy/html.scala Tue Jul 05 19:11:29 2011 +0200
14.2 +++ b/src/Pure/Thy/html.scala Wed Jul 06 09:54:40 2011 +0200
14.3 @@ -80,7 +80,7 @@
14.4 flush()
14.5 ts += elem
14.6 }
14.7 - val syms = Symbol.iterator_string(txt)
14.8 + val syms = Symbol.iterator(txt)
14.9 while (syms.hasNext) {
14.10 val s1 = syms.next
14.11 def s2() = if (syms.hasNext) syms.next else ""
15.1 --- a/src/Pure/Thy/thy_header.scala Tue Jul 05 19:11:29 2011 +0200
15.2 +++ b/src/Pure/Thy/thy_header.scala Wed Jul 06 09:54:40 2011 +0200
15.3 @@ -112,7 +112,8 @@
15.4 {
15.5 val header = read(source)
15.6 val name1 = header.name
15.7 - if (name == name1) header
15.8 - else error("Bad file name " + thy_path(name) + " for theory " + quote(name1))
15.9 + if (name != name1) error("Bad file name " + thy_path(name) + " for theory " + quote(name1))
15.10 + Path.explode(name)
15.11 + header
15.12 }
15.13 }
16.1 --- a/src/Pure/Thy/thy_info.ML Tue Jul 05 19:11:29 2011 +0200
16.2 +++ b/src/Pure/Thy/thy_info.ML Wed Jul 06 09:54:40 2011 +0200
16.3 @@ -10,6 +10,7 @@
16.4 datatype action = Update | Remove
16.5 val add_hook: (action -> string -> unit) -> unit
16.6 val get_names: unit -> string list
16.7 + val status: unit -> unit
16.8 val lookup_theory: string -> theory option
16.9 val get_theory: string -> theory
16.10 val is_finished: string -> bool
16.11 @@ -88,6 +89,9 @@
16.12
16.13 fun get_names () = Graph.topological_order (get_thys ());
16.14
16.15 +fun status () =
16.16 + List.app (Output.status o Markup.markup_only o Markup.loaded_theory) (get_names ());
16.17 +
16.18
16.19 (* access thy *)
16.20
17.1 --- a/src/Pure/Thy/thy_info.scala Tue Jul 05 19:11:29 2011 +0200
17.2 +++ b/src/Pure/Thy/thy_info.scala Wed Jul 06 09:54:40 2011 +0200
17.3 @@ -7,6 +7,20 @@
17.4 package isabelle
17.5
17.6
17.7 +object Thy_Info
17.8 +{
17.9 + /* protocol messages */
17.10 +
17.11 + object Loaded_Theory {
17.12 + def unapply(msg: XML.Tree): Option[String] =
17.13 + msg match {
17.14 + case XML.Elem(Markup(Markup.LOADED_THEORY, List((Markup.NAME, name))), _) => Some(name)
17.15 + case _ => None
17.16 + }
17.17 + }
17.18 +}
17.19 +
17.20 +
17.21 class Thy_Info(thy_load: Thy_Load)
17.22 {
17.23 /* messages */
17.24 @@ -26,16 +40,17 @@
17.25
17.26 type Deps = Map[String, Exn.Result[(String, Thy_Header.Header)]] // name -> (text, header)
17.27
17.28 - private def require_thys(
17.29 + private def require_thys(ignored: String => Boolean,
17.30 initiators: List[String], dir: Path, deps: Deps, strs: List[String]): Deps =
17.31 - (deps /: strs)(require_thy(initiators, dir, _, _))
17.32 + (deps /: strs)(require_thy(ignored, initiators, dir, _, _))
17.33
17.34 - private def require_thy(initiators: List[String], dir: Path, deps: Deps, str: String): Deps =
17.35 + private def require_thy(ignored: String => Boolean,
17.36 + initiators: List[String], dir: Path, deps: Deps, str: String): Deps =
17.37 {
17.38 val path = Path.explode(str)
17.39 val name = path.base.implode
17.40
17.41 - if (deps.isDefinedAt(name)) deps
17.42 + if (deps.isDefinedAt(name) || ignored(name)) deps
17.43 else {
17.44 val dir1 = dir + path.dir
17.45 try {
17.46 @@ -47,7 +62,7 @@
17.47 cat_error(msg, "The error(s) above occurred while examining theory " +
17.48 quote(name) + required_by("\n", initiators))
17.49 }
17.50 - require_thys(name :: initiators, dir1,
17.51 + require_thys(ignored, name :: initiators, dir1,
17.52 deps + (name -> Exn.Res(text, header)), header.imports)
17.53 }
17.54 catch { case e: Throwable => deps + (name -> Exn.Exn(e)) }
17.55 @@ -55,5 +70,5 @@
17.56 }
17.57
17.58 def dependencies(dir: Path, str: String): Deps =
17.59 - require_thy(Nil, dir, Map.empty, str) // FIXME capture errors in str (!??)
17.60 + require_thy(thy_load.is_loaded, Nil, dir, Map.empty, str)
17.61 }
18.1 --- a/src/Pure/Thy/thy_load.scala Tue Jul 05 19:11:29 2011 +0200
18.2 +++ b/src/Pure/Thy/thy_load.scala Wed Jul 06 09:54:40 2011 +0200
18.3 @@ -8,6 +8,8 @@
18.4
18.5 abstract class Thy_Load
18.6 {
18.7 + def is_loaded(name: String): Boolean
18.8 +
18.9 def check_thy(dir: Path, name: String): (String, Thy_Header.Header)
18.10 }
18.11
19.1 --- a/src/Pure/library.scala Tue Jul 05 19:11:29 2011 +0200
19.2 +++ b/src/Pure/library.scala Wed Jul 06 09:54:40 2011 +0200
19.3 @@ -61,6 +61,8 @@
19.4 result.toList
19.5 }
19.6
19.7 + def split_lines(str: String): List[String] = space_explode('\n', str)
19.8 +
19.9
19.10 /* iterate over chunks (cf. space_explode) */
19.11
19.12 @@ -185,13 +187,14 @@
19.13
19.14 class Basic_Library
19.15 {
19.16 + val ERROR = Library.ERROR
19.17 + val error = Library.error _
19.18 + val cat_error = Library.cat_error _
19.19 +
19.20 val space_explode = Library.space_explode _
19.21 + val split_lines = Library.split_lines _
19.22
19.23 val quote = Library.quote _
19.24 val commas = Library.commas _
19.25 val commas_quote = Library.commas_quote _
19.26 -
19.27 - val ERROR = Library.ERROR
19.28 - val error = Library.error _
19.29 - val cat_error = Library.cat_error _
19.30 }
20.1 --- a/src/Tools/jEdit/etc/settings Tue Jul 05 19:11:29 2011 +0200
20.2 +++ b/src/Tools/jEdit/etc/settings Wed Jul 06 09:54:40 2011 +0200
20.3 @@ -10,7 +10,7 @@
20.4
20.5 JEDIT_STYLE_SHEETS="$ISABELLE_HOME/etc/isabelle.css:$JEDIT_HOME/etc/isabelle-jedit.css:$ISABELLE_HOME_USER/etc/isabelle.css:$ISABELLE_HOME_USER/etc/isabelle-jedit.css"
20.6
20.7 -ISABELLE_JEDIT_OPTIONS="-m xsymbols -m no_brackets -m no_type_brackets"
20.8 +ISABELLE_JEDIT_OPTIONS="-m no_brackets -m no_type_brackets"
20.9
20.10 ISABELLE_TOOLS="$ISABELLE_TOOLS:$JEDIT_HOME/lib/Tools"
20.11
21.1 --- a/src/Tools/jEdit/src/html_panel.scala Tue Jul 05 19:11:29 2011 +0200
21.2 +++ b/src/Tools/jEdit/src/html_panel.scala Wed Jul 06 09:54:40 2011 +0200
21.3 @@ -92,8 +92,7 @@
21.4 <head>
21.5 <style media="all" type="text/css">
21.6 """ +
21.7 - Isabelle_System.try_read(
21.8 - Isabelle_System.getenv_strict("JEDIT_STYLE_SHEETS").split(":").map(Path.explode))
21.9 + Isabelle_System.try_read(Path.split(Isabelle_System.getenv_strict("JEDIT_STYLE_SHEETS")))
21.10
21.11 private val template_tail =
21.12 """
22.1 --- a/src/Tools/jEdit/src/plugin.scala Tue Jul 05 19:11:29 2011 +0200
22.2 +++ b/src/Tools/jEdit/src/plugin.scala Wed Jul 06 09:54:40 2011 +0200
22.3 @@ -300,7 +300,7 @@
22.4 def start_session()
22.5 {
22.6 val timeout = Time_Property("startup-timeout", Time.seconds(10)) max Time.seconds(5)
22.7 - val modes = Isabelle_System.getenv("JEDIT_PRINT_MODE").split(",").toList.map("-m" + _)
22.8 + val modes = space_explode(',', Isabelle_System.getenv("JEDIT_PRINT_MODE")).map("-m" + _)
22.9 val logic = {
22.10 val logic = Property("logic")
22.11 if (logic != null && logic != "") logic
23.1 --- a/src/Tools/jEdit/src/token_markup.scala Tue Jul 05 19:11:29 2011 +0200
23.2 +++ b/src/Tools/jEdit/src/token_markup.scala Wed Jul 06 09:54:40 2011 +0200
23.3 @@ -124,7 +124,7 @@
23.4 }
23.5 var offset = 0
23.6 var ctrl = ""
23.7 - for (sym <- Symbol.iterator_string(text)) {
23.8 + for (sym <- Symbol.iterator(text)) {
23.9 if (ctrl_style(sym).isDefined) ctrl = sym
23.10 else if (ctrl != "") {
23.11 if (symbols.is_controllable(sym) && sym != "\"" && !symbols.fonts.isDefinedAt(sym)) {