--- a/NEWS Wed Sep 11 20:48:10 2019 +0200
+++ b/NEWS Thu Sep 12 13:33:09 2019 +0200
@@ -46,6 +46,16 @@
instances during roundup.
+*** Isabelle/jEdit Prover IDE ***
+
+* Prover IDE startup is now much faster, because theory dependencies are
+no longer explored in advance. The overall session structure with its
+declarations of 'directories' is sufficient to locate theory files. Thus
+the "session focus" of option "isabelle jedit -S" has become obsolete
+(likewise for "isabelle vscode_server -S"). Existing option "-R" is both
+sufficient and more convenient to start editing a particular session.
+
+
*** HOL ***
* ASCII membership syntax concerning big operators for infimum and
--- a/src/Doc/JEdit/JEdit.thy Wed Sep 11 20:48:10 2019 +0200
+++ b/src/Doc/JEdit/JEdit.thy Thu Sep 12 13:33:09 2019 +0200
@@ -228,12 +228,11 @@
\<open>Usage: isabelle jedit [OPTIONS] [FILES ...]
Options are:
- -A NAME ancestor session for options -R and -S (default: parent)
+ -A NAME ancestor session for option -R (default: parent)
-D NAME=X set JVM system property
-J OPTION add JVM runtime option
(default $JEDIT_JAVA_SYSTEM_OPTIONS $JEDIT_JAVA_OPTIONS)
-R NAME build image with requirements from other sessions
- -S NAME like option -R, with focus on selected session
-b build only
-d DIR include session directory
-f fresh build
@@ -262,12 +261,9 @@
The \<^verbatim>\<open>-R\<close> option builds an auxiliary logic image with all theories from
other sessions that are not already present in its parent; it also opens the
session \<^verbatim>\<open>ROOT\<close> entry in the editor to facilitate editing of the main
- session. The \<^verbatim>\<open>-S\<close> option is like \<^verbatim>\<open>-R\<close>, with a focus on the selected
- session and its descendants: the namespace of accessible theories is
- restricted accordingly. This reduces startup time for big projects, notably
- the ``Archive of Formal Proofs''. The \<^verbatim>\<open>-A\<close> option specifies and alternative
- ancestor session for options \<^verbatim>\<open>-R\<close> and \<^verbatim>\<open>-S\<close>: this allows to restructure the
- hierarchy of session images on the spot.
+ session. The \<^verbatim>\<open>-A\<close> option specifies and alternative ancestor session for
+ option \<^verbatim>\<open>-R\<close>: this allows to restructure the hierarchy of session images on
+ the spot.
The \<^verbatim>\<open>-i\<close> option includes additional sessions into the name-space of
theories: multiple occurrences are possible.
--- a/src/Pure/ML/ml_process.scala Wed Sep 11 20:48:10 2019 +0200
+++ b/src/Pure/ML/ml_process.scala Thu Sep 12 13:33:09 2019 +0200
@@ -29,14 +29,15 @@
val logic_name = Isabelle_System.default_logic(logic)
val _store = store.getOrElse(Sessions.store(options))
+ val sessions_structure1 =
+ sessions_structure.getOrElse(Sessions.load_structure(options, dirs = dirs))
+
val heaps: List[String] =
if (raw_ml_system) Nil
else {
val selection = Sessions.Selection(sessions = List(logic_name))
- val selected_sessions =
- sessions_structure.getOrElse(Sessions.load_structure(options, dirs = dirs))
- .selection(selection)
- selected_sessions.build_requirements(List(logic_name)).
+ sessions_structure1.selection(selection).
+ build_requirements(List(logic_name)).
map(a => File.platform_path(_store.the_heap(a)))
}
@@ -96,7 +97,8 @@
ML_Syntax.print_pair(ML_Syntax.print_string_bytes, ML_Syntax.print_properties))(list)
List("Resources.init_session_base" +
- " {sessions = " + print_sessions(base.known.sessions.toList) +
+ " {session_positions = " + print_sessions(sessions_structure1.session_positions) +
+ ", session_directories = " + print_table(sessions_structure1.dest_session_directories) +
", docs = " + print_list(base.doc_names) +
", global_theories = " + print_table(base.global_theories.toList) +
", loaded_theories = " + print_list(base.loaded_theories.keys) +
--- a/src/Pure/PIDE/headless.scala Wed Sep 11 20:48:10 2019 +0200
+++ b/src/Pure/PIDE/headless.scala Thu Sep 12 13:33:09 2019 +0200
@@ -562,7 +562,8 @@
class Resources private[Headless](
val session_base_info: Sessions.Base_Info,
log: Logger = No_Logger)
- extends isabelle.Resources(session_base_info.check_base, log = log)
+ extends isabelle.Resources(
+ session_base_info.sessions_structure, session_base_info.check_base, log = log)
{
resources =>
--- a/src/Pure/PIDE/protocol.ML Wed Sep 11 20:48:10 2019 +0200
+++ b/src/Pure/PIDE/protocol.ML Thu Sep 12 13:33:09 2019 +0200
@@ -19,8 +19,8 @@
val _ =
Isabelle_Process.protocol_command "Prover.init_session_base"
- (fn [sessions_yxml, doc_names_yxml, global_theories_yxml, loaded_theories_yxml,
- known_theories_yxml] =>
+ (fn [session_positions_yxml, session_directories_yxml, doc_names_yxml, 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;
val decode_list = YXML.parse_body #> let open XML.Decode in list string end;
@@ -28,7 +28,8 @@
YXML.parse_body #> let open XML.Decode in list (pair string properties) end;
in
Resources.init_session_base
- {sessions = decode_sessions sessions_yxml,
+ {session_positions = decode_sessions session_positions_yxml,
+ session_directories = decode_table session_directories_yxml,
docs = decode_list doc_names_yxml,
global_theories = decode_table global_theories_yxml,
loaded_theories = decode_list loaded_theories_yxml,
--- a/src/Pure/PIDE/protocol.scala Wed Sep 11 20:48:10 2019 +0200
+++ b/src/Pure/PIDE/protocol.scala Thu Sep 12 13:33:09 2019 +0200
@@ -241,7 +241,8 @@
{
val base = resources.session_base.standard_path
protocol_command("Prover.init_session_base",
- encode_sessions(base.known.sessions.toList),
+ encode_sessions(resources.sessions_structure.session_positions),
+ encode_table(resources.sessions_structure.dest_session_directories),
encode_list(base.doc_names),
encode_table(base.global_theories.toList),
encode_list(base.loaded_theories.keys),
--- a/src/Pure/PIDE/resources.ML Wed Sep 11 20:48:10 2019 +0200
+++ b/src/Pure/PIDE/resources.ML Thu Sep 12 13:33:09 2019 +0200
@@ -8,7 +8,8 @@
sig
val default_qualifier: string
val init_session_base:
- {sessions: (string * Properties.T) list,
+ {session_positions: (string * Properties.T) list,
+ session_directories: (string * string) list,
docs: string list,
global_theories: (string * string) list,
loaded_theories: string list,
@@ -16,7 +17,6 @@
val finish_session_base: unit -> unit
val global_theory: string -> string option
val loaded_theory: string -> bool
- val known_theory: string -> Path.T option
val check_session: Proof.context -> string * Position.T -> string
val check_doc: Proof.context -> string * Position.T -> string
val master_directory: theory -> Path.T
@@ -24,6 +24,7 @@
val begin_theory: Path.T -> Thy_Header.header -> theory list -> theory
val thy_path: Path.T -> Path.T
val theory_qualifier: string -> string
+ val find_theory_file: string -> Path.T option
val import_name: string -> Path.T -> string ->
{node_name: Path.T, master_dir: Path.T, theory_name: string}
val check_thy: Path.T -> string ->
@@ -52,7 +53,8 @@
{pos = Position.of_properties props, serial = serial ()};
val empty_session_base =
- {sessions = []: (string * entry) list,
+ {session_positions = []: (string * entry) list,
+ session_directories = Symtab.empty: Path.T list Symtab.table,
docs = []: (string * entry) list,
global_theories = Symtab.empty: string Symtab.table,
loaded_theories = Symtab.empty: unit Symtab.table,
@@ -61,10 +63,14 @@
val global_session_base =
Synchronized.var "Sessions.base" empty_session_base;
-fun init_session_base {sessions, docs, global_theories, loaded_theories, known_theories} =
+fun init_session_base
+ {session_positions, session_directories, docs, global_theories, loaded_theories, known_theories} =
Synchronized.change global_session_base
(fn _ =>
- {sessions = sort_by #1 (map (apsnd make_entry) sessions),
+ {session_positions = sort_by #1 (map (apsnd make_entry) session_positions),
+ session_directories =
+ fold_rev (fn (dir, name) => Symtab.cons_list (name, Path.explode dir))
+ session_directories Symtab.empty,
docs = sort_by #1 (map (apsnd make_entry o rpair []) docs),
global_theories = Symtab.make global_theories,
loaded_theories = Symtab.make_set loaded_theories,
@@ -73,7 +79,8 @@
fun finish_session_base () =
Synchronized.change global_session_base
(fn {global_theories, loaded_theories, ...} =>
- {sessions = [],
+ {session_positions = [],
+ session_directories = Symtab.empty,
docs = [],
global_theories = global_theories,
loaded_theories = loaded_theories,
@@ -83,7 +90,6 @@
fun global_theory a = Symtab.lookup (get_session_base #global_theories) a;
fun loaded_theory a = Symtab.defined (get_session_base #loaded_theories) a;
-fun known_theory a = Symtab.lookup (get_session_base #known_theories) a;
fun check_name which kind markup ctxt (name, pos) =
let val entries = get_session_base which in
@@ -106,7 +112,7 @@
Markup.properties
(Position.entity_properties_of false serial pos) (Markup.entity Markup.sessionN name);
-val check_session = check_name #sessions "session" markup_session;
+val check_session = check_name #session_positions "session" markup_session;
val check_doc = check_name #docs "documentation" (fn name => fn _ => Markup.doc name);
@@ -157,6 +163,20 @@
then theory
else Long_Name.qualify qualifier theory;
+fun find_theory_file thy_name =
+ (case Symtab.lookup (get_session_base #known_theories) thy_name of
+ NONE =>
+ let
+ val thy_file = thy_path (Path.basic (Long_Name.base_name thy_name));
+ val session = theory_qualifier thy_name;
+ val dirs = Symtab.lookup_list (get_session_base #session_directories) session;
+ in
+ dirs |> get_first (fn dir =>
+ let val path = Path.append dir thy_file
+ in if File.is_file path then SOME path else NONE end)
+ end
+ | some => some);
+
fun import_name qualifier dir s =
let val theory = theory_name qualifier (Thy_Header.import_name s) in
if loaded_theory theory
@@ -164,7 +184,7 @@
else
let
val node_name =
- (case known_theory theory of
+ (case find_theory_file theory of
SOME node_name => node_name
| NONE =>
if Thy_Header.is_base_name s andalso Long_Name.is_qualified s
@@ -179,7 +199,7 @@
let
val thy_base_name = Long_Name.base_name thy_name;
val master_file =
- (case known_theory thy_name of
+ (case find_theory_file thy_name of
SOME known_path => check_file Path.current known_path
| NONE => check_file dir (thy_path (Path.basic thy_base_name)));
val text = File.read master_file;
--- a/src/Pure/PIDE/resources.scala Wed Sep 11 20:48:10 2019 +0200
+++ b/src/Pure/PIDE/resources.scala Thu Sep 12 13:33:09 2019 +0200
@@ -14,6 +14,7 @@
class Resources(
+ val sessions_structure: Sessions.Structure,
val session_base: Sessions.Base,
val log: Logger = No_Logger)
{
@@ -47,6 +48,13 @@
def append(node_name: Document.Node.Name, source_path: Path): String =
append(node_name.master_dir, source_path)
+ def make_theory_node(dir: String, file: Path, theory: String): Document.Node.Name =
+ {
+ val node = append(dir, file)
+ val master_dir = append(dir, file.dir)
+ Document.Node.Name(node, master_dir, theory)
+ }
+
/* source files of Isabelle/ML bootstrap */
@@ -109,22 +117,30 @@
theory
else Long_Name.qualify(qualifier, theory)
+ def find_theory_node(theory: String): Option[Document.Node.Name] =
+ session_base.known.theories.get(theory).map(_.name) orElse {
+ val thy_file = thy_path(Path.basic(Long_Name.base_name(theory)))
+ val session = session_base.theory_qualifier(theory)
+ val dirs =
+ sessions_structure.get(session) match {
+ case Some(info) => info.dirs
+ case None => Nil
+ }
+ dirs.collectFirst({
+ case dir if (dir + thy_file).is_file => make_theory_node("", dir + thy_file, theory) })
+ }
+
def import_name(qualifier: String, dir: String, s: String): Document.Node.Name =
{
val theory = theory_name(qualifier, Thy_Header.import_name(s))
if (session_base.loaded_theory(theory)) Document.Node.Name.loaded_theory(theory)
else {
- session_base.known_theory(theory) match {
+ find_theory_node(theory) match {
case Some(node_name) => node_name
case None =>
if (Thy_Header.is_base_name(s) && Long_Name.is_qualified(s))
Document.Node.Name.loaded_theory(theory)
- else {
- 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)
- }
+ else make_theory_node(dir, thy_path(Path.explode(s)), theory)
}
}
}
--- a/src/Pure/Thy/sessions.ML Wed Sep 11 20:48:10 2019 +0200
+++ b/src/Pure/Thy/sessions.ML Thu Sep 12 13:33:09 2019 +0200
@@ -86,7 +86,7 @@
val {node_name, theory_name, ...} =
Resources.import_name session session_dir s
handle ERROR msg => error (msg ^ Position.here pos);
- val theory_path = the_default node_name (Resources.known_theory theory_name);
+ val theory_path = the_default node_name (Resources.find_theory_file theory_name);
val _ = Resources.check_file ctxt (SOME Path.current) (Path.implode theory_path, pos);
in () end);
--- a/src/Pure/Thy/sessions.scala Wed Sep 11 20:48:10 2019 +0200
+++ b/src/Pure/Thy/sessions.scala Thu Sep 12 13:33:09 2019 +0200
@@ -41,7 +41,6 @@
val empty: Known = Known()
def make(local_dir: Path, bases: List[Base],
- sessions: List[(String, Position.T)] = Nil,
theories: List[Document.Node.Entry] = Nil,
loaded_files: List[(String, List[Path])] = Nil): Known =
{
@@ -58,9 +57,6 @@
entry.name.path.canonical_file.toPath.startsWith(local_path))
}
- val known_sessions =
- (sessions.toMap /: bases)({ case (known, base) => known ++ base.known.sessions })
-
val known_theories =
(Map.empty[String, Document.Node.Entry] /: (bases_iterator(false) ++ theories.iterator))({
case (known, entry) =>
@@ -92,7 +88,6 @@
(loaded_files.toMap /: bases.map(base => base.known.loaded_files))(_ ++ _)
Known(
- known_sessions,
known_theories,
known_theories_local,
known_files.iterator.map(p => (p._1, p._2.reverse)).toMap,
@@ -101,7 +96,6 @@
}
sealed case class Known(
- sessions: Map[String, Position.T] = Map.empty,
theories: Map[String, Document.Node.Entry] = Map.empty,
theories_local: Map[String, Document.Node.Entry] = Map.empty,
files: Map[JFile, List[Document.Node.Name]] = Map.empty,
@@ -180,9 +174,6 @@
def node_syntax(nodes: Document.Nodes, name: Document.Node.Name): Outer_Syntax =
nodes(name).syntax orElse loaded_theory_syntax(name) getOrElse overall_syntax
- def known_theory(name: String): Option[Document.Node.Name] =
- known.theories.get(name).map(_.name)
-
def dest_known_theories: List[(String, String)] =
for ((theory, entry) <- known.theories.toList)
yield (theory, entry.name.node)
@@ -304,7 +295,7 @@
parent_base.copy(known =
Known.make(info.dir, parent_base :: info.imports.map(session_bases(_))))
- val resources = new Resources(imports_base)
+ val resources = new Resources(sessions_structure, imports_base)
if (verbose || list_files) {
val groups =
@@ -371,7 +362,6 @@
val known =
Known.make(info.dir, List(imports_base),
- sessions = List(info.name -> info.pos),
theories = dependencies.entries,
loaded_files = loaded_files)
@@ -466,9 +456,7 @@
dirs: List[Path] = Nil,
include_sessions: List[String] = Nil,
session_ancestor: Option[String] = None,
- session_requirements: Boolean = false,
- session_focus: Boolean = false,
- all_known: Boolean = false): Base_Info =
+ session_requirements: Boolean = false): Base_Info =
{
val full_sessions = load_structure(options, dirs = dirs)
@@ -529,22 +517,11 @@
else load_structure(options, dirs = dirs, infos = infos1)
val selected_sessions1 =
- {
- val sel_sessions1 = session1 :: session :: include_sessions
- val select_sessions1 =
- if (session_focus) {
- full_sessions1.check_sessions(sel_sessions1)
- full_sessions1.imports_descendants(sel_sessions1)
- }
- else sel_sessions1
- full_sessions1.selection(Selection(sessions = select_sessions1))
- }
+ full_sessions1.selection(Selection(sessions = session1 :: session :: include_sessions))
- val sessions1 = if (all_known) full_sessions1 else selected_sessions1
- val deps1 = Sessions.deps(sessions1, progress = progress)
- val base1 = deps1(session1).copy(known = deps1.all_known)
+ val deps1 = Sessions.deps(selected_sessions1, progress = progress)
- Base_Info(options, dirs, session1, deps1.sessions_structure, deps1.errors, base1, infos1)
+ Base_Info(options, dirs, session1, full_sessions1, deps1.errors, deps1(session1), infos1)
}
@@ -701,6 +678,9 @@
val build_graph = add_edges(info_graph, "parent", _.parent)
val imports_graph = add_edges(build_graph, "imports", _.imports)
+ val session_positions: List[(String, Position.T)] =
+ (for ((name, (info, _)) <- info_graph.iterator) yield (name, info.pos)).toList
+
val session_directories: Map[JFile, String] =
(Map.empty[JFile, String] /:
(for {
@@ -735,10 +715,12 @@
}
})
- new Structure(session_directories, global_theories, build_graph, imports_graph)
+ new Structure(
+ session_positions, session_directories, global_theories, build_graph, imports_graph)
}
final class Structure private[Sessions](
+ val session_positions: List[(String, Position.T)],
val session_directories: Map[JFile, String],
val global_theories: Map[String, String],
val build_graph: Graph[String, Info],
@@ -746,6 +728,10 @@
{
sessions_structure =>
+ def dest_session_directories: List[(String, String)] =
+ for ((file, session) <- session_directories.toList)
+ yield (File.standard_path(file), session)
+
lazy val chapters: SortedMap[String, List[Info]] =
(SortedMap.empty[String, List[Info]] /: build_graph.iterator)(
{ case (chs, (_, (info, _))) =>
@@ -811,7 +797,8 @@
}
new Structure(
- session_directories, global_theories, restrict(build_graph), restrict(imports_graph))
+ session_positions, session_directories, global_theories,
+ restrict(build_graph), restrict(imports_graph))
}
def selection_deps(
--- a/src/Pure/Tools/build.ML Wed Sep 11 20:48:10 2019 +0200
+++ b/src/Pure/Tools/build.ML Thu Sep 12 13:33:09 2019 +0200
@@ -152,7 +152,8 @@
name: string,
master_dir: Path.T,
theories: (Options.T * (string * Position.T) list) list,
- sessions: (string * Properties.T) list,
+ session_positions: (string * Properties.T) list,
+ session_directories: (string * string) list,
doc_names: string list,
global_theories: (string * string) list,
loaded_theories: string list,
@@ -165,35 +166,39 @@
val position = Position.of_properties o properties;
val (symbol_codes, (command_timings, (do_output, (verbose, (browser_info,
(document_files, (graph_file, (parent_name, (chapter, (name, (master_dir,
- (theories, (sessions, (doc_names, (global_theories, (loaded_theories,
- (known_theories, bibtex_entries))))))))))))))))) =
+ (theories, (session_positions, (session_directories, (doc_names, (global_theories,
+ (loaded_theories, (known_theories, bibtex_entries)))))))))))))))))) =
pair (list (pair string int)) (pair (list properties) (pair bool (pair bool (pair string
(pair (list (pair string string)) (pair string (pair string (pair string (pair string
(pair string
(pair (((list (pair Options.decode (list (pair string position))))))
- (pair (list (pair string properties)) (pair (list string)
+ (pair (list (pair string properties))
(pair (list (pair string string)) (pair (list string)
- (pair (list (pair string string)) (list string)))))))))))))))))
+ (pair (list (pair string string)) (pair (list string)
+ (pair (list (pair string string)) (list string))))))))))))))))))
(YXML.parse_body yxml);
in
Args {symbol_codes = symbol_codes, command_timings = command_timings, do_output = do_output,
verbose = verbose, browser_info = Path.explode browser_info,
document_files = map (apply2 Path.explode) document_files,
graph_file = Path.explode graph_file, parent_name = parent_name, chapter = chapter,
- name = name, master_dir = Path.explode master_dir, theories = theories, sessions = sessions,
+ name = name, master_dir = Path.explode master_dir, theories = theories,
+ session_positions = session_positions, session_directories = session_directories,
doc_names = doc_names, global_theories = global_theories, loaded_theories = loaded_theories,
known_theories = known_theories, bibtex_entries = bibtex_entries}
end;
fun build_session (Args {symbol_codes, command_timings, do_output, verbose, browser_info,
- document_files, graph_file, parent_name, chapter, name, master_dir, theories, sessions,
- doc_names, global_theories, loaded_theories, known_theories, bibtex_entries}) =
+ document_files, graph_file, parent_name, chapter, name, master_dir, theories, session_positions,
+ session_directories, doc_names, global_theories, loaded_theories, known_theories,
+ bibtex_entries}) =
let
val symbols = HTML.make_symbols symbol_codes;
val _ =
Resources.init_session_base
- {sessions = sessions,
+ {session_positions = session_positions,
+ session_directories = session_directories,
docs = doc_names,
global_theories = global_theories,
loaded_theories = loaded_theories,
--- a/src/Pure/Tools/build.scala Wed Sep 11 20:48:10 2019 +0200
+++ b/src/Pure/Tools/build.scala Thu Sep 12 13:33:09 2019 +0200
@@ -197,6 +197,8 @@
{
val options = NUMA.policy_options(info.options, numa_node)
+ val sessions_structure = deps.sessions_structure
+
private val graph_file = Isabelle_System.tmp_file("session_graph", "pdf")
isabelle.graphview.Graph_File.write(options, graph_file, deps(name).session_graph_display)
@@ -216,15 +218,19 @@
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(pair(string, properties)))),
- pair(list(pair(string, properties)), pair(list(string),
+ pair(list(pair(string, properties)),
pair(list(pair(string, string)),
- pair(list(string), pair(list(pair(string, string)), list(string))))))))))))))))))(
+ pair(list(string), pair(list(pair(string, string)),
+ pair(list(string), pair(list(pair(string, string)), list(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.known.sessions.toList, (base.doc_names,
- (base.global_theories.toList, (base.loaded_theories.keys, (base.dest_known_theories,
- info.bibtex_entries.map(_.info)))))))))))))))))))
+ (info.theories,
+ (sessions_structure.session_positions,
+ (sessions_structure.dest_session_directories,
+ (base.doc_names, (base.global_theories.toList,
+ (base.loaded_theories.keys, (base.dest_known_theories,
+ info.bibtex_entries.map(_.info))))))))))))))))))))
})
val env =
@@ -238,7 +244,7 @@
ML_Syntax.print_string_bytes(File.platform_path(store.output_heap(name)))
if (pide && !Sessions.is_pure(name)) {
- val resources = new Resources(deps(parent))
+ val resources = new Resources(sessions_structure, deps(parent))
val session = new Session(options, resources)
val handler = new Handler(progress, session, name)
session.init_protocol_handler(handler)
@@ -246,7 +252,7 @@
val session_result = Future.promise[Process_Result]
Isabelle_Process.start(session, options, logic = parent, cwd = info.dir.file, env = env,
- sessions_structure = Some(deps.sessions_structure), store = Some(store),
+ sessions_structure = Some(sessions_structure), store = Some(store),
phase_changed =
{
case Session.Ready => session.protocol_command("build_session", args_yxml)
--- a/src/Pure/Tools/imports.scala Wed Sep 11 20:48:10 2019 +0200
+++ b/src/Pure/Tools/imports.scala Thu Sep 12 13:33:09 2019 +0200
@@ -99,21 +99,24 @@
select_dirs: List[Path] = Nil,
verbose: Boolean = false) =
{
+ val sessions_structure =
+ Sessions.load_structure(options, dirs = dirs, select_dirs = select_dirs)
+
val deps =
- Sessions.load_structure(options, dirs = dirs, select_dirs = select_dirs).
- selection_deps(options, selection, progress = progress, verbose = verbose).check_errors
+ sessions_structure.selection_deps(options, selection, progress = progress, verbose = verbose).
+ check_errors
val root_keywords = Sessions.root_syntax.keywords
if (operation_imports) {
val report_imports: List[Report] =
- deps.sessions_structure.build_topological_order.map((session_name: String) =>
+ sessions_structure.build_topological_order.map((session_name: String) =>
{
- val info = deps.sessions_structure(session_name)
+ val info = sessions_structure(session_name)
val session_base = deps(session_name)
val declared_imports =
- deps.sessions_structure.imports_requirements(List(session_name)).toSet
+ sessions_structure.imports_requirements(List(session_name)).toSet
val extra_imports =
(for {
@@ -125,18 +128,18 @@
} yield qualifier).toSet
val loaded_imports =
- deps.sessions_structure.imports_requirements(
+ sessions_structure.imports_requirements(
session_base.loaded_theories.keys.map(a =>
session_base.theory_qualifier(session_base.known.theories(a).name)))
.toSet - session_name
val minimal_imports =
loaded_imports.filter(s1 =>
- !loaded_imports.exists(s2 => deps.sessions_structure.imports_graph.is_edge(s1, s2)))
+ !loaded_imports.exists(s2 => sessions_structure.imports_graph.is_edge(s1, s2)))
def make_result(set: Set[String]): Option[List[String]] =
if (set.isEmpty) None
- else Some(deps.sessions_structure.imports_topological_order.filter(set))
+ else Some(sessions_structure.imports_topological_order.filter(set))
Report(info, declared_imports, make_result(extra_imports),
if (loaded_imports == declared_imports - session_name) None
@@ -170,13 +173,13 @@
if (operation_update) {
progress.echo("\nUpdate theory imports" + update_message + ":")
val updates =
- deps.sessions_structure.build_topological_order.flatMap(session_name =>
+ sessions_structure.build_topological_order.flatMap(session_name =>
{
- val info = deps.sessions_structure(session_name)
+ val info = sessions_structure(session_name)
val session_base = deps(session_name)
- val session_resources = new Resources(session_base)
+ val session_resources = new Resources(sessions_structure, session_base)
val imports_base = session_base.get_imports
- val imports_resources = new Resources(imports_base)
+ val imports_resources = new Resources(sessions_structure, imports_base)
def standard_import(qualifier: String, dir: String, s: String): String =
imports_resources.standard_import(session_base, qualifier, dir, s)
--- a/src/Tools/VSCode/src/server.scala Wed Sep 11 20:48:10 2019 +0200
+++ b/src/Tools/VSCode/src/server.scala Thu Sep 12 13:33:09 2019 +0200
@@ -35,7 +35,6 @@
var logic_ancestor: Option[String] = None
var log_file: Option[Path] = None
var logic_requirements = false
- var logic_focus = false
var dirs: List[Path] = Nil
var include_sessions: List[String] = Nil
var logic = default_logic
@@ -47,10 +46,9 @@
Usage: isabelle vscode_server [OPTIONS]
Options are:
- -A NAME ancestor session for options -R and -S (default: parent)
+ -A NAME ancestor session for option -R (default: parent)
-L FILE logging on FILE
-R NAME build image with requirements from other sessions
- -S NAME like option -R, with focus on selected session
-d DIR include session directory
-i NAME include session in name-space of theories
-l NAME logic session name (default ISABELLE_LOGIC=""" + quote(default_logic) + """)
@@ -63,7 +61,6 @@
"A:" -> (arg => logic_ancestor = Some(arg)),
"L:" -> (arg => log_file = Some(Path.explode(File.standard_path(arg)))),
"R:" -> (arg => { logic = arg; logic_requirements = true }),
- "S:" -> (arg => { logic = arg; logic_requirements = true; logic_focus = true }),
"d:" -> (arg => dirs = dirs ::: List(Path.explode(File.standard_path(arg)))),
"i:" -> (arg => include_sessions = include_sessions ::: List(arg)),
"l:" -> (arg => logic = arg),
@@ -79,8 +76,7 @@
val server =
new Server(channel, options, session_name = logic, session_dirs = dirs,
include_sessions = include_sessions, session_ancestor = logic_ancestor,
- session_requirements = logic_requirements, session_focus = logic_focus,
- all_known = !logic_focus, modes = modes, log = log)
+ session_requirements = logic_requirements, modes = modes, log = log)
// prevent spurious garbage on the main protocol channel
val orig_out = System.out
@@ -107,8 +103,6 @@
include_sessions: List[String] = Nil,
session_ancestor: Option[String] = None,
session_requirements: Boolean = false,
- session_focus: Boolean = false,
- all_known: Boolean = false,
modes: List[String] = Nil,
log: Logger = No_Logger)
{
@@ -271,9 +265,9 @@
val base_info =
Sessions.base_info(
options, session_name, dirs = session_dirs, include_sessions = include_sessions,
- session_ancestor = session_ancestor, session_requirements = session_requirements,
- session_focus = session_focus, all_known = all_known)
- val session_base = base_info.check_base
+ session_ancestor = session_ancestor, session_requirements = session_requirements)
+
+ base_info.check_base
def build(no_build: Boolean = false): Build.Results =
Build.build(options, build_heap = true, no_build = no_build, dirs = session_dirs,
@@ -289,7 +283,7 @@
if (!build().ok) { progress.echo(fail_msg); error(fail_msg) }
}
- val resources = new VSCode_Resources(options, session_base, log)
+ val resources = new VSCode_Resources(options, base_info, log)
{
override def commit(change: Session.Change): Unit =
if (change.deps_changed || undefined_blobs(change.version.nodes).nonEmpty)
--- a/src/Tools/VSCode/src/vscode_resources.scala Wed Sep 11 20:48:10 2019 +0200
+++ b/src/Tools/VSCode/src/vscode_resources.scala Thu Sep 12 13:33:09 2019 +0200
@@ -72,9 +72,9 @@
class VSCode_Resources(
val options: Options,
- session_base: Sessions.Base,
+ session_base_info: Sessions.Base_Info,
log: Logger = No_Logger)
- extends Resources(session_base, log = log)
+ extends Resources(session_base_info.sessions_structure, session_base_info.check_base, log = log)
{
resources =>
--- a/src/Tools/jEdit/lib/Tools/jedit Wed Sep 11 20:48:10 2019 +0200
+++ b/src/Tools/jEdit/lib/Tools/jedit Thu Sep 12 13:33:09 2019 +0200
@@ -100,12 +100,11 @@
echo "Usage: isabelle $PRG [OPTIONS] [FILES ...]"
echo
echo " Options are:"
- echo " -A NAME ancestor session for options -R and -S (default: parent)"
+ echo " -A NAME ancestor session for options -R (default: parent)"
echo " -D NAME=X set JVM system property"
echo " -J OPTION add JVM runtime option"
echo " (default $JEDIT_JAVA_SYSTEM_OPTIONS $JEDIT_JAVA_OPTIONS)"
echo " -R NAME build image with requirements from other sessions"
- echo " -S NAME like option -R, with focus on selected session"
echo " -b build only"
echo " -d DIR include session directory"
echo " -f fresh build"
@@ -146,7 +145,6 @@
ML_PROCESS_POLICY=""
JEDIT_LOGIC_ANCESTOR=""
JEDIT_LOGIC_REQUIREMENTS=""
-JEDIT_LOGIC_FOCUS=""
JEDIT_INCLUDE_SESSIONS=""
JEDIT_SESSION_DIRS="-"
JEDIT_LOGIC=""
@@ -157,7 +155,7 @@
function getoptions()
{
OPTIND=1
- while getopts "A:BFD:J:R:S:bd:fi:j:l:m:np:su" OPT
+ while getopts "A:BFD:J:R:bd:fi:j:l:m:np:su" OPT
do
case "$OPT" in
A)
@@ -173,11 +171,6 @@
JEDIT_LOGIC="$OPTARG"
JEDIT_LOGIC_REQUIREMENTS="true"
;;
- S)
- JEDIT_LOGIC="$OPTARG"
- JEDIT_LOGIC_REQUIREMENTS="true"
- JEDIT_LOGIC_FOCUS="true"
- ;;
b)
BUILD_ONLY=true
;;
@@ -426,7 +419,7 @@
if [ "$BUILD_ONLY" = false ]
then
export JEDIT_SESSION_DIRS JEDIT_LOGIC JEDIT_LOGIC_ANCESTOR JEDIT_LOGIC_REQUIREMENTS \
- JEDIT_LOGIC_FOCUS JEDIT_INCLUDE_SESSIONS JEDIT_PRINT_MODE JEDIT_NO_BUILD JEDIT_BUILD_MODE
+ JEDIT_INCLUDE_SESSIONS JEDIT_PRINT_MODE JEDIT_NO_BUILD JEDIT_BUILD_MODE
export JEDIT_ML_PROCESS_POLICY="$ML_PROCESS_POLICY"
classpath "$JEDIT_HOME/dist/jedit.jar"
exec isabelle java -splash:"$(platform_path "$ISABELLE_HOME/lib/logo/isabelle.gif")" \
--- a/src/Tools/jEdit/src/jedit_resources.scala Wed Sep 11 20:48:10 2019 +0200
+++ b/src/Tools/jEdit/src/jedit_resources.scala Thu Sep 12 13:33:09 2019 +0200
@@ -28,7 +28,7 @@
}
class JEdit_Resources private(val session_base_info: Sessions.Base_Info)
- extends Resources(session_base_info.base.platform_path)
+ extends Resources(session_base_info.sessions_structure, session_base_info.base.platform_path)
{
def session_name: String = session_base_info.session
def session_errors: List[String] = session_base_info.errors
--- a/src/Tools/jEdit/src/jedit_sessions.scala Wed Sep 11 20:48:10 2019 +0200
+++ b/src/Tools/jEdit/src/jedit_sessions.scala Thu Sep 12 13:33:09 2019 +0200
@@ -56,7 +56,6 @@
def logic_ancestor: Option[String] = proper_string(Isabelle_System.getenv("JEDIT_LOGIC_ANCESTOR"))
def logic_requirements: Boolean = Isabelle_System.getenv("JEDIT_LOGIC_REQUIREMENTS") == "true"
- def logic_focus: Boolean = Isabelle_System.getenv("JEDIT_LOGIC_FOCUS") == "true"
def logic_include_sessions: List[String] =
space_explode(':', Isabelle_System.getenv("JEDIT_INCLUDE_SESSIONS"))
@@ -124,9 +123,7 @@
include_sessions = logic_include_sessions,
session = logic_name(options),
session_ancestor = logic_ancestor,
- session_requirements = logic_requirements,
- session_focus = logic_focus,
- all_known = !logic_focus)
+ session_requirements = logic_requirements)
def session_build(
options: Options, progress: Progress = No_Progress, no_build: Boolean = false): Int =