--- /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
+ }
+ }
+}
--- /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)
+ })
+}
--- /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
+ }
+ })
+}
+
--- 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)
--- 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));
--- 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 =
--- 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);
--- 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 =
{
--- 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()
--- 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)
--- 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)
}
--- 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] =
--- 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;
--- 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 =
--- 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
- }
- }
-}
--- 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)
- })
-}
--- 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
- }
- })
-}
-
--- 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
--- 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 =
--- 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)
--- 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 */
--- 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] =
{