--- a/src/Pure/Concurrent/future.ML Tue Jul 05 19:11:29 2011 +0200
+++ b/src/Pure/Concurrent/future.ML Wed Jul 06 09:54:40 2011 +0200
@@ -584,9 +584,9 @@
(case worker_task () of
NONE => I
| SOME task => Markup.properties [(Markup.taskN, Task_Queue.str_of_task task)]);
- val _ = Output.status (Markup.markup (task_props Markup.forked) "");
+ val _ = Output.status (Markup.markup_only (task_props Markup.forked));
val x = e (); (*sic -- report "joined" only for success*)
- val _ = Output.status (Markup.markup (task_props Markup.joined) "");
+ val _ = Output.status (Markup.markup_only (task_props Markup.joined));
in x end;
--- a/src/Pure/General/markup.ML Tue Jul 05 19:11:29 2011 +0200
+++ b/src/Pure/General/markup.ML Wed Jul 06 09:54:40 2011 +0200
@@ -92,6 +92,7 @@
val command_spanN: string val command_span: string -> T
val ignored_spanN: string val ignored_span: T
val malformed_spanN: string val malformed_span: T
+ val loaded_theoryN: string val loaded_theory: string -> T
val elapsedN: string
val cpuN: string
val gcN: string
@@ -110,7 +111,7 @@
val versionN: string
val execN: string
val assignN: string val assign: int -> T
- val editN: string val edit: int -> int -> T
+ val editN: string val edit: int * int -> T
val serialN: string
val promptN: string val prompt: T
val readyN: string val ready: T
@@ -123,6 +124,7 @@
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 =
@@ -304,6 +306,11 @@
val (malformed_spanN, malformed_span) = markup_elem "malformed_span";
+(* theory loader *)
+
+val (loaded_theoryN, loaded_theory) = markup_string "loaded_theory" nameN;
+
+
(* timing *)
val timingN = "timing";
@@ -347,7 +354,7 @@
val (assignN, assign) = markup_int "assign" versionN;
val editN = "edit";
-fun edit cmd_id exec_id : T = (editN, [(idN, print_int cmd_id), (execN, print_int exec_id)]);
+fun edit (cmd_id, exec_id) : T = (editN, [(idN, print_int cmd_id), (execN, print_int exec_id)]);
(* messages *)
@@ -387,4 +394,6 @@
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 Jul 05 19:11:29 2011 +0200
+++ b/src/Pure/General/markup.scala Wed Jul 06 09:54:40 2011 +0200
@@ -246,6 +246,11 @@
val MALFORMED_SPAN = "malformed_span"
+ /* theory loader */
+
+ val LOADED_THEORY = "loaded_theory"
+
+
/* timing */
val TIMING = "timing"
--- a/src/Pure/General/path.scala Tue Jul 05 19:11:29 2011 +0200
+++ b/src/Pure/General/path.scala Wed Jul 06 09:54:40 2011 +0200
@@ -82,7 +82,7 @@
def explode(str: String): Path =
{
- val ss = Library.space_explode('/', str)
+ val ss = space_explode('/', str)
val r = ss.takeWhile(_.isEmpty).length
val es = ss.dropWhile(_.isEmpty)
val (roots, raw_elems) =
@@ -92,8 +92,12 @@
else (List(root_elem(es.head)), es.tail)
Path(norm_elems(explode_elems(raw_elems) ++ roots))
}
+
+ def split(str: String): List[Path] =
+ space_explode(':', str).filterNot(_.isEmpty).map(explode)
}
+
class Path
{
protected val elems: List[Path.Elem] = Nil // reversed elements
@@ -138,11 +142,12 @@
/* expand */
- def expand(env: String => String): Path =
+ def expand: Path =
{
def eval(elem: Path.Elem): List[Path.Elem] =
elem match {
- case Path.Variable(s) => Path.explode(env(s)).elems
+ case Path.Variable(s) =>
+ Path.explode(Isabelle_System.getenv_strict(s)).elems
case x => List(x)
}
--- a/src/Pure/General/symbol.scala Tue Jul 05 19:11:29 2011 +0200
+++ b/src/Pure/General/symbol.scala Wed Jul 06 09:54:40 2011 +0200
@@ -64,11 +64,11 @@
def is_plain(c: Char): Boolean = !(c == '\r' || c == '\\' || '\ud800' <= c && c <= '\udfff')
- def is_physical_newline(s: CharSequence): Boolean =
- "\n".contentEquals(s) || "\r".contentEquals(s) || "\r\n".contentEquals(s)
+ def is_physical_newline(s: String): Boolean =
+ s == "\n" || s == "\r" || s == "\r\n"
- def is_malformed(s: CharSequence): Boolean =
- !(s.length == 1 && is_plain(s.charAt(0))) && malformed_symbol.pattern.matcher(s).matches
+ def is_malformed(s: String): Boolean =
+ !(s.length == 1 && is_plain(s(0))) && malformed_symbol.pattern.matcher(s).matches
class Matcher(text: CharSequence)
{
@@ -87,8 +87,11 @@
/* efficient iterators */
- def iterator(text: CharSequence): Iterator[CharSequence] =
- new Iterator[CharSequence]
+ private val char_symbols: Array[String] =
+ (0 until 256).iterator.map(i => new String(Array(i.toChar))).toArray
+
+ def iterator(text: CharSequence): Iterator[String] =
+ new Iterator[String]
{
private val matcher = new Matcher(text)
private var i = 0
@@ -96,28 +99,19 @@
def next =
{
val n = matcher(i, text.length)
- val s = text.subSequence(i, i + n)
+ val s =
+ if (n == 0) ""
+ else if (n == 1) {
+ val c = text.charAt(i)
+ if (c < char_symbols.length) char_symbols(c)
+ else text.subSequence(i, i + n).toString
+ }
+ else text.subSequence(i, i + n).toString
i += n
s
}
}
- private val char_symbols: Array[String] =
- (0 until 128).iterator.map(i => new String(Array(i.toChar))).toArray
-
- private def make_string(sym: CharSequence): String =
- sym.length match {
- case 0 => ""
- case 1 =>
- val c = sym.charAt(0)
- if (c < char_symbols.length) char_symbols(c)
- else sym.toString
- case _ => sym.toString
- }
-
- def iterator_string(text: CharSequence): Iterator[String] =
- iterator(text).map(make_string)
-
/* decoding offsets */
--- a/src/Pure/Isar/toplevel.ML Tue Jul 05 19:11:29 2011 +0200
+++ b/src/Pure/Isar/toplevel.ML Wed Jul 06 09:54:40 2011 +0200
@@ -185,8 +185,9 @@
Proof (prf, _) => Proof_Node.position prf
| _ => raise UNDEF);
-fun end_theory _ (State (NONE, SOME (Theory (Context.Theory thy, _)))) = Theory.end_theory thy
- | end_theory pos _ = error ("Unfinished theory at end of input" ^ Position.str_of pos);
+fun end_theory _ (State (NONE, SOME (Theory (Context.Theory thy, _)))) = thy
+ | end_theory pos (State (SOME _, _)) = error ("Unfinished theory " ^ Position.str_of pos)
+ | end_theory pos (State (NONE, NONE)) = error ("Missing theory " ^ Position.str_of pos);
(* print state *)
@@ -284,6 +285,12 @@
| SOME exn => raise FAILURE (result', exn))
end;
+val exit_transaction =
+ apply_transaction
+ (fn Theory (Context.Theory thy, _) => Theory (Context.Theory (Theory.end_theory thy), NONE)
+ | node => node) (K ())
+ #> (fn State (node', _) => State (NONE, node'));
+
end;
@@ -300,8 +307,8 @@
fun apply_tr _ (Init (master, _, f)) (State (NONE, _)) =
State (SOME (Theory (Context.Theory
(Theory.checkpoint (Runtime.controlled_execution f master)), NONE)), NONE)
- | apply_tr _ Exit (State (prev as SOME (Theory (Context.Theory _, _)), _)) =
- State (NONE, prev)
+ | apply_tr _ Exit (State (SOME (state as Theory (Context.Theory _, _)), _)) =
+ exit_transaction state
| apply_tr int (Keep f) state =
Runtime.controlled_execution (fn x => tap (f int) x) state
| apply_tr int (Transaction (f, g)) (State (SOME state, _)) =
@@ -567,7 +574,7 @@
Position.setmp_thread_data pos f x;
fun status tr m =
- setmp_thread_position tr (fn () => Output.status (Markup.markup m "")) ();
+ setmp_thread_position tr (fn () => Output.status (Markup.markup_only m)) ();
fun error_msg tr msg =
setmp_thread_position tr (fn () => Output.error_msg msg) ();
--- a/src/Pure/PIDE/document.ML Tue Jul 05 19:11:29 2011 +0200
+++ b/src/Pure/PIDE/document.ML Wed Jul 06 09:54:40 2011 +0200
@@ -18,7 +18,8 @@
type edit = string * ((command_id option * command_id option) list) option
type state
val init_state: state
- val cancel: state -> unit
+ val get_theory: state -> version_id -> Position.T -> string -> theory
+ val cancel_execution: state -> unit -> unit
val define_command: command_id -> string -> state -> state
val edit: version_id -> version_id -> edit list -> state -> (command_id * exec_id) list * state
val execute: version_id -> state -> state
@@ -49,15 +50,23 @@
structure Entries = Linear_Set(type key = command_id val ord = int_ord);
-abstype node = Node of exec_id option Entries.T (*command entries with excecutions*)
- and version = Version of node Graph.T (*development graph wrt. static imports*)
+abstype node = Node of
+ {last: exec_id, entries: exec_id option Entries.T} (*command entries with excecutions*)
+and version = Version of node Graph.T (*development graph wrt. static imports*)
with
-val empty_node = Node Entries.empty;
-val empty_version = Version Graph.empty;
+fun make_node (last, entries) =
+ Node {last = last, entries = entries};
+
+fun get_last (Node {last, ...}) = last;
+fun set_last last (Node {entries, ...}) = make_node (last, entries);
-fun fold_entries start f (Node entries) = Entries.fold start f entries;
-fun first_entry start P (Node entries) = Entries.get_first start P entries;
+fun map_entries f (Node {last, entries}) = make_node (last, f entries);
+fun fold_entries start f (Node {entries, ...}) = Entries.fold start f entries;
+fun first_entry start P (Node {entries, ...}) = Entries.get_first start P entries;
+
+val empty_node = make_node (no_id, Entries.empty);
+val empty_version = Version Graph.empty;
(* node edits and associated executions *)
@@ -67,23 +76,22 @@
(*NONE: remove node, SOME: insert/remove commands*)
((command_id option * command_id option) list) option;
-fun the_entry (Node entries) id =
+fun the_entry (Node {entries, ...}) id =
(case Entries.lookup entries id of
NONE => err_undef "command entry" id
| SOME entry => entry);
-fun update_entry (id, exec_id) (Node entries) =
- Node (Entries.update (id, SOME exec_id) entries);
+fun update_entry (id, exec_id) =
+ map_entries (Entries.update (id, SOME exec_id));
fun reset_after id entries =
(case Entries.get_after entries id of
NONE => entries
| SOME next => Entries.update (next, NONE) entries);
-fun edit_node (id, SOME id2) (Node entries) =
- Node (Entries.insert_after id (id2, NONE) entries)
- | edit_node (id, NONE) (Node entries) =
- Node (entries |> Entries.delete_after id |> reset_after id);
+val edit_node = map_entries o fold
+ (fn (id, SOME id2) => Entries.insert_after id (id2, NONE)
+ | (id, NONE) => Entries.delete_after id #> reset_after id);
(* version operations *)
@@ -97,7 +105,7 @@
fun edit_nodes (name, SOME edits) (Version nodes) =
Version (nodes
|> Graph.default_node (name, empty_node)
- |> Graph.map_node name (fold edit_node edits))
+ |> Graph.map_node name (edit_node edits))
| edit_nodes (name, NONE) (Version nodes) =
Version (perhaps (try (Graph.del_node name)) nodes);
@@ -182,14 +190,18 @@
NONE => err_undef "command execution" id
| SOME exec => exec);
+fun get_theory state version_id pos name =
+ let
+ val last = get_last (get_node (the_version state version_id) name);
+ val st = #2 (Lazy.force (the_exec state last));
+ in Toplevel.end_theory pos st end;
+
(* document execution *)
-fun cancel (State {execution, ...}) =
- List.app Future.cancel execution;
-
-fun await_cancellation (State {execution, ...}) =
- ignore (Future.join_results execution);
+fun cancel_execution (State {execution, ...}) =
+ (List.app Future.cancel execution;
+ fn () => ignore (Future.join_results execution));
end;
@@ -311,9 +323,9 @@
(case prev of
NONE => no_id
| SOME prev_id => the_default no_id (the_entry node prev_id));
- val (_, rev_upds, st') =
+ val (last, rev_upds, st') =
fold_entries (SOME id) (new_exec name o #2 o #1) node (prev_exec, [], st);
- val node' = fold update_entry rev_upds node;
+ val node' = node |> fold update_entry rev_upds |> set_last last;
in (rev_upds @ rev_updates, put_node name node' version, st') end)
end;
@@ -338,20 +350,12 @@
fun force_exec NONE = ()
| force_exec (SOME exec_id) = ignore (Lazy.force (the_exec state exec_id));
- val _ = cancel state;
-
val execution' = (* FIXME proper node deps *)
Future.forks {name = "Document.execute", group = NONE, deps = [], pri = 1}
[fn () =>
- let
- val _ = await_cancellation state;
- val _ =
- node_names_of version |> List.app (fn name =>
- fold_entries NONE (fn (_, exec) => fn () => force_exec exec)
- (get_node version name) ());
- in () end];
-
- val _ = await_cancellation state; (* FIXME async!? *)
+ node_names_of version |> List.app (fn name =>
+ fold_entries NONE (fn (_, exec) => fn () => force_exec exec)
+ (get_node version name) ())];
in (versions, commands, execs, execution') end);
--- a/src/Pure/PIDE/isar_document.ML Tue Jul 05 19:11:29 2011 +0200
+++ b/src/Pure/PIDE/isar_document.ML Wed Jul 06 09:54:40 2011 +0200
@@ -4,12 +4,19 @@
Protocol message formats for interactive Isar documents.
*)
-structure Isar_Document: sig end =
+signature ISAR_DOCUMENT =
+sig
+ val state: unit -> Document.state
+end
+
+structure Isar_Document: ISAR_DOCUMENT =
struct
val global_state = Synchronized.var "Isar_Document" Document.init_state;
val change_state = Synchronized.change global_state;
+fun state () = Synchronized.value global_state;
+
val _ =
Isabelle_Process.add_command "Isar_Document.define_command"
(fn [id, text] => change_state (Document.define_command (Document.parse_id id) text));
@@ -30,12 +37,12 @@
(XML_Data.dest_option XML_Data.dest_int)
(XML_Data.dest_option XML_Data.dest_int))))) (YXML.parse_body edits_yxml);
- val _ = Document.cancel state;
+ val await_cancellation = Document.cancel_execution state;
val (updates, state') = Document.edit old_id new_id edits state;
+ val _ = await_cancellation ();
val _ =
- implode (map (fn (id, exec_id) => Markup.markup (Markup.edit id exec_id) "") updates)
- |> Markup.markup (Markup.assign new_id)
- |> Output.status;
+ Output.status (Markup.markup (Markup.assign new_id)
+ (implode (map (Markup.markup_only o Markup.edit) updates)));
val state'' = Document.execute new_id state';
in state'' end));
--- a/src/Pure/System/isabelle_process.ML Tue Jul 05 19:11:29 2011 +0200
+++ b/src/Pure/System/isabelle_process.ML Wed Jul 06 09:54:40 2011 +0200
@@ -173,11 +173,14 @@
val _ = quick_and_dirty := true;
val _ = Goal.parallel_proofs := 0;
val _ = Context.set_thread_data NONE;
- val _ = Unsynchronized.change print_mode
- (fold (update op =) [isabelle_processN, Keyword.keyword_statusN, Pretty.symbolicN]);
+ val _ =
+ Unsynchronized.change print_mode
+ (fold (update op =)
+ [Symbol.xsymbolsN, isabelle_processN, Keyword.keyword_statusN, Pretty.symbolicN]);
val in_stream = setup_channels in_fifo out_fifo;
val _ = Keyword.status ();
+ val _ = Thy_Info.status ();
val _ = Output.status (Markup.markup Markup.ready "process ready");
in loop in_stream end));
--- a/src/Pure/System/isabelle_system.scala Tue Jul 05 19:11:29 2011 +0200
+++ b/src/Pure/System/isabelle_system.scala Wed Jul 06 09:54:40 2011 +0200
@@ -95,8 +95,8 @@
val isabelle_symbols = settings.getOrElse("ISABELLE_SYMBOLS", "")
if (isabelle_symbols == "") error("Undefined environment variable: ISABELLE_SYMBOLS")
val files =
- isabelle_symbols.split(":").toList.map(s => new File(standard_system.jvm_path(s)))
- new Symbol.Interpretation(Standard_System.try_read(files).split("\n").toList)
+ Path.split(isabelle_symbols).map(p => new File(standard_system.jvm_path(p.implode)))
+ new Symbol.Interpretation(split_lines(Standard_System.try_read(files)))
}
_state = Some(State(standard_system, settings, symbols))
@@ -120,7 +120,7 @@
/* path specifications */
- def standard_path(path: Path): String = path.expand(getenv_strict).implode
+ def standard_path(path: Path): String = path.expand.implode
def platform_path(path: Path): String = standard_system.jvm_path(standard_path(path))
def platform_file(path: Path) = new File(platform_path(path))
@@ -265,8 +265,8 @@
def isabelle_tool(name: String, args: String*): (String, Int) =
{
- getenv_strict("ISABELLE_TOOLS").split(":").find { dir =>
- val file = platform_file(Path.explode(dir) + Path.basic(name))
+ Path.split(getenv_strict("ISABELLE_TOOLS")).find { dir =>
+ val file = platform_file(dir + Path.basic(name))
try {
file.isFile && file.canRead && file.canExecute &&
!name.endsWith("~") && !name.endsWith(".orig")
@@ -274,7 +274,7 @@
catch { case _: SecurityException => false }
} match {
case Some(dir) =>
- val file = standard_path(Path.explode(dir) + Path.basic(name))
+ val file = standard_path(dir + Path.basic(name))
Standard_System.process_output(execute(true, (List(file) ++ args): _*))
case None => ("Unknown Isabelle tool: " + name, 2)
}
@@ -334,8 +334,8 @@
/* components */
- def components(): List[String] =
- getenv_strict("ISABELLE_COMPONENTS").split(":").toList
+ def components(): List[Path] =
+ Path.split(getenv_strict("ISABELLE_COMPONENTS"))
/* find logics */
@@ -344,8 +344,8 @@
{
val ml_ident = getenv_strict("ML_IDENTIFIER")
val logics = new mutable.ListBuffer[String]
- for (dir <- getenv_strict("ISABELLE_PATH").split(":")) {
- val files = platform_file(Path.explode(dir) + Path.explode(ml_ident)).listFiles()
+ for (dir <- Path.split(getenv_strict("ISABELLE_PATH"))) {
+ val files = platform_file(dir + Path.explode(ml_ident)).listFiles()
if (files != null) {
for (file <- files if file.isFile) logics += file.getName
}
@@ -362,7 +362,7 @@
def install_fonts()
{
val ge = GraphicsEnvironment.getLocalGraphicsEnvironment()
- for (font <- getenv_strict("ISABELLE_FONTS").split(":"))
- ge.registerFont(Font.createFont(Font.TRUETYPE_FONT, platform_file(Path.explode(font))))
+ for (font <- Path.split(getenv_strict("ISABELLE_FONTS")))
+ ge.registerFont(Font.createFont(Font.TRUETYPE_FONT, platform_file(font)))
}
}
--- a/src/Pure/System/session.scala Tue Jul 05 19:11:29 2011 +0200
+++ b/src/Pure/System/session.scala Wed Jul 06 09:54:40 2011 +0200
@@ -115,6 +115,8 @@
/* global state */
+ @volatile var loaded_theories: Set[String] = Set()
+
@volatile private var syntax = new Outer_Syntax(Isabelle_System.symbols)
def current_syntax(): Outer_Syntax = syntax
@@ -138,6 +140,9 @@
val thy_load = new Thy_Load
{
+ override def is_loaded(name: String): Boolean =
+ loaded_theories.contains(name)
+
override def check_thy(dir: Path, name: String): (String, Thy_Header.Header) =
{
val file = Isabelle_System.platform_file(dir + Thy_Header.thy_path(name))
@@ -255,6 +260,7 @@
catch { case _: Document.State.Fail => bad_result(result) }
case List(Keyword.Command_Decl(name, kind)) => syntax += (name, kind)
case List(Keyword.Keyword_Decl(name)) => syntax += name
+ case List(Thy_Info.Loaded_Theory(name)) => loaded_theories += name
case _ => bad_result(result)
}
}
--- a/src/Pure/System/session_manager.scala Tue Jul 05 19:11:29 2011 +0200
+++ b/src/Pure/System/session_manager.scala Wed Jul 06 09:54:40 2011 +0200
@@ -42,8 +42,7 @@
def component_sessions(): List[List[String]] =
{
val toplevel_sessions =
- Isabelle_System.components().map(s =>
- Isabelle_System.platform_file(Path.explode(s))).filter(is_session_dir)
+ Isabelle_System.components().map(Isabelle_System.platform_file).filter(is_session_dir)
((Nil: List[List[String]]) /: toplevel_sessions)(find_sessions(Nil, _, _)).reverse
}
}
--- a/src/Pure/System/standard_system.scala Tue Jul 05 19:11:29 2011 +0200
+++ b/src/Pure/System/standard_system.scala Wed Jul 06 09:54:40 2011 +0200
@@ -264,8 +264,9 @@
class Standard_System
{
+ /* platform_root */
+
val platform_root = if (Platform.is_windows) Cygwin.check_root() else "/"
- override def toString = platform_root
/* jvm_path */
@@ -291,7 +292,7 @@
path
case path => path
}
- for (p <- rest.split("/") if p != "") {
+ for (p <- space_explode('/', rest) if p != "") {
val len = result_path.length
if (len > 0 && result_path(len - 1) != File.separatorChar)
result_path += File.separatorChar
--- a/src/Pure/Thy/html.scala Tue Jul 05 19:11:29 2011 +0200
+++ b/src/Pure/Thy/html.scala Wed Jul 06 09:54:40 2011 +0200
@@ -80,7 +80,7 @@
flush()
ts += elem
}
- val syms = Symbol.iterator_string(txt)
+ val syms = Symbol.iterator(txt)
while (syms.hasNext) {
val s1 = syms.next
def s2() = if (syms.hasNext) syms.next else ""
--- a/src/Pure/Thy/thy_header.scala Tue Jul 05 19:11:29 2011 +0200
+++ b/src/Pure/Thy/thy_header.scala Wed Jul 06 09:54:40 2011 +0200
@@ -112,7 +112,8 @@
{
val header = read(source)
val name1 = header.name
- if (name == name1) header
- else error("Bad file name " + thy_path(name) + " for theory " + quote(name1))
+ if (name != name1) error("Bad file name " + thy_path(name) + " for theory " + quote(name1))
+ Path.explode(name)
+ header
}
}
--- a/src/Pure/Thy/thy_info.ML Tue Jul 05 19:11:29 2011 +0200
+++ b/src/Pure/Thy/thy_info.ML Wed Jul 06 09:54:40 2011 +0200
@@ -10,6 +10,7 @@
datatype action = Update | Remove
val add_hook: (action -> string -> unit) -> unit
val get_names: unit -> string list
+ val status: unit -> unit
val lookup_theory: string -> theory option
val get_theory: string -> theory
val is_finished: string -> bool
@@ -88,6 +89,9 @@
fun get_names () = Graph.topological_order (get_thys ());
+fun status () =
+ List.app (Output.status o Markup.markup_only o Markup.loaded_theory) (get_names ());
+
(* access thy *)
--- a/src/Pure/Thy/thy_info.scala Tue Jul 05 19:11:29 2011 +0200
+++ b/src/Pure/Thy/thy_info.scala Wed Jul 06 09:54:40 2011 +0200
@@ -7,6 +7,20 @@
package isabelle
+object Thy_Info
+{
+ /* protocol messages */
+
+ object Loaded_Theory {
+ def unapply(msg: XML.Tree): Option[String] =
+ msg match {
+ case XML.Elem(Markup(Markup.LOADED_THEORY, List((Markup.NAME, name))), _) => Some(name)
+ case _ => None
+ }
+ }
+}
+
+
class Thy_Info(thy_load: Thy_Load)
{
/* messages */
@@ -26,16 +40,17 @@
type Deps = Map[String, Exn.Result[(String, Thy_Header.Header)]] // name -> (text, header)
- private def require_thys(
+ private def require_thys(ignored: String => Boolean,
initiators: List[String], dir: Path, deps: Deps, strs: List[String]): Deps =
- (deps /: strs)(require_thy(initiators, dir, _, _))
+ (deps /: strs)(require_thy(ignored, initiators, dir, _, _))
- private def require_thy(initiators: List[String], dir: Path, deps: Deps, str: String): Deps =
+ private def require_thy(ignored: String => Boolean,
+ initiators: List[String], dir: Path, deps: Deps, str: String): Deps =
{
val path = Path.explode(str)
val name = path.base.implode
- if (deps.isDefinedAt(name)) deps
+ if (deps.isDefinedAt(name) || ignored(name)) deps
else {
val dir1 = dir + path.dir
try {
@@ -47,7 +62,7 @@
cat_error(msg, "The error(s) above occurred while examining theory " +
quote(name) + required_by("\n", initiators))
}
- require_thys(name :: initiators, dir1,
+ require_thys(ignored, name :: initiators, dir1,
deps + (name -> Exn.Res(text, header)), header.imports)
}
catch { case e: Throwable => deps + (name -> Exn.Exn(e)) }
@@ -55,5 +70,5 @@
}
def dependencies(dir: Path, str: String): Deps =
- require_thy(Nil, dir, Map.empty, str) // FIXME capture errors in str (!??)
+ require_thy(thy_load.is_loaded, Nil, dir, Map.empty, str)
}
--- a/src/Pure/Thy/thy_load.scala Tue Jul 05 19:11:29 2011 +0200
+++ b/src/Pure/Thy/thy_load.scala Wed Jul 06 09:54:40 2011 +0200
@@ -8,6 +8,8 @@
abstract class Thy_Load
{
+ def is_loaded(name: String): Boolean
+
def check_thy(dir: Path, name: String): (String, Thy_Header.Header)
}
--- a/src/Pure/library.scala Tue Jul 05 19:11:29 2011 +0200
+++ b/src/Pure/library.scala Wed Jul 06 09:54:40 2011 +0200
@@ -61,6 +61,8 @@
result.toList
}
+ def split_lines(str: String): List[String] = space_explode('\n', str)
+
/* iterate over chunks (cf. space_explode) */
@@ -185,13 +187,14 @@
class Basic_Library
{
+ val ERROR = Library.ERROR
+ val error = Library.error _
+ val cat_error = Library.cat_error _
+
val space_explode = Library.space_explode _
+ val split_lines = Library.split_lines _
val quote = Library.quote _
val commas = Library.commas _
val commas_quote = Library.commas_quote _
-
- val ERROR = Library.ERROR
- val error = Library.error _
- val cat_error = Library.cat_error _
}
--- a/src/Tools/jEdit/etc/settings Tue Jul 05 19:11:29 2011 +0200
+++ b/src/Tools/jEdit/etc/settings Wed Jul 06 09:54:40 2011 +0200
@@ -10,7 +10,7 @@
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"
-ISABELLE_JEDIT_OPTIONS="-m xsymbols -m no_brackets -m no_type_brackets"
+ISABELLE_JEDIT_OPTIONS="-m no_brackets -m no_type_brackets"
ISABELLE_TOOLS="$ISABELLE_TOOLS:$JEDIT_HOME/lib/Tools"
--- a/src/Tools/jEdit/src/html_panel.scala Tue Jul 05 19:11:29 2011 +0200
+++ b/src/Tools/jEdit/src/html_panel.scala Wed Jul 06 09:54:40 2011 +0200
@@ -92,8 +92,7 @@
<head>
<style media="all" type="text/css">
""" +
- Isabelle_System.try_read(
- Isabelle_System.getenv_strict("JEDIT_STYLE_SHEETS").split(":").map(Path.explode))
+ Isabelle_System.try_read(Path.split(Isabelle_System.getenv_strict("JEDIT_STYLE_SHEETS")))
private val template_tail =
"""
--- a/src/Tools/jEdit/src/plugin.scala Tue Jul 05 19:11:29 2011 +0200
+++ b/src/Tools/jEdit/src/plugin.scala Wed Jul 06 09:54:40 2011 +0200
@@ -300,7 +300,7 @@
def start_session()
{
val timeout = Time_Property("startup-timeout", Time.seconds(10)) max Time.seconds(5)
- val modes = Isabelle_System.getenv("JEDIT_PRINT_MODE").split(",").toList.map("-m" + _)
+ val modes = space_explode(',', Isabelle_System.getenv("JEDIT_PRINT_MODE")).map("-m" + _)
val logic = {
val logic = Property("logic")
if (logic != null && logic != "") logic
--- a/src/Tools/jEdit/src/token_markup.scala Tue Jul 05 19:11:29 2011 +0200
+++ b/src/Tools/jEdit/src/token_markup.scala Wed Jul 06 09:54:40 2011 +0200
@@ -124,7 +124,7 @@
}
var offset = 0
var ctrl = ""
- for (sym <- Symbol.iterator_string(text)) {
+ for (sym <- Symbol.iterator(text)) {
if (ctrl_style(sym).isDefined) ctrl = sym
else if (ctrl != "") {
if (symbols.is_controllable(sym) && sym != "\"" && !symbols.fonts.isDefinedAt(sym)) {