# HG changeset patch # User wenzelm # Date 1309938880 -7200 # Node ID ff935aea9557aa9f83b87d8242017b6ff20caea9 # Parent 052eaf7509cf2b5a9dc65eedfa143d889e0f7534# Parent 8252d51d70e2a1c99e93cb9910abfd81d14575ed merged diff -r 052eaf7509cf -r ff935aea9557 src/Pure/Concurrent/future.ML --- 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; diff -r 052eaf7509cf -r ff935aea9557 src/Pure/General/markup.ML --- 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; diff -r 052eaf7509cf -r ff935aea9557 src/Pure/General/markup.scala --- 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" diff -r 052eaf7509cf -r ff935aea9557 src/Pure/General/path.scala --- 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) } diff -r 052eaf7509cf -r ff935aea9557 src/Pure/General/symbol.scala --- 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 */ diff -r 052eaf7509cf -r ff935aea9557 src/Pure/Isar/toplevel.ML --- 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) (); diff -r 052eaf7509cf -r ff935aea9557 src/Pure/PIDE/document.ML --- 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); diff -r 052eaf7509cf -r ff935aea9557 src/Pure/PIDE/isar_document.ML --- 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)); diff -r 052eaf7509cf -r ff935aea9557 src/Pure/System/isabelle_process.ML --- 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)); diff -r 052eaf7509cf -r ff935aea9557 src/Pure/System/isabelle_system.scala --- 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))) } } diff -r 052eaf7509cf -r ff935aea9557 src/Pure/System/session.scala --- 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) } } diff -r 052eaf7509cf -r ff935aea9557 src/Pure/System/session_manager.scala --- 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 } } diff -r 052eaf7509cf -r ff935aea9557 src/Pure/System/standard_system.scala --- 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 diff -r 052eaf7509cf -r ff935aea9557 src/Pure/Thy/html.scala --- 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 "" diff -r 052eaf7509cf -r ff935aea9557 src/Pure/Thy/thy_header.scala --- 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 } } diff -r 052eaf7509cf -r ff935aea9557 src/Pure/Thy/thy_info.ML --- 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 *) diff -r 052eaf7509cf -r ff935aea9557 src/Pure/Thy/thy_info.scala --- 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) } diff -r 052eaf7509cf -r ff935aea9557 src/Pure/Thy/thy_load.scala --- 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) } diff -r 052eaf7509cf -r ff935aea9557 src/Pure/library.scala --- 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 _ } diff -r 052eaf7509cf -r ff935aea9557 src/Tools/jEdit/etc/settings --- 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" diff -r 052eaf7509cf -r ff935aea9557 src/Tools/jEdit/src/html_panel.scala --- 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 @@