--- a/NEWS Thu Sep 12 14:51:45 2019 +0100
+++ b/NEWS Thu Sep 12 14:51:50 2019 +0100
@@ -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
@@ -75,6 +85,11 @@
*** System ***
+* The command-line tool "isabelle imports" has been discontinued: strict
+checking of session directories enforces session-qualified theory names
+in applications -- users are responsible to specify session ROOT entries
+properly.
+
* Theory export via Isabelle/Scala has been reworked. The former "fact"
name space is now split into individual "thm" items: names are
potentially indexed, such as "foo" for singleton facts, or "bar(1)",
--- a/src/Doc/JEdit/JEdit.thy Thu Sep 12 14:51:45 2019 +0100
+++ b/src/Doc/JEdit/JEdit.thy Thu Sep 12 14:51:50 2019 +0100
@@ -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/Doc/System/Sessions.thy Thu Sep 12 14:51:45 2019 +0100
+++ b/src/Doc/System/Sessions.thy Thu Sep 12 14:51:50 2019 +0100
@@ -484,92 +484,6 @@
\<close>
-section \<open>Maintain theory imports wrt.\ session structure\<close>
-
-text \<open>
- The @{tool_def "imports"} tool helps to maintain theory imports wrt.\
- session structure. It supports three main operations via options \<^verbatim>\<open>-I\<close>,
- \<^verbatim>\<open>-M\<close>, \<^verbatim>\<open>-U\<close>. Its command-line usage is: @{verbatim [display]
-\<open>Usage: isabelle imports [OPTIONS] [SESSIONS ...]
-
- Options are:
- -B NAME include session NAME and all descendants
- -D DIR include session directory and select its sessions
- -I operation: report session imports
- -M operation: Mercurial repository check for theory files
- -R operate on requirements of selected sessions
- -U operation: update theory imports to use session qualifiers
- -X NAME exclude sessions from group NAME and all descendants
- -a select all sessions
- -d DIR include session directory
- -g NAME select session group NAME
- -i incremental update according to session graph structure
- -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME)
- -v verbose
- -x NAME exclude session NAME and all descendants
-
- Maintain theory imports wrt. session structure. At least one operation
- needs to be specified (see options -I -M -U).\<close>}
-
- \<^medskip>
- The selection of sessions and session directories works as for @{tool build}
- via options \<^verbatim>\<open>-B\<close>, \<^verbatim>\<open>-D\<close>, \<^verbatim>\<open>-R\<close>, \<^verbatim>\<open>-X\<close>, \<^verbatim>\<open>-a\<close>, \<^verbatim>\<open>-d\<close>, \<^verbatim>\<open>-g\<close>, \<^verbatim>\<open>-x\<close> (see
- \secref{sec:tool-build}).
-
- \<^medskip>
- Option \<^verbatim>\<open>-o\<close> overrides Isabelle system options as for @{tool build}
- (see \secref{sec:tool-build}).
-
- \<^medskip>
- Option \<^verbatim>\<open>-v\<close> increases the general level of verbosity.
-
- \<^medskip>
- Option \<^verbatim>\<open>-I\<close> determines reports session imports:
-
- \<^descr>[Potential session imports] are derived from old-style use of theory
- files from other sessions via the directory structure. After declaring
- those as \isakeyword{sessions} in the corresponding \<^verbatim>\<open>ROOT\<close> file entry, a
- proper session-qualified theory name can be used (cf.\ option \<^verbatim>\<open>-U\<close>). For
- example, adhoc \<^theory_text>\<open>imports\<close> \<^verbatim>\<open>"~~/src/HOL/Library/Multiset"\<close> becomes formal
- \<^theory_text>\<open>imports\<close> \<^verbatim>\<open>"HOL-Library.Multiset"\<close> after adding \isakeyword{sessions}
- \<^verbatim>\<open>"HOL-Library"\<close> to the \<^verbatim>\<open>ROOT\<close> entry.
-
- \<^descr>[Actual session imports] are derived from the session qualifiers of all
- currently imported theories. This helps to minimize dependencies in the
- session import structure to what is actually required.
-
- \<^medskip>
- Option \<^verbatim>\<open>-M\<close> checks imported theories against the Mercurial repositories of
- the underlying session directories; non-repository directories are ignored.
- This helps to find files that are accidentally ignored, e.g.\ due to
- rearrangements of the session structure.
-
- \<^medskip>
- Option \<^verbatim>\<open>-U\<close> updates theory imports with old-style directory specifications
- to canonical session-qualified theory names, according to the theory name
- space imported via \isakeyword{sessions} within the \<^verbatim>\<open>ROOT\<close> specification.
-
- Option \<^verbatim>\<open>-i\<close> modifies the meaning of option \<^verbatim>\<open>-U\<close> to proceed incrementally,
- following to the session graph structure in bottom-up order. This may
- lead to more accurate results in complex session hierarchies.
-\<close>
-
-subsubsection \<open>Examples\<close>
-
-text \<open>
- Determine potential session imports for some project directory:
- @{verbatim [display] \<open>isabelle imports -I -D 'some/where/My_Project'\<close>}
-
- \<^smallskip>
- Mercurial repository check for some project directory:
- @{verbatim [display] \<open>isabelle imports -M -D 'some/where/My_Project'\<close>}
-
- \<^smallskip>
- Incremental update of theory imports for some project directory:
- @{verbatim [display] \<open>isabelle imports -U -i -D 'some/where/My_Project'\<close>}
-\<close>
-
-
section \<open>Retrieve theory exports \label{sec:tool-export}\<close>
text \<open>
--- a/src/Pure/ML/ml_process.scala Thu Sep 12 14:51:45 2019 +0100
+++ b/src/Pure/ML/ml_process.scala Thu Sep 12 14:51:50 2019 +0100
@@ -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 Thu Sep 12 14:51:45 2019 +0100
+++ b/src/Pure/PIDE/headless.scala Thu Sep 12 14:51:50 2019 +0100
@@ -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 Thu Sep 12 14:51:45 2019 +0100
+++ b/src/Pure/PIDE/protocol.ML Thu Sep 12 14:51:50 2019 +0100
@@ -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 Thu Sep 12 14:51:45 2019 +0100
+++ b/src/Pure/PIDE/protocol.scala Thu Sep 12 14:51:50 2019 +0100
@@ -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 Thu Sep 12 14:51:45 2019 +0100
+++ b/src/Pure/PIDE/resources.ML Thu Sep 12 14:51:50 2019 +0100
@@ -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 Thu Sep 12 14:51:45 2019 +0100
+++ b/src/Pure/PIDE/resources.scala Thu Sep 12 14:51:50 2019 +0100
@@ -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/System/isabelle_tool.scala Thu Sep 12 14:51:45 2019 +0100
+++ b/src/Pure/System/isabelle_tool.scala Thu Sep 12 14:51:50 2019 +0100
@@ -148,7 +148,6 @@
Doc.isabelle_tool,
Dump.isabelle_tool,
Export.isabelle_tool,
- Imports.isabelle_tool,
ML_Process.isabelle_tool,
Mkroot.isabelle_tool,
Options.isabelle_tool,
--- a/src/Pure/Thy/sessions.ML Thu Sep 12 14:51:45 2019 +0100
+++ b/src/Pure/Thy/sessions.ML Thu Sep 12 14:51:50 2019 +0100
@@ -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 Thu Sep 12 14:51:45 2019 +0100
+++ b/src/Pure/Thy/sessions.scala Thu Sep 12 14:51:50 2019 +0100
@@ -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)
@@ -191,8 +182,7 @@
imports getOrElse Base.bootstrap(session_directories, global_theories)
}
- sealed case class Deps(
- sessions_structure: Structure, session_bases: Map[String, Base], all_known: Known)
+ sealed case class Deps(sessions_structure: Structure, session_bases: Map[String, Base])
{
override def toString: String = "Sessions.Deps(" + sessions_structure + ")"
@@ -304,7 +294,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 +361,6 @@
val known =
Known.make(info.dir, List(imports_base),
- sessions = List(info.name -> info.pos),
theories = dependencies.entries,
loaded_files = loaded_files)
@@ -439,10 +428,7 @@
}
})
- val all_known =
- Known.make(Path.current, sessions_structure.imports_topological_order.map(session_bases(_)))
-
- Deps(sessions_structure, session_bases, all_known)
+ Deps(sessions_structure, session_bases)
}
@@ -466,9 +452,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)
@@ -505,7 +489,7 @@
List(
make_info(info.options,
dir_selected = false,
- dir = info.dir,
+ dir = Path.explode("$ISABELLE_TMP_PREFIX"),
chapter = info.chapter,
Session_Entry(
pos = info.pos,
@@ -529,22 +513,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 +674,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 {
@@ -711,7 +687,7 @@
val session = info.name
val canonical_dir = dir.canonical_file
dirs.get(canonical_dir) match {
- case Some(session1) if session1 != session =>
+ case Some(session1) =>
val info1 = info_graph.get_node(session1)
error("Duplicate use of directory " + dir +
"\n for session " + quote(session1) + Position.here(info1.pos) +
@@ -735,10 +711,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 +724,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 +793,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 Thu Sep 12 14:51:45 2019 +0100
+++ b/src/Pure/Tools/build.ML Thu Sep 12 14:51:50 2019 +0100
@@ -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 Thu Sep 12 14:51:45 2019 +0100
+++ b/src/Pure/Tools/build.scala Thu Sep 12 14:51:50 2019 +0100
@@ -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 Thu Sep 12 14:51:45 2019 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,322 +0,0 @@
-/* Title: Pure/Tools/imports.scala
- Author: Makarius
-
-Maintain theory imports wrt. session structure.
-*/
-
-package isabelle
-
-
-import java.io.{File => JFile}
-
-
-object Imports
-{
- /* repository files */
-
- def repository_files(progress: Progress, start: Path, pred: JFile => Boolean = _ => true)
- : List[JFile] =
- Mercurial.find_repository(start) match {
- case None =>
- progress.echo_warning("Ignoring directory " + start + " (no Mercurial repository)")
- Nil
- case Some(hg) =>
- val start_path = start.canonical_file.toPath
- for {
- name <- hg.known_files()
- file = (hg.root + Path.explode(name)).file
- if pred(file) && File.canonical(file).toPath.startsWith(start_path)
- } yield file
- }
-
-
- /* report imports */
-
- sealed case class Report(
- info: Sessions.Info,
- declared_imports: Set[String],
- potential_imports: Option[List[String]],
- actual_imports: Option[List[String]])
- {
- def print(keywords: Keyword.Keywords, result: List[String]): String =
- {
- def print_name(name: String): String = Token.quote_name(keywords, name)
-
- " session " + print_name(info.name) + ": " + result.map(print_name(_)).mkString(" ")
- }
- }
-
-
- /* update imports */
-
- sealed case class Update(range: Text.Range, old_text: String, new_text: String)
- {
- def edits: List[Text.Edit] =
- Text.Edit.replace(range.start, old_text, new_text)
-
- override def toString: String =
- range.toString + ": " + old_text + " -> " + new_text
- }
-
- def update_name(keywords: Keyword.Keywords, pos: Position.T, update: String => String)
- : Option[(JFile, Update)] =
- {
- val file =
- pos match {
- case Position.File(file) => Path.explode(file).canonical_file
- case _ => error("Missing file in position" + Position.here(pos))
- }
-
- val text = File.read(file)
-
- val range =
- pos match {
- case Position.Range(symbol_range) => Symbol.Text_Chunk(text).decode(symbol_range)
- case _ => error("Missing range in position" + Position.here(pos))
- }
-
- Token.read_name(keywords, range.substring(text)) match {
- case Some(tok) =>
- val s1 = tok.source
- val s2 = Token.quote_name(keywords, update(tok.content))
- if (s1 == s2) None else Some((file, Update(range, s1, s2)))
- case None => error("Name token expected" + Position.here(pos))
- }
- }
-
-
- /* collective operations */
-
- def imports(
- options: Options,
- operation_imports: Boolean = false,
- operation_repository_files: Boolean = false,
- operation_update: Boolean = false,
- update_message: String = "",
- progress: Progress = No_Progress,
- selection: Sessions.Selection = Sessions.Selection.empty,
- dirs: List[Path] = Nil,
- select_dirs: List[Path] = Nil,
- verbose: Boolean = false) =
- {
- val deps =
- Sessions.load_structure(options, dirs = dirs, select_dirs = select_dirs).
- 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) =>
- {
- val info = deps.sessions_structure(session_name)
- val session_base = deps(session_name)
-
- val declared_imports =
- deps.sessions_structure.imports_requirements(List(session_name)).toSet
-
- val extra_imports =
- (for {
- a <- session_base.known.theory_names
- if session_base.theory_qualifier(a) == info.name
- b <- deps.all_known.get_file(a.path.file)
- qualifier = session_base.theory_qualifier(b)
- if !declared_imports.contains(qualifier)
- } yield qualifier).toSet
-
- val loaded_imports =
- deps.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)))
-
- def make_result(set: Set[String]): Option[List[String]] =
- if (set.isEmpty) None
- else Some(deps.sessions_structure.imports_topological_order.filter(set))
-
- Report(info, declared_imports, make_result(extra_imports),
- if (loaded_imports == declared_imports - session_name) None
- else make_result(minimal_imports))
- })
-
- progress.echo("\nPotential session imports:")
- for {
- report <- report_imports.sortBy(_.declared_imports.size)
- potential_imports <- report.potential_imports
- } progress.echo(report.print(root_keywords, potential_imports))
-
- progress.echo("\nActual session imports:")
- for {
- report <- report_imports
- actual_imports <- report.actual_imports
- } progress.echo(report.print(root_keywords, actual_imports))
- }
-
- if (operation_repository_files) {
- progress.echo("\nMercurial repository check:")
- val unused_files =
- for {
- (_, dir) <- Sessions.directories(dirs, select_dirs)
- file <- repository_files(progress, dir, file => file.getName.endsWith(".thy"))
- if deps.all_known.get_file(file).isEmpty
- } yield file
- unused_files.foreach(file => progress.echo("unused file " + quote(file.toString)))
- }
-
- if (operation_update) {
- progress.echo("\nUpdate theory imports" + update_message + ":")
- val updates =
- deps.sessions_structure.build_topological_order.flatMap(session_name =>
- {
- val info = deps.sessions_structure(session_name)
- val session_base = deps(session_name)
- val session_resources = new Resources(session_base)
- val imports_base = session_base.get_imports
- val imports_resources = new Resources(imports_base)
-
- def standard_import(qualifier: String, dir: String, s: String): String =
- imports_resources.standard_import(session_base, qualifier, dir, s)
-
- val updates_root =
- for {
- (_, pos) <- info.theories.flatMap(_._2)
- upd <- update_name(root_keywords, pos, standard_import(info.name, info.dir.implode, _))
- } yield upd
-
- val updates_theories =
- (for {
- name <- session_base.known.theories_local.iterator.map(p => p._2.name)
- if session_base.theory_qualifier(name) == info.name
- (_, pos) <- session_resources.check_thy(name, Token.Pos.file(name.node)).imports_pos
- upd <- update_name(session_base.overall_syntax.keywords, pos,
- standard_import(session_base.theory_qualifier(name), name.master_dir, _))
- } yield upd).toList
-
- updates_root ::: updates_theories
- })
-
- val file_updates = (Multi_Map.empty[JFile, Update] /: updates)(_ + _)
- val conflicts =
- file_updates.iterator_list.flatMap({ case (file, upds) =>
- Library.duplicates(upds.sortBy(_.range.start),
- (x: Update, y: Update) => x.range overlaps y.range) match
- {
- case Nil => None
- case bad => Some((file, bad))
- }
- })
- if (conflicts.nonEmpty)
- error(cat_lines(
- conflicts.map({ case (file, bad) =>
- "Conflicting updates for file " + file + bad.mkString("\n ", "\n ", "") })))
-
- for ((file, upds) <- file_updates.iterator_list.toList.sortBy(p => p._1.toString)) {
- progress.echo("file " + quote(file.toString))
- val edits =
- upds.sortBy(upd => - upd.range.start).flatMap(upd =>
- Text.Edit.replace(upd.range.start, upd.old_text, upd.new_text))
- val new_text =
- (File.read(file) /: edits)({ case (text, edit) =>
- edit.edit(text, 0) match {
- case (None, text1) => text1
- case (Some(_), _) => error("Failed to apply edit " + edit + " to file " + file)
- }
- })
- File.write_backup2(Path.explode(File.standard_path(file)), new_text)
- }
- }
- }
-
-
- /* Isabelle tool wrapper */
-
- val isabelle_tool =
- Isabelle_Tool("imports", "maintain theory imports wrt. session structure", args =>
- {
- var base_sessions: List[String] = Nil
- var select_dirs: List[Path] = Nil
- var operation_imports = false
- var operation_repository_files = false
- var requirements = false
- var operation_update = false
- var exclude_session_groups: List[String] = Nil
- var all_sessions = false
- var dirs: List[Path] = Nil
- var session_groups: List[String] = Nil
- var incremental_update = false
- var options = Options.init()
- var verbose = false
- var exclude_sessions: List[String] = Nil
-
- val getopts = Getopts("""
-Usage: isabelle imports [OPTIONS] [SESSIONS ...]
-
- Options are:
- -B NAME include session NAME and all descendants
- -D DIR include session directory and select its sessions
- -I operation: report session imports
- -M operation: Mercurial repository check for theory files
- -R operate on requirements of selected sessions
- -U operation: update theory imports to use session qualifiers
- -X NAME exclude sessions from group NAME and all descendants
- -a select all sessions
- -d DIR include session directory
- -g NAME select session group NAME
- -i incremental update according to session graph structure
- -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME)
- -v verbose
- -x NAME exclude session NAME and all descendants
-
- Maintain theory imports wrt. session structure. At least one operation
- needs to be specified (see options -I -M -U).
-""",
- "B:" -> (arg => base_sessions = base_sessions ::: List(arg)),
- "D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))),
- "I" -> (_ => operation_imports = true),
- "M" -> (_ => operation_repository_files = true),
- "R" -> (_ => requirements = true),
- "U" -> (_ => operation_update = true),
- "X:" -> (arg => exclude_session_groups = exclude_session_groups ::: List(arg)),
- "a" -> (_ => all_sessions = true),
- "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
- "g:" -> (arg => session_groups = session_groups ::: List(arg)),
- "i" -> (_ => incremental_update = true),
- "o:" -> (arg => options = options + arg),
- "v" -> (_ => verbose = true),
- "x:" -> (arg => exclude_sessions = exclude_sessions ::: List(arg)))
-
- val sessions = getopts(args)
- if (args.isEmpty || !(operation_imports || operation_repository_files || operation_update))
- getopts.usage()
-
- val selection =
- Sessions.Selection(requirements, all_sessions, base_sessions, exclude_session_groups,
- exclude_sessions, session_groups, sessions)
-
- val progress = new Console_Progress(verbose = verbose)
-
- if (operation_imports || operation_repository_files ||
- operation_update && !incremental_update)
- {
- imports(options, operation_imports = operation_imports,
- operation_repository_files = operation_repository_files,
- operation_update = operation_update,
- progress = progress, selection = selection, dirs = dirs, select_dirs = select_dirs,
- verbose = verbose)
- }
- else if (operation_update && incremental_update) {
- Sessions.load_structure(options, dirs = dirs, select_dirs = select_dirs).
- selection(selection).imports_topological_order.foreach(name =>
- {
- imports(options, operation_update = operation_update, progress = progress,
- update_message = " for session " + quote(name),
- selection = Sessions.Selection(sessions = List(name)),
- dirs = dirs ::: select_dirs, verbose = verbose)
- })
- }
- })
-}
--- a/src/Pure/build-jars Thu Sep 12 14:51:45 2019 +0100
+++ b/src/Pure/build-jars Thu Sep 12 14:51:50 2019 +0100
@@ -151,7 +151,6 @@
Tools/doc.scala
Tools/dump.scala
Tools/fontforge.scala
- Tools/imports.scala
Tools/main.scala
Tools/mkroot.scala
Tools/print_operation.scala
--- a/src/Tools/VSCode/src/server.scala Thu Sep 12 14:51:45 2019 +0100
+++ b/src/Tools/VSCode/src/server.scala Thu Sep 12 14:51:50 2019 +0100
@@ -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 Thu Sep 12 14:51:45 2019 +0100
+++ b/src/Tools/VSCode/src/vscode_resources.scala Thu Sep 12 14:51:50 2019 +0100
@@ -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 Thu Sep 12 14:51:45 2019 +0100
+++ b/src/Tools/jEdit/lib/Tools/jedit Thu Sep 12 14:51:50 2019 +0100
@@ -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 Thu Sep 12 14:51:45 2019 +0100
+++ b/src/Tools/jEdit/src/jedit_resources.scala Thu Sep 12 14:51:50 2019 +0100
@@ -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 Thu Sep 12 14:51:45 2019 +0100
+++ b/src/Tools/jEdit/src/jedit_sessions.scala Thu Sep 12 14:51:50 2019 +0100
@@ -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 =