# HG changeset patch # User wenzelm # Date 1492082667 -7200 # Node ID 7ca8810b1d48943d865e32f27ebf79993da179a8 # Parent b0f89998c2a135d1d1af669d1e1917e26a6766fe# Parent 7c40477e0a879dd46355c1dbb4f828793ce19c44 merged diff -r b0f89998c2a1 -r 7ca8810b1d48 src/Pure/ML/ml_console.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/ML/ml_console.scala Thu Apr 13 13:24:27 2017 +0200 @@ -0,0 +1,135 @@ +/* Title: Pure/ML/ml_console.scala + Author: Makarius + +The raw ML process in interactive mode. +*/ + +package isabelle + + +import java.io.{IOException, BufferedReader, InputStreamReader} + + +object ML_Console +{ + /* command line entry point */ + + def main(args: Array[String]) + { + Command_Line.tool { + var dirs: List[Path] = Nil + var logic = Isabelle_System.getenv("ISABELLE_LOGIC") + var modes: List[String] = Nil + var no_build = false + var options = Options.init() + var raw_ml_system = false + var system_mode = false + + val getopts = Getopts(""" +Usage: isabelle console [OPTIONS] + + Options are: + -d DIR include session directory + -l NAME logic session name (default ISABELLE_LOGIC=""" + quote(logic) + """) + -m MODE add print mode for output + -n no build of session image on startup + -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) + -r bootstrap from raw Poly/ML + -s system build mode for session image + + Build a logic session image and run the raw Isabelle ML process + in interactive mode, with line editor ISABELLE_LINE_EDITOR=""" + + quote(Isabelle_System.getenv("ISABELLE_LINE_EDITOR")) + """. +""", + "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))), + "l:" -> (arg => logic = arg), + "m:" -> (arg => modes = arg :: modes), + "n" -> (arg => no_build = true), + "o:" -> (arg => options = options + arg), + "r" -> (_ => raw_ml_system = true), + "s" -> (_ => system_mode = true)) + + val more_args = getopts(args) + if (!more_args.isEmpty) getopts.usage() + + + // build + if (!no_build && !raw_ml_system && + !Build.build(options = options, build_heap = true, no_build = true, + dirs = dirs, system_mode = system_mode, sessions = List(logic)).ok) + { + val progress = new Console_Progress() + progress.echo("Build started for Isabelle/" + logic + " ...") + progress.interrupt_handler { + val res = + Build.build(options = options, progress = progress, build_heap = true, + dirs = dirs, system_mode = system_mode, sessions = List(logic)) + if (!res.ok) sys.exit(res.rc) + } + } + + // process loop + val process = + ML_Process(options, logic = logic, args = List("-i"), dirs = dirs, redirect = true, + modes = if (raw_ml_system) Nil else modes ::: List("ASCII"), + raw_ml_system = raw_ml_system, store = Sessions.store(system_mode), + session_base = + if (raw_ml_system) None + else Some(Sessions.session_base(options, logic, dirs))) + val process_output = Future.thread[Unit]("process_output") { + try { + var result = new StringBuilder(100) + var finished = false + while (!finished) { + var c = -1 + var done = false + while (!done && (result.length == 0 || process.stdout.ready)) { + c = process.stdout.read + if (c >= 0) result.append(c.asInstanceOf[Char]) + else done = true + } + if (result.length > 0) { + System.out.print(result.toString) + System.out.flush() + result.length = 0 + } + else { + process.stdout.close() + finished = true + } + } + } + catch { case e: IOException => case Exn.Interrupt() => } + } + val process_input = Future.thread[Unit]("process_input") { + val reader = new BufferedReader(new InputStreamReader(System.in)) + POSIX_Interrupt.handler { process.interrupt } { + try { + var finished = false + while (!finished) { + reader.readLine() match { + case null => + process.stdin.close() + finished = true + case line => + process.stdin.write(line) + process.stdin.write("\n") + process.stdin.flush() + } + } + } + catch { case e: IOException => case Exn.Interrupt() => } + } + } + val process_result = Future.thread[Int]("process_result") { + val rc = process.join + process_input.cancel + rc + } + + process_output.join + process_input.join + process_result.join + } + } +} diff -r b0f89998c2a1 -r 7ca8810b1d48 src/Pure/ML/ml_process.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/ML/ml_process.scala Thu Apr 13 13:24:27 2017 +0200 @@ -0,0 +1,194 @@ +/* Title: Pure/ML/ml_process.scala + Author: Makarius + +The raw ML process. +*/ + +package isabelle + + +import java.io.{File => JFile} + + +object ML_Process +{ + def apply(options: Options, + logic: String = "", + args: List[String] = Nil, + dirs: List[Path] = Nil, + modes: List[String] = Nil, + raw_ml_system: Boolean = false, + cwd: JFile = null, + env: Map[String, String] = Isabelle_System.settings(), + redirect: Boolean = false, + cleanup: () => Unit = () => (), + channel: Option[System_Channel] = None, + sessions: Option[Sessions.T] = None, + session_base: Option[Sessions.Base] = None, + store: Sessions.Store = Sessions.store()): Bash.Process = + { + val logic_name = Isabelle_System.default_logic(logic) + val heaps: List[String] = + if (raw_ml_system) Nil + else { + val selection = Sessions.Selection(sessions = List(logic_name)) + val (_, selected_sessions) = + sessions.getOrElse(Sessions.load(options, dirs)).selection(selection) + (selected_sessions.build_ancestors(logic_name) ::: List(logic_name)). + map(a => File.platform_path(store.heap(a))) + } + + val eval_init = + if (heaps.isEmpty) { + List( + """ + fun chapter (_: string) = (); + fun section (_: string) = (); + fun subsection (_: string) = (); + fun subsubsection (_: string) = (); + fun paragraph (_: string) = (); + fun subparagraph (_: string) = (); + val ML_file = PolyML.use; + """, + if (Isabelle_System.getenv("ML_SYSTEM") == "polyml-5.6") + """ + structure FixedInt = IntInf; + structure RunCall = + struct + open RunCall + val loadWord: word * word -> word = + run_call2 RuntimeCalls.POLY_SYS_load_word; + val storeWord: word * word * word -> unit = + run_call3 RuntimeCalls.POLY_SYS_assign_word; + end; + """ + else "", + if (Platform.is_windows) + "fun exit 0 = OS.Process.exit OS.Process.success" + + " | exit 1 = OS.Process.exit OS.Process.failure" + + " | exit rc = OS.Process.exit (RunCall.unsafeCast (Word8.fromInt rc))" + else + "fun exit rc = Posix.Process.exit (Word8.fromInt rc)", + "PolyML.Compiler.prompt1 := \"Poly/ML> \"", + "PolyML.Compiler.prompt2 := \"Poly/ML# \"") + } + else + List( + "(PolyML.SaveState.loadHierarchy " + + ML_Syntax.print_list(ML_Syntax.print_string0)(heaps) + + "; PolyML.print_depth 0) handle exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ " + + ML_Syntax.print_string0(": " + logic_name + "\n") + + "); OS.Process.exit OS.Process.failure)") + + val eval_modes = + if (modes.isEmpty) Nil + else List("Print_Mode.add_modes " + ML_Syntax.print_list(ML_Syntax.print_string0)(modes)) + + // options + val isabelle_process_options = Isabelle_System.tmp_file("options") + File.write(isabelle_process_options, YXML.string_of_body(options.encode)) + val env_options = Map("ISABELLE_PROCESS_OPTIONS" -> File.standard_path(isabelle_process_options)) + val eval_options = if (heaps.isEmpty) Nil else List("Options.load_default ()") + + // session base + val eval_session_base = + session_base match { + case None => Nil + case Some(base) => + def print_table(table: List[(String, String)]): String = + ML_Syntax.print_list( + ML_Syntax.print_pair( + ML_Syntax.print_string, ML_Syntax.print_string))(table) + List("Resources.init_session_base {default_qualifier = \"\"" + + ", global_theories = " + print_table(base.global_theories.toList) + + ", loaded_theories = " + print_table(base.loaded_theories.toList) + + ", known_theories = " + print_table(base.dest_known_theories) + "}") + } + + // process + val eval_process = + if (heaps.isEmpty) + List("PolyML.print_depth " + ML_Syntax.print_int(options.int("ML_print_depth"))) + else + channel match { + case None => + List("Isabelle_Process.init_options ()") + case Some(ch) => + List("Isabelle_Process.init_protocol " + ML_Syntax.print_string0(ch.server_name)) + } + + // ISABELLE_TMP + val isabelle_tmp = Isabelle_System.tmp_dir("process") + val env_tmp = Map("ISABELLE_TMP" -> File.standard_path(isabelle_tmp)) + + val ml_runtime_options = + { + val ml_options = Word.explode(Isabelle_System.getenv("ML_OPTIONS")) + if (ml_options.exists(_.containsSlice("gcthreads"))) ml_options + else ml_options ::: List("--gcthreads", options.int("threads").toString) + } + + // bash + val bash_args = + ml_runtime_options ::: + (eval_init ::: eval_modes ::: eval_options ::: eval_session_base ::: eval_process). + map(eval => List("--eval", eval)).flatten ::: args + + Bash.process( + "exec " + options.string("ML_process_policy") + """ "$ML_HOME/poly" -q """ + + Bash.strings(bash_args), + cwd = cwd, + env = + Isabelle_System.library_path(env ++ env_options ++ env_tmp, + Isabelle_System.getenv_strict("ML_HOME")), + redirect = redirect, + cleanup = () => + { + isabelle_process_options.delete + Isabelle_System.rm_tree(isabelle_tmp) + cleanup() + }) + } + + + /* Isabelle tool wrapper */ + + val isabelle_tool = Isabelle_Tool("process", "raw ML process (batch mode)", args => + { + var dirs: List[Path] = Nil + var eval_args: List[String] = Nil + var logic = Isabelle_System.getenv("ISABELLE_LOGIC") + var modes: List[String] = Nil + var options = Options.init() + + val getopts = Getopts(""" +Usage: isabelle process [OPTIONS] + + Options are: + -T THEORY load theory + -d DIR include session directory + -e ML_EXPR evaluate ML expression on startup + -f ML_FILE evaluate ML file on startup + -l NAME logic session name (default ISABELLE_LOGIC=""" + quote(logic) + """) + -m MODE add print mode for output + -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) + + Run the raw Isabelle ML process in batch mode. +""", + "T:" -> (arg => + eval_args = eval_args ::: List("--eval", "use_thy " + ML_Syntax.print_string0(arg))), + "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))), + "e:" -> (arg => eval_args = eval_args ::: List("--eval", arg)), + "f:" -> (arg => eval_args = eval_args ::: List("--use", arg)), + "l:" -> (arg => logic = arg), + "m:" -> (arg => modes = arg :: modes), + "o:" -> (arg => options = options + arg)) + + val more_args = getopts(args) + if (args.isEmpty || !more_args.isEmpty) getopts.usage() + + val rc = ML_Process(options, logic = logic, args = eval_args, dirs = dirs, modes = modes). + result().print_stdout.rc + sys.exit(rc) + }) +} diff -r b0f89998c2a1 -r 7ca8810b1d48 src/Pure/ML/ml_statistics.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/ML/ml_statistics.scala Thu Apr 13 13:24:27 2017 +0200 @@ -0,0 +1,151 @@ +/* Title: Pure/ML/ml_statistics.scala + Author: Makarius + +ML runtime statistics. +*/ + +package isabelle + + +import scala.collection.mutable +import scala.collection.immutable.{SortedSet, SortedMap} +import scala.swing.{Frame, Component} + +import org.jfree.data.xy.{XYSeries, XYSeriesCollection} +import org.jfree.chart.{JFreeChart, ChartPanel, ChartFactory} +import org.jfree.chart.plot.PlotOrientation + + +object ML_Statistics +{ + /* content interpretation */ + + final case class Entry(time: Double, data: Map[String, Double]) + + def apply(session_name: String, ml_statistics: List[Properties.T]): ML_Statistics = + new ML_Statistics(session_name, ml_statistics) + + val empty = apply("", Nil) + + + /* standard fields */ + + type Fields = (String, Iterable[String]) + + val tasks_fields: Fields = + ("Future tasks", + List("tasks_ready", "tasks_pending", "tasks_running", "tasks_passive", "tasks_urgent")) + + val workers_fields: Fields = + ("Worker threads", List("workers_total", "workers_active", "workers_waiting")) + + val GC_fields: Fields = + ("GCs", List("partial_GCs", "full_GCs")) + + val heap_fields: Fields = + ("Heap", List("size_heap", "size_allocation", "size_allocation_free", + "size_heap_free_last_full_GC", "size_heap_free_last_GC")) + + val threads_fields: Fields = + ("Threads", List("threads_total", "threads_in_ML", "threads_wait_condvar", + "threads_wait_IO", "threads_wait_mutex", "threads_wait_signal")) + + val time_fields: Fields = + ("Time", List("time_CPU", "time_GC")) + + val speed_fields: Fields = + ("Speed", List("speed_CPU", "speed_GC")) + + + val all_fields: List[Fields] = + List(tasks_fields, workers_fields, GC_fields, heap_fields, threads_fields, + time_fields, speed_fields) + + val main_fields: List[Fields] = + List(tasks_fields, workers_fields, heap_fields) +} + +final class ML_Statistics private(val session_name: String, val ml_statistics: List[Properties.T]) +{ + val Now = new Properties.Double("now") + def now(props: Properties.T): Double = Now.unapply(props).get + + require(ml_statistics.forall(props => Now.unapply(props).isDefined)) + + val time_start = if (ml_statistics.isEmpty) 0.0 else now(ml_statistics.head) + val duration = if (ml_statistics.isEmpty) 0.0 else now(ml_statistics.last) - time_start + + val fields: Set[String] = + SortedSet.empty[String] ++ + (for (props <- ml_statistics.iterator; (x, _) <- props.iterator if x != Now.name) + yield x) + + val content: List[ML_Statistics.Entry] = + { + var last_edge = Map.empty[String, (Double, Double, Double)] + val result = new mutable.ListBuffer[ML_Statistics.Entry] + for (props <- ml_statistics) { + val time = now(props) - time_start + require(time >= 0.0) + + // rising edges -- relative speed + val speeds = + for ((key, value) <- props; a <- Library.try_unprefix("time", key)) yield { + val (x0, y0, s0) = last_edge.getOrElse(a, (0.0, 0.0, 0.0)) + + val x1 = time + val y1 = java.lang.Double.parseDouble(value) + val s1 = if (x1 == x0) 0.0 else (y1 - y0) / (x1 - x0) + + val b = ("speed" + a).intern + if (y1 > y0) { last_edge += (a -> (x1, y1, s1)); (b, s1) } else (b, s0) + } + + val data = + SortedMap.empty[String, Double] ++ speeds ++ + (for ((x, y) <- props.iterator if x != Now.name) + yield (x, java.lang.Double.parseDouble(y))) + result += ML_Statistics.Entry(time, data) + } + result.toList + } + + + /* charts */ + + def update_data(data: XYSeriesCollection, selected_fields: Iterable[String]) + { + data.removeAllSeries + for { + field <- selected_fields.iterator + series = new XYSeries(field) + } { + content.foreach(entry => series.add(entry.time, entry.data(field))) + data.addSeries(series) + } + } + + def chart(title: String, selected_fields: Iterable[String]): JFreeChart = + { + val data = new XYSeriesCollection + update_data(data, selected_fields) + + ChartFactory.createXYLineChart(title, "time", "value", data, + PlotOrientation.VERTICAL, true, true, true) + } + + def chart(fields: ML_Statistics.Fields): JFreeChart = + chart(fields._1, fields._2) + + def show_frames(fields: List[ML_Statistics.Fields] = ML_Statistics.main_fields): Unit = + fields.map(chart(_)).foreach(c => + GUI_Thread.later { + new Frame { + iconImage = GUI.isabelle_image() + title = session_name + contents = Component.wrap(new ChartPanel(c)) + visible = true + } + }) +} + diff -r b0f89998c2a1 -r 7ca8810b1d48 src/Pure/PIDE/document.scala --- a/src/Pure/PIDE/document.scala Wed Apr 12 09:27:47 2017 +0200 +++ b/src/Pure/PIDE/document.scala Thu Apr 13 13:24:27 2017 +0200 @@ -99,6 +99,8 @@ { val empty = Name("") + def loaded_theory(theory: String): Name = Name(theory, "", theory) + object Ordering extends scala.math.Ordering[Name] { def compare(name1: Name, name2: Name): Int = name1.node compare name2.node @@ -114,7 +116,6 @@ case _ => false } - def loaded_theory: Name = Name(theory, "", theory) def is_theory: Boolean = theory.nonEmpty def theory_base_name: String = Long_Name.base_name(theory) diff -r b0f89998c2a1 -r 7ca8810b1d48 src/Pure/PIDE/protocol.ML --- a/src/Pure/PIDE/protocol.ML Wed Apr 12 09:27:47 2017 +0200 +++ b/src/Pure/PIDE/protocol.ML Thu Apr 13 13:24:27 2017 +0200 @@ -18,6 +18,19 @@ Isabelle_Process.init_options_interactive ())); val _ = + Isabelle_Process.protocol_command "Prover.session_base" + (fn [default_qualifier, global_theories_yxml, loaded_theories_yxml, known_theories_yxml] => + let + val decode_table = YXML.parse_body #> let open XML.Decode in list (pair string string) end; + in + Resources.init_session_base + {default_qualifier = default_qualifier, + global_theories = decode_table global_theories_yxml, + loaded_theories = decode_table loaded_theories_yxml, + known_theories = decode_table known_theories_yxml} + end); + +val _ = Isabelle_Process.protocol_command "Document.define_blob" (fn [digest, content] => Document.change_state (Document.define_blob digest content)); diff -r b0f89998c2a1 -r 7ca8810b1d48 src/Pure/PIDE/protocol.scala --- a/src/Pure/PIDE/protocol.scala Wed Apr 12 09:27:47 2017 +0200 +++ b/src/Pure/PIDE/protocol.scala Thu Apr 13 13:24:27 2017 +0200 @@ -302,6 +302,22 @@ protocol_command("Prover.options", Symbol.encode_yxml(opts.encode)) + /* session base */ + + private def encode_table(table: List[(String, String)]): String = + { + import XML.Encode._ + Symbol.encode_yxml(list(pair(string, string))(table)) + } + + def session_base(resources: Resources): Unit = + protocol_command("Prover.session_base", + Symbol.encode(resources.default_qualifier), + encode_table(resources.session_base.global_theories.toList), + encode_table(resources.session_base.loaded_theories.toList), + encode_table(resources.session_base.dest_known_theories)) + + /* interned items */ def define_blob(digest: SHA1.Digest, bytes: Bytes): Unit = diff -r b0f89998c2a1 -r 7ca8810b1d48 src/Pure/PIDE/resources.ML --- a/src/Pure/PIDE/resources.ML Wed Apr 12 09:27:47 2017 +0200 +++ b/src/Pure/PIDE/resources.ML Thu Apr 13 13:24:27 2017 +0200 @@ -6,15 +6,15 @@ signature RESOURCES = sig - val set_session_base: + val init_session_base: {default_qualifier: string, global_theories: (string * string) list, loaded_theories: (string * string) list, known_theories: (string * string) list} -> unit - val reset_session_base: unit -> unit + val finish_session_base: unit -> unit val default_qualifier: unit -> string val global_theory: string -> string option - val loaded_theory: string -> Path.T option + val loaded_theory: string -> string option val known_theory: string -> Path.T option val master_directory: theory -> Path.T val imports_of: theory -> (string * Position.T) list @@ -40,27 +40,32 @@ (* session base *) -val init_session_base = +val empty_session_base = {default_qualifier = "Draft", global_theories = Symtab.empty: string Symtab.table, - loaded_theories = Symtab.empty: Path.T Symtab.table, + loaded_theories = Symtab.empty: string Symtab.table, known_theories = Symtab.empty: Path.T Symtab.table}; val global_session_base = - Synchronized.var "Sessions.base" init_session_base; + Synchronized.var "Sessions.base" empty_session_base; -fun set_session_base {default_qualifier, global_theories, loaded_theories, known_theories} = +fun init_session_base {default_qualifier, global_theories, loaded_theories, known_theories} = Synchronized.change global_session_base (fn _ => {default_qualifier = if default_qualifier <> "" then default_qualifier - else #default_qualifier init_session_base, + else #default_qualifier empty_session_base, global_theories = Symtab.make global_theories, - loaded_theories = Symtab.make (map (apsnd Path.explode) loaded_theories), + loaded_theories = Symtab.make loaded_theories, known_theories = Symtab.make (map (apsnd Path.explode) known_theories)}); -fun reset_session_base () = - Synchronized.change global_session_base (K init_session_base); +fun finish_session_base () = + Synchronized.change global_session_base + (fn {global_theories, loaded_theories, ...} => + {default_qualifier = #default_qualifier empty_session_base, + global_theories = global_theories, + loaded_theories = loaded_theories, + known_theories = #known_theories empty_session_base}); fun get_session_base f = f (Synchronized.value global_session_base); @@ -108,21 +113,26 @@ SOME qualifier => qualifier | NONE => Long_Name.qualifier theory); +fun theory_name qualifier theory0 = + (case loaded_theory theory0 of + SOME theory => (true, theory) + | NONE => + let val theory = + if Long_Name.is_qualified theory0 orelse is_some (global_theory theory0) + orelse true (* FIXME *) then theory0 + else Long_Name.qualify qualifier theory0 + in (false, theory) end); + fun import_name qualifier dir s = - let - val theory0 = Thy_Header.import_name s; - val theory = - if Long_Name.is_qualified theory0 orelse is_some (global_theory theory0) - orelse true (* FIXME *) then theory0 - else Long_Name.qualify qualifier theory0; - val node_name = - the (get_first (fn e => e ()) - [fn () => loaded_theory theory, - fn () => loaded_theory theory0, - fn () => known_theory theory, - fn () => known_theory theory0, - fn () => SOME (File.full_path dir (thy_path (Path.expand (Path.explode s))))]) - in {node_name = node_name, master_dir = Path.dir node_name, theory_name = theory} end; + (case theory_name qualifier (Thy_Header.import_name s) of + (true, theory) => + {node_name = Path.basic theory, master_dir = Path.current, theory_name = theory} + | (false, theory) => + let val node_name = + (case known_theory theory of + SOME node_name => node_name + | NONE => File.full_path dir (thy_path (Path.expand (Path.explode s)))) + in {node_name = node_name, master_dir = Path.dir node_name, theory_name = theory} end); fun check_file dir file = File.check_file (File.full_path dir file); diff -r b0f89998c2a1 -r 7ca8810b1d48 src/Pure/PIDE/resources.scala --- a/src/Pure/PIDE/resources.scala Wed Apr 12 09:27:47 2017 +0200 +++ b/src/Pure/PIDE/resources.scala Thu Apr 13 13:24:27 2017 +0200 @@ -70,24 +70,30 @@ def theory_qualifier(name: Document.Node.Name): String = session_base.global_theories.getOrElse(name.theory, Long_Name.qualifier(name.theory)) - def import_name(qualifier: String, dir: String, s: String): Document.Node.Name = - { - val theory0 = Thy_Header.import_name(s) - val theory = - if (Long_Name.is_qualified(theory0) || session_base.global_theories.isDefinedAt(theory0) - || true /* FIXME */) theory0 - else theory0 // FIXME Long_Name.qualify(qualifier, theory0) + def theory_name(qualifier: String, theory0: String): (Boolean, String) = + session_base.loaded_theories.get(theory0) match { + case Some(theory) => (true, theory) + case None => + val theory = + if (Long_Name.is_qualified(theory0) || session_base.global_theories.isDefinedAt(theory0) + || true /* FIXME */) theory0 + else Long_Name.qualify(qualifier, theory0) + (false, theory) + } - session_base.loaded_theories.get(theory) orElse - session_base.loaded_theories.get(theory0) orElse - session_base.known_theories.get(theory) orElse - session_base.known_theories.get(theory0) getOrElse { - val path = Path.explode(s) - val node = append(dir, thy_path(path)) - val master_dir = append(dir, path.dir) - Document.Node.Name(node, master_dir, theory) + def import_name(qualifier: String, dir: String, s: String): Document.Node.Name = + theory_name(qualifier, Thy_Header.import_name(s)) match { + case (true, theory) => Document.Node.Name.loaded_theory(theory) + case (false, theory) => + session_base.known_theories.get(theory) match { + case Some(node_name) => node_name + case None => + val path = Path.explode(s) + val node = append(dir, thy_path(path)) + val master_dir = append(dir, path.dir) + Document.Node.Name(node, master_dir, theory) + } } - } def with_thy_reader[A](name: Document.Node.Name, f: Reader[Char] => A): A = { diff -r b0f89998c2a1 -r 7ca8810b1d48 src/Pure/PIDE/session.scala --- a/src/Pure/PIDE/session.scala Wed Apr 12 09:27:47 2017 +0200 +++ b/src/Pure/PIDE/session.scala Thu Apr 13 13:24:27 2017 +0200 @@ -443,6 +443,7 @@ case _ if output.is_init => prover.get.options(session_options) + prover.get.session_base(resources) phase = Session.Ready debugger.ready() diff -r b0f89998c2a1 -r 7ca8810b1d48 src/Pure/ROOT --- a/src/Pure/ROOT Wed Apr 12 09:27:47 2017 +0200 +++ b/src/Pure/ROOT Thu Apr 13 13:24:27 2017 +0200 @@ -7,4 +7,4 @@ options [threads = 1] theories Pure (global) - ML_Bootstrap + ML_Bootstrap (global) diff -r b0f89998c2a1 -r 7ca8810b1d48 src/Pure/Thy/sessions.scala --- a/src/Pure/Thy/sessions.scala Wed Apr 12 09:27:47 2017 +0200 +++ b/src/Pure/Thy/sessions.scala Thu Apr 13 13:24:27 2017 +0200 @@ -33,8 +33,11 @@ { def pure(options: Options): Base = session_base(options, Thy_Header.PURE) - lazy val bootstrap: Base = - Base(keywords = Thy_Header.bootstrap_header, syntax = Thy_Header.bootstrap_syntax) + def bootstrap(global_theories: Map[String, String]): Base = + Base( + global_theories = global_theories, + keywords = Thy_Header.bootstrap_header, + syntax = Thy_Header.bootstrap_syntax) private[Sessions] def known_theories( local_dir: Path, @@ -85,7 +88,7 @@ sealed case class Base( global_theories: Map[String, String] = Map.empty, - loaded_theories: Map[String, Document.Node.Name] = Map.empty, + loaded_theories: Map[String, String] = Map.empty, known_theories: Map[String, Document.Node.Name] = Map.empty, known_theories_local: Map[String, Document.Node.Name] = Map.empty, known_files: Map[JFile, List[Document.Node.Name]] = Map.empty, @@ -96,8 +99,6 @@ { def platform_path: Base = copy( - loaded_theories = - for ((a, b) <- loaded_theories) yield (a, b.map(File.platform_path(_))), known_theories = for ((a, b) <- known_theories) yield (a, b.map(File.platform_path(_))), known_theories_local = @@ -108,10 +109,6 @@ def loaded_theory(name: Document.Node.Name): Boolean = loaded_theories.isDefinedAt(name.theory) - def dest_loaded_theories: List[(String, String)] = - for ((theory, node_name) <- loaded_theories.toList) - yield (theory, node_name.node) - def dest_known_theories: List[(String, String)] = for ((theory, node_name) <- known_theories.toList) yield (theory, node_name.node) @@ -143,7 +140,7 @@ try { val parent_base = info.parent match { - case None => Base.bootstrap + case None => Base.bootstrap(global_theories) case Some(parent) => session_bases(parent) } val resources = new Resources(parent_base, @@ -595,7 +592,7 @@ (dir + ROOT).is_file || (dir + ROOTS).is_file private def check_session_dir(dir: Path): Path = - if (is_session_dir(dir)) dir + if (is_session_dir(dir)) File.pwd() + dir.expand else error("Bad session root directory: " + dir.toString) def load(options: Options, dirs: List[Path] = Nil, select_dirs: List[Path] = Nil): T = @@ -626,13 +623,11 @@ } val default_dirs = Isabelle_System.components().filter(is_session_dir(_)) - dirs.foreach(check_session_dir(_)) - select_dirs.foreach(check_session_dir(_)) make( for { (select, dir) <- (default_dirs ::: dirs).map((false, _)) ::: select_dirs.map((true, _)) - info <- load_dir(select, dir) + info <- load_dir(select, check_session_dir(dir)) } yield info) } diff -r b0f89998c2a1 -r 7ca8810b1d48 src/Pure/Thy/thy_info.scala --- a/src/Pure/Thy/thy_info.scala Wed Apr 12 09:27:47 2017 +0200 +++ b/src/Pure/Thy/thy_info.scala Thu Apr 13 13:24:27 2017 +0200 @@ -80,12 +80,12 @@ lazy val syntax: Outer_Syntax = resources.session_base.syntax.add_keywords(keywords).add_abbrevs(abbrevs) - def loaded_theories: Map[String, Document.Node.Name] = + def loaded_theories: Map[String, String] = (resources.session_base.loaded_theories /: rev_deps) { case (loaded, dep) => - val name = dep.name.loaded_theory - loaded + (name.theory -> name) + - (name.theory_base_name -> name) // legacy + val name = dep.name + loaded + (name.theory -> name.theory) + + (name.theory_base_name -> name.theory) // legacy } def loaded_files: List[Path] = diff -r b0f89998c2a1 -r 7ca8810b1d48 src/Pure/Tools/build.ML --- a/src/Pure/Tools/build.ML Wed Apr 12 09:27:47 2017 +0200 +++ b/src/Pure/Tools/build.ML Thu Apr 13 13:24:27 2017 +0200 @@ -180,7 +180,7 @@ val symbols = HTML.make_symbols symbol_codes; val _ = - Resources.set_session_base + Resources.init_session_base {default_qualifier = name, global_theories = global_theories, loaded_theories = loaded_theories, @@ -210,7 +210,7 @@ |> Exn.capture); val res2 = Exn.capture Session.finish (); - val _ = Resources.reset_session_base (); + val _ = Resources.finish_session_base (); val _ = Par_Exn.release_all [res1, res2]; in () end; diff -r b0f89998c2a1 -r 7ca8810b1d48 src/Pure/Tools/build.scala --- a/src/Pure/Tools/build.scala Wed Apr 12 09:27:47 2017 +0200 +++ b/src/Pure/Tools/build.scala Thu Apr 13 13:24:27 2017 +0200 @@ -205,14 +205,14 @@ pair(Path.encode, pair(list(pair(Path.encode, Path.encode)), pair(string, pair(string, pair(string, pair(string, pair(Path.encode, pair(list(pair(Options.encode, list(string))), - pair(list(pair(string, string)), - pair(list(pair(string, string)), list(pair(string, string))))))))))))))))( + pair(list(pair(string, string)), pair(list(pair(string, string)), + list(pair(string, string))))))))))))))))( (Symbol.codes, (command_timings, (do_output, (verbose, (store.browser_info, (info.document_files, (File.standard_path(graph_file), (parent, (info.chapter, (name, (Path.current, (info.theories, - (base.global_theories.toList, - (base.dest_loaded_theories, base.dest_known_theories))))))))))))))) + (base.global_theories.toList, (base.loaded_theories.toList, + base.dest_known_theories))))))))))))))) }) val env = diff -r b0f89998c2a1 -r 7ca8810b1d48 src/Pure/Tools/ml_console.scala --- a/src/Pure/Tools/ml_console.scala Wed Apr 12 09:27:47 2017 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,135 +0,0 @@ -/* Title: Pure/Tools/ml_console.scala - Author: Makarius - -The raw ML process in interactive mode. -*/ - -package isabelle - - -import java.io.{IOException, BufferedReader, InputStreamReader} - - -object ML_Console -{ - /* command line entry point */ - - def main(args: Array[String]) - { - Command_Line.tool { - var dirs: List[Path] = Nil - var logic = Isabelle_System.getenv("ISABELLE_LOGIC") - var modes: List[String] = Nil - var no_build = false - var options = Options.init() - var raw_ml_system = false - var system_mode = false - - val getopts = Getopts(""" -Usage: isabelle console [OPTIONS] - - Options are: - -d DIR include session directory - -l NAME logic session name (default ISABELLE_LOGIC=""" + quote(logic) + """) - -m MODE add print mode for output - -n no build of session image on startup - -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) - -r bootstrap from raw Poly/ML - -s system build mode for session image - - Build a logic session image and run the raw Isabelle ML process - in interactive mode, with line editor ISABELLE_LINE_EDITOR=""" + - quote(Isabelle_System.getenv("ISABELLE_LINE_EDITOR")) + """. -""", - "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))), - "l:" -> (arg => logic = arg), - "m:" -> (arg => modes = arg :: modes), - "n" -> (arg => no_build = true), - "o:" -> (arg => options = options + arg), - "r" -> (_ => raw_ml_system = true), - "s" -> (_ => system_mode = true)) - - val more_args = getopts(args) - if (!more_args.isEmpty) getopts.usage() - - - // build - if (!no_build && !raw_ml_system && - !Build.build(options = options, build_heap = true, no_build = true, - dirs = dirs, system_mode = system_mode, sessions = List(logic)).ok) - { - val progress = new Console_Progress() - progress.echo("Build started for Isabelle/" + logic + " ...") - progress.interrupt_handler { - val res = - Build.build(options = options, progress = progress, build_heap = true, - dirs = dirs, system_mode = system_mode, sessions = List(logic)) - if (!res.ok) sys.exit(res.rc) - } - } - - // process loop - val process = - ML_Process(options, logic = logic, args = List("-i"), dirs = dirs, redirect = true, - modes = if (raw_ml_system) Nil else modes ::: List("ASCII"), - raw_ml_system = raw_ml_system, store = Sessions.store(system_mode), - session_base = - if (raw_ml_system) None - else Some(Sessions.session_base(options, logic, dirs))) - val process_output = Future.thread[Unit]("process_output") { - try { - var result = new StringBuilder(100) - var finished = false - while (!finished) { - var c = -1 - var done = false - while (!done && (result.length == 0 || process.stdout.ready)) { - c = process.stdout.read - if (c >= 0) result.append(c.asInstanceOf[Char]) - else done = true - } - if (result.length > 0) { - System.out.print(result.toString) - System.out.flush() - result.length = 0 - } - else { - process.stdout.close() - finished = true - } - } - } - catch { case e: IOException => case Exn.Interrupt() => } - } - val process_input = Future.thread[Unit]("process_input") { - val reader = new BufferedReader(new InputStreamReader(System.in)) - POSIX_Interrupt.handler { process.interrupt } { - try { - var finished = false - while (!finished) { - reader.readLine() match { - case null => - process.stdin.close() - finished = true - case line => - process.stdin.write(line) - process.stdin.write("\n") - process.stdin.flush() - } - } - } - catch { case e: IOException => case Exn.Interrupt() => } - } - } - val process_result = Future.thread[Int]("process_result") { - val rc = process.join - process_input.cancel - rc - } - - process_output.join - process_input.join - process_result.join - } - } -} diff -r b0f89998c2a1 -r 7ca8810b1d48 src/Pure/Tools/ml_process.scala --- a/src/Pure/Tools/ml_process.scala Wed Apr 12 09:27:47 2017 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,194 +0,0 @@ -/* Title: Pure/Tools/ml_process.scala - Author: Makarius - -The raw ML process. -*/ - -package isabelle - - -import java.io.{File => JFile} - - -object ML_Process -{ - def apply(options: Options, - logic: String = "", - args: List[String] = Nil, - dirs: List[Path] = Nil, - modes: List[String] = Nil, - raw_ml_system: Boolean = false, - cwd: JFile = null, - env: Map[String, String] = Isabelle_System.settings(), - redirect: Boolean = false, - cleanup: () => Unit = () => (), - channel: Option[System_Channel] = None, - sessions: Option[Sessions.T] = None, - session_base: Option[Sessions.Base] = None, - store: Sessions.Store = Sessions.store()): Bash.Process = - { - val logic_name = Isabelle_System.default_logic(logic) - val heaps: List[String] = - if (raw_ml_system) Nil - else { - val selection = Sessions.Selection(sessions = List(logic_name)) - val (_, selected_sessions) = - sessions.getOrElse(Sessions.load(options, dirs)).selection(selection) - (selected_sessions.build_ancestors(logic_name) ::: List(logic_name)). - map(a => File.platform_path(store.heap(a))) - } - - val eval_init = - if (heaps.isEmpty) { - List( - """ - fun chapter (_: string) = (); - fun section (_: string) = (); - fun subsection (_: string) = (); - fun subsubsection (_: string) = (); - fun paragraph (_: string) = (); - fun subparagraph (_: string) = (); - val ML_file = PolyML.use; - """, - if (Isabelle_System.getenv("ML_SYSTEM") == "polyml-5.6") - """ - structure FixedInt = IntInf; - structure RunCall = - struct - open RunCall - val loadWord: word * word -> word = - run_call2 RuntimeCalls.POLY_SYS_load_word; - val storeWord: word * word * word -> unit = - run_call3 RuntimeCalls.POLY_SYS_assign_word; - end; - """ - else "", - if (Platform.is_windows) - "fun exit 0 = OS.Process.exit OS.Process.success" + - " | exit 1 = OS.Process.exit OS.Process.failure" + - " | exit rc = OS.Process.exit (RunCall.unsafeCast (Word8.fromInt rc))" - else - "fun exit rc = Posix.Process.exit (Word8.fromInt rc)", - "PolyML.Compiler.prompt1 := \"Poly/ML> \"", - "PolyML.Compiler.prompt2 := \"Poly/ML# \"") - } - else - List( - "(PolyML.SaveState.loadHierarchy " + - ML_Syntax.print_list(ML_Syntax.print_string0)(heaps) + - "; PolyML.print_depth 0) handle exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ " + - ML_Syntax.print_string0(": " + logic_name + "\n") + - "); OS.Process.exit OS.Process.failure)") - - val eval_modes = - if (modes.isEmpty) Nil - else List("Print_Mode.add_modes " + ML_Syntax.print_list(ML_Syntax.print_string0)(modes)) - - // options - val isabelle_process_options = Isabelle_System.tmp_file("options") - File.write(isabelle_process_options, YXML.string_of_body(options.encode)) - val env_options = Map("ISABELLE_PROCESS_OPTIONS" -> File.standard_path(isabelle_process_options)) - val eval_options = if (heaps.isEmpty) Nil else List("Options.load_default ()") - - // session base - val eval_session_base = - session_base match { - case None => Nil - case Some(base) => - def print_table(table: List[(String, String)]): String = - ML_Syntax.print_list( - ML_Syntax.print_pair( - ML_Syntax.print_string, ML_Syntax.print_string))(table) - List("Resources.set_session_base {default_qualifier = \"\"" + - ", global_theories = " + print_table(base.global_theories.toList) + - ", loaded_theories = " + print_table(base.dest_loaded_theories) + - ", known_theories = " + print_table(base.dest_known_theories) + "}") - } - - // process - val eval_process = - if (heaps.isEmpty) - List("PolyML.print_depth " + ML_Syntax.print_int(options.int("ML_print_depth"))) - else - channel match { - case None => - List("Isabelle_Process.init_options ()") - case Some(ch) => - List("Isabelle_Process.init_protocol " + ML_Syntax.print_string0(ch.server_name)) - } - - // ISABELLE_TMP - val isabelle_tmp = Isabelle_System.tmp_dir("process") - val env_tmp = Map("ISABELLE_TMP" -> File.standard_path(isabelle_tmp)) - - val ml_runtime_options = - { - val ml_options = Word.explode(Isabelle_System.getenv("ML_OPTIONS")) - if (ml_options.exists(_.containsSlice("gcthreads"))) ml_options - else ml_options ::: List("--gcthreads", options.int("threads").toString) - } - - // bash - val bash_args = - ml_runtime_options ::: - (eval_init ::: eval_modes ::: eval_options ::: eval_session_base ::: eval_process). - map(eval => List("--eval", eval)).flatten ::: args - - Bash.process( - "exec " + options.string("ML_process_policy") + """ "$ML_HOME/poly" -q """ + - Bash.strings(bash_args), - cwd = cwd, - env = - Isabelle_System.library_path(env ++ env_options ++ env_tmp, - Isabelle_System.getenv_strict("ML_HOME")), - redirect = redirect, - cleanup = () => - { - isabelle_process_options.delete - Isabelle_System.rm_tree(isabelle_tmp) - cleanup() - }) - } - - - /* Isabelle tool wrapper */ - - val isabelle_tool = Isabelle_Tool("process", "raw ML process (batch mode)", args => - { - var dirs: List[Path] = Nil - var eval_args: List[String] = Nil - var logic = Isabelle_System.getenv("ISABELLE_LOGIC") - var modes: List[String] = Nil - var options = Options.init() - - val getopts = Getopts(""" -Usage: isabelle process [OPTIONS] - - Options are: - -T THEORY load theory - -d DIR include session directory - -e ML_EXPR evaluate ML expression on startup - -f ML_FILE evaluate ML file on startup - -l NAME logic session name (default ISABELLE_LOGIC=""" + quote(logic) + """) - -m MODE add print mode for output - -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) - - Run the raw Isabelle ML process in batch mode. -""", - "T:" -> (arg => - eval_args = eval_args ::: List("--eval", "use_thy " + ML_Syntax.print_string0(arg))), - "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))), - "e:" -> (arg => eval_args = eval_args ::: List("--eval", arg)), - "f:" -> (arg => eval_args = eval_args ::: List("--use", arg)), - "l:" -> (arg => logic = arg), - "m:" -> (arg => modes = arg :: modes), - "o:" -> (arg => options = options + arg)) - - val more_args = getopts(args) - if (args.isEmpty || !more_args.isEmpty) getopts.usage() - - val rc = ML_Process(options, logic = logic, args = eval_args, dirs = dirs, modes = modes). - result().print_stdout.rc - sys.exit(rc) - }) -} diff -r b0f89998c2a1 -r 7ca8810b1d48 src/Pure/Tools/ml_statistics.scala --- a/src/Pure/Tools/ml_statistics.scala Wed Apr 12 09:27:47 2017 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,151 +0,0 @@ -/* Title: Pure/Tools/ml_statistics.scala - Author: Makarius - -ML runtime statistics. -*/ - -package isabelle - - -import scala.collection.mutable -import scala.collection.immutable.{SortedSet, SortedMap} -import scala.swing.{Frame, Component} - -import org.jfree.data.xy.{XYSeries, XYSeriesCollection} -import org.jfree.chart.{JFreeChart, ChartPanel, ChartFactory} -import org.jfree.chart.plot.PlotOrientation - - -object ML_Statistics -{ - /* content interpretation */ - - final case class Entry(time: Double, data: Map[String, Double]) - - def apply(session_name: String, ml_statistics: List[Properties.T]): ML_Statistics = - new ML_Statistics(session_name, ml_statistics) - - val empty = apply("", Nil) - - - /* standard fields */ - - type Fields = (String, Iterable[String]) - - val tasks_fields: Fields = - ("Future tasks", - List("tasks_ready", "tasks_pending", "tasks_running", "tasks_passive", "tasks_urgent")) - - val workers_fields: Fields = - ("Worker threads", List("workers_total", "workers_active", "workers_waiting")) - - val GC_fields: Fields = - ("GCs", List("partial_GCs", "full_GCs")) - - val heap_fields: Fields = - ("Heap", List("size_heap", "size_allocation", "size_allocation_free", - "size_heap_free_last_full_GC", "size_heap_free_last_GC")) - - val threads_fields: Fields = - ("Threads", List("threads_total", "threads_in_ML", "threads_wait_condvar", - "threads_wait_IO", "threads_wait_mutex", "threads_wait_signal")) - - val time_fields: Fields = - ("Time", List("time_CPU", "time_GC")) - - val speed_fields: Fields = - ("Speed", List("speed_CPU", "speed_GC")) - - - val all_fields: List[Fields] = - List(tasks_fields, workers_fields, GC_fields, heap_fields, threads_fields, - time_fields, speed_fields) - - val main_fields: List[Fields] = - List(tasks_fields, workers_fields, heap_fields) -} - -final class ML_Statistics private(val session_name: String, val ml_statistics: List[Properties.T]) -{ - val Now = new Properties.Double("now") - def now(props: Properties.T): Double = Now.unapply(props).get - - require(ml_statistics.forall(props => Now.unapply(props).isDefined)) - - val time_start = if (ml_statistics.isEmpty) 0.0 else now(ml_statistics.head) - val duration = if (ml_statistics.isEmpty) 0.0 else now(ml_statistics.last) - time_start - - val fields: Set[String] = - SortedSet.empty[String] ++ - (for (props <- ml_statistics.iterator; (x, _) <- props.iterator if x != Now.name) - yield x) - - val content: List[ML_Statistics.Entry] = - { - var last_edge = Map.empty[String, (Double, Double, Double)] - val result = new mutable.ListBuffer[ML_Statistics.Entry] - for (props <- ml_statistics) { - val time = now(props) - time_start - require(time >= 0.0) - - // rising edges -- relative speed - val speeds = - for ((key, value) <- props; a <- Library.try_unprefix("time", key)) yield { - val (x0, y0, s0) = last_edge.getOrElse(a, (0.0, 0.0, 0.0)) - - val x1 = time - val y1 = java.lang.Double.parseDouble(value) - val s1 = if (x1 == x0) 0.0 else (y1 - y0) / (x1 - x0) - - val b = ("speed" + a).intern - if (y1 > y0) { last_edge += (a -> (x1, y1, s1)); (b, s1) } else (b, s0) - } - - val data = - SortedMap.empty[String, Double] ++ speeds ++ - (for ((x, y) <- props.iterator if x != Now.name) - yield (x, java.lang.Double.parseDouble(y))) - result += ML_Statistics.Entry(time, data) - } - result.toList - } - - - /* charts */ - - def update_data(data: XYSeriesCollection, selected_fields: Iterable[String]) - { - data.removeAllSeries - for { - field <- selected_fields.iterator - series = new XYSeries(field) - } { - content.foreach(entry => series.add(entry.time, entry.data(field))) - data.addSeries(series) - } - } - - def chart(title: String, selected_fields: Iterable[String]): JFreeChart = - { - val data = new XYSeriesCollection - update_data(data, selected_fields) - - ChartFactory.createXYLineChart(title, "time", "value", data, - PlotOrientation.VERTICAL, true, true, true) - } - - def chart(fields: ML_Statistics.Fields): JFreeChart = - chart(fields._1, fields._2) - - def show_frames(fields: List[ML_Statistics.Fields] = ML_Statistics.main_fields): Unit = - fields.map(chart(_)).foreach(c => - GUI_Thread.later { - new Frame { - iconImage = GUI.isabelle_image() - title = session_name - contents = Component.wrap(new ChartPanel(c)) - visible = true - } - }) -} - diff -r b0f89998c2a1 -r 7ca8810b1d48 src/Pure/build-jars --- a/src/Pure/build-jars Wed Apr 12 09:27:47 2017 +0200 +++ b/src/Pure/build-jars Thu Apr 13 13:24:27 2017 +0200 @@ -82,7 +82,10 @@ Isar/outer_syntax.scala Isar/parse.scala Isar/token.scala + ML/ml_console.scala ML/ml_lex.scala + ML/ml_process.scala + ML/ml_statistics.scala ML/ml_syntax.scala PIDE/command.scala PIDE/command_span.scala @@ -133,9 +136,6 @@ Tools/debugger.scala Tools/doc.scala Tools/main.scala - Tools/ml_console.scala - Tools/ml_process.scala - Tools/ml_statistics.scala Tools/print_operation.scala Tools/profiling_report.scala Tools/simplifier_trace.scala diff -r b0f89998c2a1 -r 7ca8810b1d48 src/Tools/VSCode/src/vscode_resources.scala --- a/src/Tools/VSCode/src/vscode_resources.scala Wed Apr 12 09:27:47 2017 +0200 +++ b/src/Tools/VSCode/src/vscode_resources.scala Thu Apr 13 13:24:27 2017 +0200 @@ -63,9 +63,12 @@ def node_name(file: JFile): Document.Node.Name = { val node = file.getPath - val theory = Thy_Header.theory_name(node) - val master_dir = if (theory == "") "" else file.getParent - Document.Node.Name(node, master_dir, theory) + theory_name(default_qualifier, Thy_Header.theory_name(node)) match { + case (true, theory) => Document.Node.Name.loaded_theory(theory) + case (false, theory) => + val master_dir = if (theory == "") "" else file.getParent + Document.Node.Name(node, master_dir, theory) + } } override def append(dir: String, source_path: Path): String = diff -r b0f89998c2a1 -r 7ca8810b1d48 src/Tools/jEdit/src/document_model.scala --- a/src/Tools/jEdit/src/document_model.scala Wed Apr 12 09:27:47 2017 +0200 +++ b/src/Tools/jEdit/src/document_model.scala Thu Apr 13 13:24:27 2017 +0200 @@ -310,7 +310,7 @@ last_perspective: Document.Node.Perspective_Text = Document.Node.no_perspective_text, pending_edits: List[Text.Edit] = Nil): File_Model = { - val file = PIDE.resources.node_name_file(node_name) + val file = JEdit_Lib.check_file(node_name.node) file.foreach(PIDE.plugin.file_watcher.register_parent(_)) val content = Document_Model.File_Content(text) diff -r b0f89998c2a1 -r 7ca8810b1d48 src/Tools/jEdit/src/jedit_lib.scala --- a/src/Tools/jEdit/src/jedit_lib.scala Wed Apr 12 09:27:47 2017 +0200 +++ b/src/Tools/jEdit/src/jedit_lib.scala Thu Apr 13 13:24:27 2017 +0200 @@ -9,6 +9,7 @@ import isabelle._ +import java.io.{File => JFile} import java.awt.{Component, Container, GraphicsEnvironment, Point, Rectangle, Dimension} import java.awt.event.{InputEvent, KeyEvent, KeyListener} import javax.swing.{Icon, ImageIcon, JWindow, SwingUtilities} @@ -16,6 +17,7 @@ import scala.util.parsing.input.CharSequenceReader import org.gjt.sp.jedit.{jEdit, Buffer, View, GUIUtilities, Debug, EditPane} +import org.gjt.sp.jedit.io.{VFS, FileVFS, VFSManager} import org.gjt.sp.jedit.gui.KeyEventWorkaround import org.gjt.sp.jedit.buffer.{JEditBuffer, LineManager} import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea, TextAreaPainter} @@ -93,6 +95,15 @@ } + /* files */ + + def is_file(name: String): Boolean = + VFSManager.getVFSForPath(name).isInstanceOf[FileVFS] + + def check_file(name: String): Option[JFile] = + if (is_file(name)) Some(new JFile(name)) else None + + /* buffers */ def buffer_text(buffer: JEditBuffer): String = @@ -111,10 +122,12 @@ } } + def buffer_line_manager(buffer: JEditBuffer): LineManager = + Untyped.get[LineManager](buffer, "lineMgr") + def buffer_name(buffer: Buffer): String = buffer.getSymlinkPath - def buffer_line_manager(buffer: JEditBuffer): LineManager = - Untyped.get[LineManager](buffer, "lineMgr") + def buffer_file(buffer: Buffer): Option[JFile] = check_file(buffer_name(buffer)) /* main jEdit components */ diff -r b0f89998c2a1 -r 7ca8810b1d48 src/Tools/jEdit/src/jedit_resources.scala --- a/src/Tools/jEdit/src/jedit_resources.scala Wed Apr 12 09:27:47 2017 +0200 +++ b/src/Tools/jEdit/src/jedit_resources.scala Thu Apr 13 13:24:27 2017 +0200 @@ -25,28 +25,20 @@ { /* document node name */ - def node_name(buffer: Buffer): Document.Node.Name = - { - val node = JEdit_Lib.buffer_name(buffer) - val theory = Thy_Header.theory_name(node) - val master_dir = if (theory == "") "" else buffer.getDirectory - Document.Node.Name(node, master_dir, theory) - } - def node_name(path: String): Document.Node.Name = { val vfs = VFSManager.getVFSForPath(path) val node = if (vfs.isInstanceOf[FileVFS]) MiscUtilities.resolveSymlinks(path) else path - val theory = Thy_Header.theory_name(node) - val master_dir = if (theory == "") "" else vfs.getParentOfPath(path) - Document.Node.Name(node, master_dir, theory) + theory_name(default_qualifier, Thy_Header.theory_name(node)) match { + case (true, theory) => Document.Node.Name.loaded_theory(theory) + case (false, theory) => + val master_dir = if (theory == "") "" else vfs.getParentOfPath(path) + Document.Node.Name(node, master_dir, theory) + } } - def node_name_file(name: Document.Node.Name): Option[JFile] = - { - val vfs = VFSManager.getVFSForPath(name.node) - if (vfs.isInstanceOf[FileVFS]) Some(new JFile(name.node)) else None - } + def node_name(buffer: Buffer): Document.Node.Name = + node_name(JEdit_Lib.buffer_name(buffer)) def theory_node_name(buffer: Buffer): Option[Document.Node.Name] = {