--- a/src/Pure/PIDE/document.ML Sat Apr 08 21:35:04 2017 +0200
+++ b/src/Pure/PIDE/document.ML Sat Apr 08 22:36:32 2017 +0200
@@ -177,9 +177,6 @@
SOME eval => Command.eval_finished eval
| NONE => false);
-fun loaded_theory name =
- get_first Thy_Info.lookup_theory [name, Long_Name.base_name name];
-
fun get_node nodes name = String_Graph.get_node nodes name
handle String_Graph.UNDEF _ => empty_node;
fun default_node name = String_Graph.default_node (name, empty_node);
@@ -463,7 +460,7 @@
val delay_request' = Event_Timer.future (Time.now () + delay);
fun finished_import (name, (node, _)) =
- finished_result node orelse is_some (loaded_theory name);
+ finished_result node orelse is_some (Thy_Info.lookup_theory name);
val nodes = nodes_of (the_version state version_id);
val required = make_required nodes;
@@ -530,7 +527,7 @@
handle ERROR msg => (Output.error_message msg; NONE);
val parents_reports =
imports |> map_filter (fn (import, pos) =>
- (case loaded_theory import of
+ (case Thy_Info.lookup_theory import of
NONE =>
maybe_end_theory pos
(case get_result (snd (the (AList.lookup (op =) deps import))) of
@@ -554,7 +551,7 @@
else NONE;
fun check_theory full name node =
- is_some (loaded_theory name) orelse
+ is_some (Thy_Info.lookup_theory name) orelse
null (#errors (get_header node)) andalso (not full orelse is_some (get_result node));
fun last_common keywords state node_required node0 node =
--- a/src/Pure/PIDE/document.scala Sat Apr 08 21:35:04 2017 +0200
+++ b/src/Pure/PIDE/document.scala Sat Apr 08 22:36:32 2017 +0200
@@ -117,7 +117,6 @@
def loaded_theory: Name = Name(theory, "", theory)
def is_theory: Boolean = theory.nonEmpty
- def theory_qualifier: String = Long_Name.qualifier(theory)
def theory_base_name: String = Long_Name.base_name(theory)
override def toString: String = if (is_theory) theory else node
--- a/src/Pure/PIDE/protocol.scala Sat Apr 08 21:35:04 2017 +0200
+++ b/src/Pure/PIDE/protocol.scala Sat Apr 08 22:36:32 2017 +0200
@@ -359,14 +359,13 @@
{ case Document.Node.Edits(a) => (Nil, list(pair(option(id), option(id)))(a)) },
{ case Document.Node.Deps(header) =>
val master_dir = File.standard_url(name.master_dir)
- val theory = name.theory_base_name // FIXME
val imports = header.imports.map({ case (a, _) => a.node })
val keywords =
header.keywords.map({ case (a, Keyword.Spec(b, c, d)) => (a, ((b, c), d)) })
(Nil,
pair(string, pair(string, pair(list(string), pair(list(pair(string,
pair(pair(string, list(string)), list(string)))), list(string)))))(
- (master_dir, (theory, (imports, (keywords, header.errors)))))) },
+ (master_dir, (name.theory, (imports, (keywords, header.errors)))))) },
{ case Document.Node.Perspective(a, b, c) =>
(bool_atom(a) :: b.commands.map(cmd => long_atom(cmd.id)),
list(pair(id, pair(string, list(string))))(c.dest)) }))
--- a/src/Pure/PIDE/resources.ML Sat Apr 08 21:35:04 2017 +0200
+++ b/src/Pure/PIDE/resources.ML Sat Apr 08 22:36:32 2017 +0200
@@ -19,7 +19,8 @@
val master_directory: theory -> Path.T
val imports_of: theory -> (string * Position.T) list
val thy_path: Path.T -> Path.T
- val import_name: Path.T -> Path.T -> {node_name: Path.T, theory_name: string}
+ val theory_qualifier: string -> string
+ val import_name: string -> Path.T -> Path.T -> {node_name: Path.T, theory_name: string}
val check_thy: Path.T -> string ->
{master: Path.T * SHA1.digest, text: string, theory_pos: Position.T,
imports: (string * Position.T) list, keywords: Thy_Header.keywords}
@@ -39,7 +40,7 @@
(* session base *)
val init_session_base =
- {default_qualifier = "",
+ {default_qualifier = "Draft",
global_theories = Symtab.make_set [],
loaded_theories = Symtab.empty: Path.T Symtab.table,
known_theories = Symtab.empty: Path.T Symtab.table};
@@ -50,7 +51,9 @@
fun set_session_base {default_qualifier, global_theories, loaded_theories, known_theories} =
Synchronized.change global_session_base
(fn _ =>
- {default_qualifier = default_qualifier,
+ {default_qualifier =
+ if default_qualifier <> "" then default_qualifier
+ else #default_qualifier init_session_base,
global_theories = Symtab.make_set global_theories,
loaded_theories = Symtab.make (map (apsnd Path.explode) loaded_theories),
known_theories = Symtab.make (map (apsnd Path.explode) known_theories)});
@@ -99,12 +102,16 @@
val thy_path = Path.ext "thy";
-fun import_name dir path =
+fun theory_qualifier theory =
+ Long_Name.qualifier theory;
+
+fun import_name qualifier dir path =
let
val theory0 = Path.implode (Path.base path);
val theory =
- if Long_Name.is_qualified theory0 orelse global_theory theory0 then theory0
- else Long_Name.qualify (default_qualifier ()) theory0;
+ if Long_Name.is_qualified theory0 orelse global_theory theory0
+ orelse true (* FIXME *) then theory0
+ else Long_Name.qualify qualifier theory0;
val node_name =
the (get_first (fn e => e ())
[fn () => loaded_theory theory,
--- a/src/Pure/PIDE/resources.scala Sat Apr 08 21:35:04 2017 +0200
+++ b/src/Pure/PIDE/resources.scala Sat Apr 08 22:36:32 2017 +0200
@@ -15,7 +15,7 @@
class Resources(
val session_base: Sessions.Base,
- val default_qualifier: String = "",
+ val default_qualifier: String = Sessions.DRAFT,
val log: Logger = No_Logger)
{
val thy_info = new Thy_Info(this)
@@ -67,12 +67,16 @@
}
else Nil
- def import_name(dir: String, s: String): Document.Node.Name =
+ def theory_qualifier(name: Document.Node.Name): String =
+ Long_Name.qualifier(name.theory)
+
+ def import_name(qualifier: String, dir: String, s: String): Document.Node.Name =
{
val theory0 = Thy_Header.base_name(s)
val theory =
- if (Long_Name.is_qualified(theory0) || session_base.global_theories.contains(theory0)) theory0
- else Long_Name.qualify(default_qualifier, theory0)
+ if (Long_Name.is_qualified(theory0) || session_base.global_theories.contains(theory0)
+ || true /* FIXME */) theory0
+ else theory0 // FIXME Long_Name.qualify(qualifier, theory0)
session_base.loaded_theories.get(theory) orElse
session_base.loaded_theories.get(theory0) orElse
@@ -109,7 +113,8 @@
Completion.report_names(pos, 1, List((base_name, ("theory", base_name)))))
val imports =
- header.imports.map({ case (s, pos) => (import_name(node_name.master_dir, s), pos) })
+ header.imports.map({ case (s, pos) =>
+ (import_name(theory_qualifier(node_name), node_name.master_dir, s), pos) })
Document.Node.Header(imports, header.keywords, header.abbrevs)
}
catch { case exn: Throwable => Document.Node.bad_header(Exn.message(exn)) }
@@ -125,13 +130,20 @@
/* special header */
def special_header(name: Document.Node.Name): Option[Document.Node.Header] =
- if (Thy_Header.is_ml_root(name.theory))
- Some(Document.Node.Header(
- List((import_name(name.master_dir, Thy_Header.ML_BOOTSTRAP), Position.none))))
- else if (Thy_Header.is_bootstrap(name.theory))
- Some(Document.Node.Header(
- List((import_name(name.master_dir, Thy_Header.PURE), Position.none))))
- else None
+ {
+ 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))
+ else Nil
+
+ if (imports.isEmpty) None
+ else Some(Document.Node.Header(imports.map((_, Position.none))))
+ }
/* blobs */
--- a/src/Pure/Thy/sessions.scala Sat Apr 08 21:35:04 2017 +0200
+++ b/src/Pure/Thy/sessions.scala Sat Apr 08 22:36:32 2017 +0200
@@ -19,6 +19,8 @@
{
/* base info and source dependencies */
+ val DRAFT = "Draft"
+
def is_pure(name: String): Boolean = name == Thy_Header.PURE
object Base
@@ -108,7 +110,8 @@
{
val root_theories =
info.theories.flatMap({ case (_, thys) =>
- thys.map(thy => (resources.import_name(info.dir.implode, thy), info.pos))
+ thys.map(thy =>
+ (resources.import_name(session_name, info.dir.implode, thy), info.pos))
})
val thy_deps = resources.thy_info.dependencies(root_theories)
@@ -450,7 +453,7 @@
try {
val name = entry.name
- if (name == "") error("Bad session name")
+ if (name == "" || name == DRAFT) error("Bad session name")
if (is_pure(name) && entry.parent.isDefined) error("Illegal parent session")
if (!is_pure(name) && !entry.parent.isDefined) error("Missing parent session")
--- a/src/Pure/Thy/thy_info.ML Sat Apr 08 21:35:04 2017 +0200
+++ b/src/Pure/Thy/thy_info.ML Sat Apr 08 22:36:32 2017 +0200
@@ -17,6 +17,7 @@
{document: bool,
symbols: HTML.symbols,
last_timing: Toplevel.transition -> Time.time,
+ qualifier: string,
master_dir: Path.T} -> (string * Position.T) list -> unit
val use_thy: string -> unit
val script_thy: Position.T -> string -> theory -> theory
@@ -285,12 +286,13 @@
in
-fun require_thys document symbols last_timing initiators dir strs tasks =
- fold_map (require_thy document symbols last_timing initiators dir) strs tasks |>> forall I
-and require_thy document symbols last_timing initiators dir (str, require_pos) tasks =
+fun require_thys document symbols last_timing initiators qualifier dir strs tasks =
+ fold_map (require_thy document symbols last_timing initiators qualifier dir) strs tasks
+ |>> forall I
+and require_thy document symbols last_timing initiators qualifier dir (str, require_pos) tasks =
let
val path = Path.expand (Path.explode str);
- val {node_name, theory_name} = Resources.import_name dir path;
+ val {node_name, theory_name} = Resources.import_name qualifier dir path;
fun check_entry (Task (node_name', _, _)) =
if op = (apply2 File.platform_path (node_name, node_name'))
then ()
@@ -317,6 +319,7 @@
val parents = map (base_name o #1) imports;
val (parents_current, tasks') =
require_thys document symbols last_timing (theory_name :: initiators)
+ (Resources.theory_qualifier theory_name)
(Path.append dir (master_dir (Option.map #1 deps))) imports tasks;
val all_current = current andalso parents_current;
@@ -342,14 +345,16 @@
(* use theories *)
-fun use_theories {document, symbols, last_timing, master_dir} imports =
- schedule_tasks
- (snd (require_thys document symbols last_timing [] master_dir imports String_Graph.empty));
+fun use_theories {document, symbols, last_timing, qualifier, master_dir} imports =
+ let
+ val (_, tasks) =
+ require_thys document symbols last_timing [] qualifier master_dir imports String_Graph.empty;
+ in schedule_tasks tasks end;
fun use_thy name =
use_theories
{document = false, symbols = HTML.no_symbols, last_timing = K Time.zeroTime,
- master_dir = Path.current}
+ qualifier = Resources.default_qualifier (), master_dir = Path.current}
[(name, Position.none)];
--- a/src/Pure/Tools/build.ML Sat Apr 08 21:35:04 2017 +0200
+++ b/src/Pure/Tools/build.ML Sat Apr 08 22:36:32 2017 +0200
@@ -101,7 +101,7 @@
(* build theories *)
-fun build_theories symbols last_timing master_dir (options, thys) =
+fun build_theories symbols last_timing qualifier master_dir (options, thys) =
let
val condition = space_explode "," (Options.string options "condition");
val conds = filter_out (can getenv_strict) condition;
@@ -115,6 +115,7 @@
document = Present.document_enabled (Options.string options "document"),
symbols = symbols,
last_timing = last_timing,
+ qualifier = qualifier,
master_dir = master_dir}
|>
(case Options.string options "profiling" of
@@ -180,7 +181,7 @@
val _ =
Resources.set_session_base
- {default_qualifier = "" (* FIXME *),
+ {default_qualifier = name,
global_theories = global_theories,
loaded_theories = loaded_theories,
known_theories = known_theories};
@@ -204,7 +205,7 @@
val res1 =
theories |>
- (List.app (build_theories symbols last_timing master_dir)
+ (List.app (build_theories symbols last_timing name master_dir)
|> session_timing name verbose
|> Exn.capture);
val res2 = Exn.capture Session.finish ();