--- a/src/Doc/Isar_Ref/Spec.thy Mon Apr 17 16:39:01 2017 +0200
+++ b/src/Doc/Isar_Ref/Spec.thy Mon Apr 17 21:50:56 2017 +0200
@@ -101,16 +101,15 @@
for syntactic completion. The default for a new keyword is just its name,
but completion may be avoided by defining @{keyword "abbrevs"} with empty
text.
-
+
\<^descr> @{command (global) "end"} concludes the current theory definition. Note
that some other commands, e.g.\ local theory targets \<^theory_text>\<open>locale\<close> or \<^theory_text>\<open>class\<close>
may involve a \<^theory_text>\<open>begin\<close> that needs to be matched by @{command (local) "end"},
according to the usual rules for nested blocks.
\<^descr> \<^theory_text>\<open>thy_deps\<close> visualizes the theory hierarchy as a directed acyclic graph.
- By default, all imported theories are shown, taking the base session as a
- starting point. Alternatively, it is possibly to restrict the full theory
- graph by giving bounds, analogously to @{command_ref class_deps}.
+ By default, all imported theories are shown. This may be restricted by
+ specifying bounds wrt. the theory inclusion relation.
\<close>
@@ -157,11 +156,11 @@
means any results stemming from definitions and proofs in the extended
context will be exported into the enclosing target by lifting over extra
parameters and premises.
-
+
\<^descr> @{command (local) "end"} concludes the current local theory, according to
the nesting of contexts. Note that a global @{command (global) "end"} has a
different meaning: it concludes the theory itself (\secref{sec:begin-thy}).
-
+
\<^descr> \<^theory_text>\<open>private\<close> or \<^theory_text>\<open>qualified\<close> may be given as modifiers before any local
theory command. This restricts name space accesses to the local scope, as
determined by the enclosing \<^theory_text>\<open>context begin \<dots> end\<close> block. Outside its scope,
@@ -189,7 +188,7 @@
on the underlying target infrastructure (locale, type class etc.). The
general idea is as follows, considering a context named \<open>c\<close> with parameter
\<open>x\<close> and assumption \<open>A[x]\<close>.
-
+
Definitions are exported by introducing a global version with additional
arguments; a syntactic abbreviation links the long form with the abstract
version of the target context. For example, \<open>a \<equiv> t[x]\<close> becomes \<open>c.a ?x \<equiv>
@@ -321,7 +320,7 @@
object-logic. This usually covers object-level equality \<open>x = y\<close> and
equivalence \<open>A \<longleftrightarrow> B\<close>. End-users normally need not change the @{attribute
defn} setup.
-
+
Definitions may be presented with explicit arguments on the LHS, as well as
additional conditions, e.g.\ \<open>f x y = t\<close> instead of \<open>f \<equiv> \<lambda>x y. t\<close> and \<open>y \<noteq> 0
\<Longrightarrow> g x y = u\<close> instead of an unrestricted \<open>g \<equiv> \<lambda>x y. u\<close>.
@@ -331,18 +330,18 @@
\<^descr> \<^theory_text>\<open>abbreviation c where eq\<close> introduces a syntactic constant which is
associated with a certain term according to the meta-level equality \<open>eq\<close>.
-
+
Abbreviations participate in the usual type-inference process, but are
expanded before the logic ever sees them. Pretty printing of terms involves
higher-order rewriting with rules stemming from reverted abbreviations. This
needs some care to avoid overlapping or looping syntactic replacements!
-
+
The optional \<open>mode\<close> specification restricts output to a particular print
mode; using ``\<open>input\<close>'' here achieves the effect of one-way abbreviations.
The mode may also include an ``\<^theory_text>\<open>output\<close>'' qualifier that affects the
concrete syntax declared for abbreviations, cf.\ \<^theory_text>\<open>syntax\<close> in
\secref{sec:syn-trans}.
-
+
\<^descr> \<^theory_text>\<open>print_abbrevs\<close> prints all constant abbreviations of the current context;
the ``\<open>!\<close>'' option indicates extra verbosity.
\<close>
@@ -574,12 +573,12 @@
the locale specification. When defining an operation derived from the
parameters, \<^theory_text>\<open>definition\<close> (\secref{sec:term-definitions}) is usually more
appropriate.
-
+
Note that ``\<^theory_text>\<open>(is p\<^sub>1 \<dots> p\<^sub>n)\<close>'' patterns given in the syntax of @{element
"assumes"} and @{element "defines"} above are illegal in locale definitions.
In the long goal format of \secref{sec:goals}, term bindings may be included
as expected, though.
-
+
\<^medskip>
Locale specifications are ``closed up'' by turning the given text into a
predicate definition \<open>loc_axioms\<close> and deriving the original assumptions as
@@ -587,7 +586,7 @@
the newly specified assumptions, omitting the content of included locale
expressions. The full cumulative view is only provided on export, involving
another predicate \<open>loc\<close> that refers to the complete specification text.
-
+
In any case, the predicate arguments are those locale parameters that
actually occur in the respective piece of text. Also these predicates
operate at the meta-level in theory, but the locale packages attempts to
@@ -1111,7 +1110,7 @@
\<^descr> \<^theory_text>\<open>ML_val\<close> and \<^theory_text>\<open>ML_command\<close> are diagnostic versions of \<^theory_text>\<open>ML\<close>, which means
that the context may not be updated. \<^theory_text>\<open>ML_val\<close> echos the bindings produced
at the ML toplevel, but \<^theory_text>\<open>ML_command\<close> is silent.
-
+
\<^descr> \<^theory_text>\<open>setup "text"\<close> changes the current theory context by applying \<open>text\<close>,
which refers to an ML expression of type @{ML_type "theory -> theory"}. This
enables to initialize any object-logic specific tools and packages written
@@ -1223,7 +1222,7 @@
\<alpha>\<^sub>n) t\<close> for the existing type \<open>\<tau>\<close>. Unlike the semantic type definitions in
Isabelle/HOL, type synonyms are merely syntactic abbreviations without any
logical significance. Internally, type synonyms are fully expanded.
-
+
\<^descr> \<^theory_text>\<open>typedecl (\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n) t\<close> declares a new type constructor \<open>t\<close>. If the
object-logic defines a base sort \<open>s\<close>, then the constructor is declared to
operate on that, via the axiomatic type-class instance \<open>t :: (s, \<dots>, s)s\<close>.
--- a/src/Pure/PIDE/command.scala Mon Apr 17 16:39:01 2017 +0200
+++ b/src/Pure/PIDE/command.scala Mon Apr 17 21:50:56 2017 +0200
@@ -451,8 +451,7 @@
val blobs =
files.map(file =>
(Exn.capture {
- val name =
- Document.Node.Name(resources.append(node_name.master_dir, Path.explode(file)))
+ val name = Document.Node.Name(resources.append(node_name, Path.explode(file)))
val blob = get_blob(name).map(blob => ((blob.bytes.sha1_digest, blob.chunk)))
(name, blob)
}).user_error)
--- a/src/Pure/PIDE/rendering.scala Mon Apr 17 16:39:01 2017 +0200
+++ b/src/Pure/PIDE/rendering.scala Mon Apr 17 21:50:56 2017 +0200
@@ -423,6 +423,9 @@
rev_infos.filter(p => p._1 == important).reverse.map(_._2)
}
+ def perhaps_append_file(node_name: Document.Node.Name, name: String): String =
+ if (Path.is_valid(name)) session.resources.append(node_name, Path.explode(name)) else name
+
def tooltips(elements: Markup.Elements, range: Text.Range): Option[Text.Info[List[XML.Tree]]] =
{
val results =
@@ -448,7 +451,7 @@
Some(info + (r0, true, XML.Text(txt1 + txt2)))
case (info, Text.Info(r0, XML.Elem(Markup.Path(name), _))) =>
- val file = session.resources.append_file(snapshot.node_name.master_dir, name)
+ val file = perhaps_append_file(snapshot.node_name, name)
val text =
if (name == file) "file " + quote(file)
else "path " + quote(name) + "\nfile " + quote(file)
--- a/src/Pure/PIDE/resources.ML Mon Apr 17 16:39:01 2017 +0200
+++ b/src/Pure/PIDE/resources.ML Mon Apr 17 21:50:56 2017 +0200
@@ -254,7 +254,7 @@
warning ("Cannot present theory with skipped proofs: " ^ quote name)
else
let val tex_source = Thy_Output.present_thy thy res toks |> Buffer.content;
- in if document then Present.theory_output name tex_source else () end
+ in if document then Present.theory_output (Long_Name.base_name name) tex_source else () end
end;
in (thy, present, size text) end;
--- a/src/Pure/PIDE/resources.scala Mon Apr 17 16:39:01 2017 +0200
+++ b/src/Pure/PIDE/resources.scala Mon Apr 17 21:50:56 2017 +0200
@@ -28,10 +28,8 @@
def append(dir: String, source_path: Path): String =
(Path.explode(dir) + source_path).expand.implode
- def append_file(dir: String, raw_name: String): String =
- if (Path.is_valid(raw_name)) append(dir, Path.explode(raw_name))
- else raw_name
-
+ def append(node_name: Document.Node.Name, source_path: Path): String =
+ append(node_name.master_dir, source_path)
/* source files of Isabelle/ML bootstrap */
@@ -85,7 +83,7 @@
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 {
+ session_base.known_theory(theory) match {
case Some(node_name) => node_name
case None =>
val path = Path.explode(s)
@@ -95,11 +93,12 @@
}
}
+ def import_name(node_name: Document.Node.Name, s: String): Document.Node.Name =
+ import_name(theory_qualifier(node_name), node_name.master_dir, s)
+
def with_thy_reader[A](name: Document.Node.Name, f: Reader[Char] => A): A =
{
- val path = Path.explode(name.node)
- if (!path.is_file) error("No such file: " + path.toString)
-
+ val path = File.check_file(Path.explode(name.node))
val reader = Scan.byte_reader(path.file)
try { f(reader) } finally { reader.close }
}
@@ -118,9 +117,7 @@
" for file " + thy_path(Path.basic(base_name)) + Position.here(pos) +
Completion.report_names(pos, 1, List((base_name, ("theory", base_name)))))
- val imports =
- header.imports.map({ case (s, pos) =>
- (import_name(theory_qualifier(node_name), node_name.master_dir, s), pos) })
+ val imports = header.imports.map({ case (s, pos) => (import_name(node_name, s), pos) })
Document.Node.Header(imports, header.keywords, header.abbrevs)
}
catch { case exn: Throwable => Document.Node.bad_header(Exn.message(exn)) }
@@ -137,16 +134,10 @@
def special_header(name: Document.Node.Name): Option[Document.Node.Header] =
{
- val qualifier = theory_qualifier(name)
- val dir = name.master_dir
-
val imports =
- if (Thy_Header.is_ml_root(name.theory))
- List(import_name(qualifier, dir, Thy_Header.ML_BOOTSTRAP))
- else if (Thy_Header.is_bootstrap(name.theory))
- List(import_name(qualifier, dir, Thy_Header.PURE))
+ if (Thy_Header.is_ml_root(name.theory)) List(import_name(name, Thy_Header.ML_BOOTSTRAP))
+ else if (Thy_Header.is_bootstrap(name.theory)) List(import_name(name, Thy_Header.PURE))
else Nil
-
if (imports.isEmpty) None
else Some(Document.Node.Header(imports.map((_, Position.none))))
}
--- a/src/Pure/Thy/present.ML Mon Apr 17 16:39:01 2017 +0200
+++ b/src/Pure/Thy/present.ML Mon Apr 17 21:50:56 2017 +0200
@@ -7,7 +7,6 @@
signature PRESENT =
sig
val session_name: theory -> string
- val session_graph: string -> (string -> bool) -> theory -> Graph_Display.entry list
val document_enabled: string -> bool
val document_variants: string -> (string * string) list
val init: HTML.symbols -> bool -> bool -> Path.T -> string -> string -> (string * string) list ->
@@ -55,28 +54,6 @@
val session_name = #name o Browser_Info.get;
-(* session graph *)
-
-fun session_graph parent_session parent_loaded =
- let
- val parent_session_name = "session." ^ parent_session;
- val parent_session_node = Graph_Display.content_node ("[" ^ parent_session ^ "]") [];
- fun node_name name = if parent_loaded name then parent_session_name else "theory." ^ name;
- fun theory_entry thy =
- let
- val name = Context.theory_name thy;
- val deps = map (node_name o Context.theory_name) (Theory.parents_of thy);
- in
- if parent_loaded (Context.theory_long_name thy) then NONE
- else SOME ((node_name name, Graph_Display.content_node name []), deps)
- end;
- in
- fn thy =>
- ((parent_session_name, parent_session_node), []) ::
- map_filter theory_entry (Theory.nodes_of thy)
- end;
-
-
(** global browser info state **)
--- a/src/Pure/Thy/sessions.scala Mon Apr 17 16:39:01 2017 +0200
+++ b/src/Pure/Thy/sessions.scala Mon Apr 17 21:50:56 2017 +0200
@@ -24,30 +24,16 @@
def is_pure(name: String): Boolean = name == Thy_Header.PURE
- sealed case class Known_Theories(
- 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)
-
- object Base
+ object Known
{
- def pure(options: Options): Base = session_base(options, Thy_Header.PURE)
+ val empty: Known = Known()
- 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,
- bases: List[Base],
- theories: List[Document.Node.Name]): Known_Theories =
+ def make(local_dir: Path, bases: List[Base], theories: List[Document.Node.Name]): Known =
{
def bases_iterator(local: Boolean) =
for {
base <- bases.iterator
- (_, name) <- (if (local) base.known_theories_local else base.known_theories).iterator
+ (_, name) <- (if (local) base.known.theories_local else base.known.theories).iterator
} yield name
def local_theories_iterator =
@@ -81,42 +67,59 @@
known
else known + (file -> (name :: theories1))
})
- Known_Theories(known_theories, known_theories_local,
+ Known(known_theories, known_theories_local,
known_files.iterator.map(p => (p._1, p._2.reverse)).toMap)
}
}
+ sealed case class Known(
+ theories: Map[String, Document.Node.Name] = Map.empty,
+ theories_local: Map[String, Document.Node.Name] = Map.empty,
+ files: Map[JFile, List[Document.Node.Name]] = Map.empty)
+ {
+ def platform_path: Known =
+ copy(theories = for ((a, b) <- theories) yield (a, b.map(File.platform_path(_))),
+ theories_local = for ((a, b) <- theories_local) yield (a, b.map(File.platform_path(_))),
+ files = for ((a, b) <- files) yield (a, b.map(c => c.map(File.platform_path(_)))))
+ }
+
+ object Base
+ {
+ def pure(options: Options): Base = session_base(options, Thy_Header.PURE)
+
+ def bootstrap(global_theories: Map[String, String]): Base =
+ Base(
+ global_theories = global_theories,
+ keywords = Thy_Header.bootstrap_header,
+ syntax = Thy_Header.bootstrap_syntax)
+ }
+
sealed case class Base(
global_theories: Map[String, String] = 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,
+ known: Known = Known.empty,
keywords: Thy_Header.Keywords = Nil,
syntax: Outer_Syntax = Outer_Syntax.empty,
sources: List[(Path, SHA1.Digest)] = Nil,
session_graph: Graph_Display.Graph = Graph_Display.empty_graph)
{
- def platform_path: Base =
- copy(
- known_theories =
- for ((a, b) <- known_theories) yield (a, b.map(File.platform_path(_))),
- known_theories_local =
- for ((a, b) <- known_theories_local) yield (a, b.map(File.platform_path(_))),
- known_files =
- for ((a, b) <- known_files) yield (a, b.map(c => c.map(File.platform_path(_)))))
+ def platform_path: Base = copy(known = known.platform_path)
def loaded_theory(name: Document.Node.Name): Boolean =
loaded_theories.isDefinedAt(name.theory)
+ def known_theory(name: String): Option[Document.Node.Name] =
+ known.theories.get(name)
+
+ def known_file(file: JFile): Option[Document.Node.Name] =
+ known.files.getOrElse(file.getCanonicalFile, Nil).headOption
+
def dest_known_theories: List[(String, String)] =
- for ((theory, node_name) <- known_theories.toList)
+ for ((theory, node_name) <- known.theories.toList)
yield (theory, node_name.node)
}
- sealed case class Deps(
- session_bases: Map[String, Base],
- all_known_theories: Known_Theories)
+ sealed case class Deps(session_bases: Map[String, Base], all_known: Known)
{
def is_empty: Boolean = session_bases.isEmpty
def apply(name: String): Base = session_bases(name)
@@ -130,7 +133,7 @@
list_files: Boolean = false,
check_keywords: Set[String] = Set.empty,
global_theories: Map[String, String] = Map.empty,
- all_known_theories: Boolean = false): Deps =
+ all_known: Boolean = false): Deps =
{
val session_bases =
(Map.empty[String, Base] /: sessions.imports_topological_order)({
@@ -138,12 +141,16 @@
if (progress.stopped) throw Exn.Interrupt()
try {
- val parent_base =
+ val parent_base: Sessions.Base =
info.parent match {
case None => Base.bootstrap(global_theories)
case Some(parent) => session_bases(parent)
}
- val resources = new Resources(parent_base,
+ val imports_base: Sessions.Base =
+ parent_base.copy(known =
+ Known.make(info.dir, parent_base :: info.imports.map(session_bases(_)), Nil))
+
+ val resources = new Resources(imports_base,
default_qualifier = info.theory_qualifier(session_name))
if (verbose || list_files) {
@@ -168,11 +175,6 @@
}
}
- val known_theories =
- Base.known_theories(info.dir,
- parent_base :: info.imports.map(session_bases(_)),
- thy_deps.deps.map(_.name))
-
val syntax = thy_deps.syntax
val theory_files = thy_deps.deps.map(dep => Path.explode(dep.name.node))
@@ -205,13 +207,11 @@
val base =
Base(global_theories = global_theories,
loaded_theories = thy_deps.loaded_theories,
- known_theories = known_theories.known_theories,
- known_theories_local = known_theories.known_theories_local,
- known_files = known_theories.known_files,
+ known = Known.make(info.dir, List(imports_base), thy_deps.deps.map(_.name)),
keywords = thy_deps.keywords,
syntax = syntax,
sources = all_files.map(p => (p, SHA1.digest(p.file))),
- session_graph = thy_deps.session_graph(info.parent getOrElse "", parent_base))
+ session_graph = thy_deps.session_graph(info.parent getOrElse "", imports_base))
session_bases + (session_name -> base)
}
@@ -222,31 +222,25 @@
}
})
- val known_theories =
- if (all_known_theories)
- Base.known_theories(Path.current, session_bases.toList.map(_._2), Nil)
- else Known_Theories()
-
- Deps(session_bases, known_theories)
+ Deps(session_bases,
+ if (all_known) Known.make(Path.current, session_bases.toList.map(_._2), Nil)
+ else Known.empty)
}
def session_base(
options: Options,
session: String,
dirs: List[Path] = Nil,
- all_known_theories: Boolean = false): Base =
+ all_known: Boolean = false): Base =
{
val full_sessions = load(options, dirs = dirs)
val global_theories = full_sessions.global_theories
val selected_sessions = full_sessions.selection(Selection(sessions = List(session)))._2
- if (all_known_theories) {
+ if (all_known) {
val deps = Sessions.deps(
- full_sessions, global_theories = global_theories, all_known_theories = all_known_theories)
- deps(session).copy(
- known_theories = deps.all_known_theories.known_theories,
- known_theories_local = deps.all_known_theories.known_theories_local,
- known_files = deps.all_known_theories.known_files)
+ full_sessions, global_theories = global_theories, all_known = all_known)
+ deps(session).copy(known = deps.all_known)
}
else
deps(selected_sessions, global_theories = global_theories)(session)
@@ -387,7 +381,7 @@
if (imports_graph.defined(name)) Some(imports_graph.get_node(name)) else None
def global_theories: Map[String, String] =
- (Map.empty[String, String] /:
+ (Thy_Header.bootstrap_global_theories.toMap /:
(for {
(session_name, (info, _)) <- imports_graph.iterator
thy <- info.global_theories.iterator } yield (thy, session_name, info)))({
--- a/src/Pure/Thy/thy_header.scala Mon Apr 17 16:39:01 2017 +0200
+++ b/src/Pure/Thy/thy_header.scala Mon Apr 17 21:50:56 2017 +0200
@@ -73,10 +73,11 @@
val PURE = "Pure"
val ML_BOOTSTRAP = "ML_Bootstrap"
- val ML_ROOT = "ML_Root"
- val ml_roots = List("ROOT0.ML" -> "ML_Root0", "ROOT.ML" -> ML_ROOT)
+ val ml_roots = List("ROOT0.ML" -> "ML_Root0", "ROOT.ML" -> "ML_Root")
val bootstrap_thys = List(PURE, ML_BOOTSTRAP).map(a => a -> ("Bootstrap_" + a))
+ val bootstrap_global_theories = (ml_roots ::: bootstrap_thys).map(p => (p._2 -> PURE))
+
private val Thy_File_Name = new Regex(""".*?([^/\\:]+)\.thy""")
private val Import_Name = new Regex(""".*?([^/\\:]+)""")
--- a/src/Pure/Tools/thy_deps.ML Mon Apr 17 16:39:01 2017 +0200
+++ b/src/Pure/Tools/thy_deps.ML Mon Apr 17 21:50:56 2017 +0200
@@ -6,7 +6,8 @@
signature THY_DEPS =
sig
- val thy_deps: Proof.context -> theory list option * theory list option -> Graph_Display.entry list
+ val thy_deps: Proof.context -> theory list option * theory list option ->
+ Graph_Display.entry list
val thy_deps_cmd: Proof.context ->
(string * Position.T) list option * (string * Position.T) list option -> unit
end;
@@ -14,26 +15,21 @@
structure Thy_Deps: THY_DEPS =
struct
-fun gen_thy_deps _ ctxt (NONE, NONE) =
- let
- val parent_session = Session.get_name ();
- val parent_loaded = is_some o Thy_Info.lookup_theory;
- in Present.session_graph parent_session parent_loaded (Proof_Context.theory_of ctxt) end
- | gen_thy_deps prep_thy ctxt bounds =
- let
- val (upper, lower) = apply2 ((Option.map o map) (prep_thy ctxt)) bounds;
- val rel = Context.subthy o swap;
- val pred =
- (case upper of
- SOME Bs => (fn thy => exists (fn B => rel (thy, B)) Bs)
- | NONE => K true) andf
- (case lower of
- SOME Bs => (fn thy => exists (fn B => rel (B, thy)) Bs)
- | NONE => K true);
- fun node thy =
- ((Context.theory_name thy, Graph_Display.content_node (Context.theory_name thy) []),
- map Context.theory_name (filter pred (Theory.parents_of thy)));
- in map node (filter pred (Theory.nodes_of (Proof_Context.theory_of ctxt))) end;
+fun gen_thy_deps prep_thy ctxt bounds =
+ let
+ val (upper, lower) = apply2 ((Option.map o map) (prep_thy ctxt)) bounds;
+ val rel = Context.subthy o swap;
+ val pred =
+ (case upper of
+ SOME Bs => (fn thy => exists (fn B => rel (thy, B)) Bs)
+ | NONE => K true) andf
+ (case lower of
+ SOME Bs => (fn thy => exists (fn B => rel (B, thy)) Bs)
+ | NONE => K true);
+ fun node thy =
+ ((Context.theory_name thy, Graph_Display.content_node (Context.theory_name thy) []),
+ map Context.theory_name (filter pred (Theory.parents_of thy)));
+ in map node (filter pred (Theory.nodes_of (Proof_Context.theory_of ctxt))) end;
val thy_deps =
gen_thy_deps (fn ctxt => fn thy =>
--- a/src/Tools/VSCode/src/vscode_rendering.scala Mon Apr 17 16:39:01 2017 +0200
+++ b/src/Tools/VSCode/src/vscode_rendering.scala Mon Apr 17 21:50:56 2017 +0200
@@ -237,7 +237,7 @@
range, Nil, VSCode_Rendering.hyperlink_elements, _ =>
{
case (links, Text.Info(_, XML.Elem(Markup.Path(name), _))) =>
- val file = model.resources.append_file(snapshot.node_name.master_dir, name)
+ val file = perhaps_append_file(snapshot.node_name, name)
Some(Line.Node_Range(file) :: links)
case (links, Text.Info(info_range, XML.Elem(Markup(Markup.ENTITY, props), _))) =>
--- a/src/Tools/VSCode/src/vscode_resources.scala Mon Apr 17 16:39:01 2017 +0200
+++ b/src/Tools/VSCode/src/vscode_resources.scala Mon Apr 17 21:50:56 2017 +0200
@@ -61,15 +61,15 @@
def node_file(name: Document.Node.Name): JFile = new JFile(name.node)
def node_name(file: JFile): Document.Node.Name =
- {
- val node = file.getPath
- 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)
+ session_base.known_file(file) getOrElse {
+ val node = file.getPath
+ 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/completion_popup.scala Mon Apr 17 16:39:01 2017 +0200
+++ b/src/Tools/jEdit/src/completion_popup.scala Mon Apr 17 21:50:56 2017 +0200
@@ -195,8 +195,7 @@
if (text == "" || text.endsWith("/")) (path, "")
else (path.dir, path.base.implode)
- val directory =
- new JFile(PIDE.resources.append(rendering.snapshot.node_name.master_dir, dir))
+ val directory = new JFile(PIDE.resources.append(rendering.snapshot.node_name, dir))
val files = directory.listFiles
if (files == null) Nil
else {
--- a/src/Tools/jEdit/src/jedit_rendering.scala Mon Apr 17 16:39:01 2017 +0200
+++ b/src/Tools/jEdit/src/jedit_rendering.scala Mon Apr 17 21:50:56 2017 +0200
@@ -304,7 +304,7 @@
range, Vector.empty, JEdit_Rendering.hyperlink_elements, _ =>
{
case (links, Text.Info(info_range, XML.Elem(Markup.Path(name), _))) =>
- val file = PIDE.resources.append_file(snapshot.node_name.master_dir, name)
+ val file = perhaps_append_file(snapshot.node_name, name)
val link = JEdit_Editor.hyperlink_file(true, file)
Some(links :+ Text.Info(snapshot.convert(info_range), link))
--- a/src/Tools/jEdit/src/jedit_resources.scala Mon Apr 17 16:39:01 2017 +0200
+++ b/src/Tools/jEdit/src/jedit_resources.scala Mon Apr 17 21:50:56 2017 +0200
@@ -25,17 +25,20 @@
{
/* document node name */
+ def known_file(path: String): Option[Document.Node.Name] =
+ JEdit_Lib.check_file(path).flatMap(session_base.known_file(_))
+
def node_name(path: String): Document.Node.Name =
- {
- val vfs = VFSManager.getVFSForPath(path)
- val node = if (vfs.isInstanceOf[FileVFS]) MiscUtilities.resolveSymlinks(path) else path
- 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)
+ known_file(path) getOrElse {
+ val vfs = VFSManager.getVFSForPath(path)
+ val node = if (vfs.isInstanceOf[FileVFS]) MiscUtilities.resolveSymlinks(path) else path
+ 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(buffer: Buffer): Document.Node.Name =
node_name(JEdit_Lib.buffer_name(buffer))
--- a/src/Tools/jEdit/src/theories_dockable.scala Mon Apr 17 16:39:01 2017 +0200
+++ b/src/Tools/jEdit/src/theories_dockable.scala Mon Apr 17 21:50:56 2017 +0200
@@ -172,7 +172,7 @@
val component = Node_Renderer_Component
component.node_name = name
component.checkbox.selected = nodes_required.contains(name)
- component.label.text = name.theory
+ component.label.text = name.theory_base_name
component
}
}