more qualifier treatment, but in the end it is still ignored;
authorwenzelm
Sat Apr 08 22:36:32 2017 +0200 (2017-04-08)
changeset 65445e9e7f5f5794c
parent 65444 1f5821b19741
child 65446 ed18feb34c07
more qualifier treatment, but in the end it is still ignored;
src/Pure/PIDE/document.ML
src/Pure/PIDE/document.scala
src/Pure/PIDE/protocol.scala
src/Pure/PIDE/resources.ML
src/Pure/PIDE/resources.scala
src/Pure/Thy/sessions.scala
src/Pure/Thy/thy_info.ML
src/Pure/Tools/build.ML
     1.1 --- a/src/Pure/PIDE/document.ML	Sat Apr 08 21:35:04 2017 +0200
     1.2 +++ b/src/Pure/PIDE/document.ML	Sat Apr 08 22:36:32 2017 +0200
     1.3 @@ -177,9 +177,6 @@
     1.4      SOME eval => Command.eval_finished eval
     1.5    | NONE => false);
     1.6  
     1.7 -fun loaded_theory name =
     1.8 -  get_first Thy_Info.lookup_theory [name, Long_Name.base_name name];
     1.9 -
    1.10  fun get_node nodes name = String_Graph.get_node nodes name
    1.11    handle String_Graph.UNDEF _ => empty_node;
    1.12  fun default_node name = String_Graph.default_node (name, empty_node);
    1.13 @@ -463,7 +460,7 @@
    1.14        val delay_request' = Event_Timer.future (Time.now () + delay);
    1.15  
    1.16        fun finished_import (name, (node, _)) =
    1.17 -        finished_result node orelse is_some (loaded_theory name);
    1.18 +        finished_result node orelse is_some (Thy_Info.lookup_theory name);
    1.19  
    1.20        val nodes = nodes_of (the_version state version_id);
    1.21        val required = make_required nodes;
    1.22 @@ -530,7 +527,7 @@
    1.23          handle ERROR msg => (Output.error_message msg; NONE);
    1.24      val parents_reports =
    1.25        imports |> map_filter (fn (import, pos) =>
    1.26 -        (case loaded_theory import of
    1.27 +        (case Thy_Info.lookup_theory import of
    1.28            NONE =>
    1.29              maybe_end_theory pos
    1.30                (case get_result (snd (the (AList.lookup (op =) deps import))) of
    1.31 @@ -554,7 +551,7 @@
    1.32    else NONE;
    1.33  
    1.34  fun check_theory full name node =
    1.35 -  is_some (loaded_theory name) orelse
    1.36 +  is_some (Thy_Info.lookup_theory name) orelse
    1.37    null (#errors (get_header node)) andalso (not full orelse is_some (get_result node));
    1.38  
    1.39  fun last_common keywords state node_required node0 node =
     2.1 --- a/src/Pure/PIDE/document.scala	Sat Apr 08 21:35:04 2017 +0200
     2.2 +++ b/src/Pure/PIDE/document.scala	Sat Apr 08 22:36:32 2017 +0200
     2.3 @@ -117,7 +117,6 @@
     2.4        def loaded_theory: Name = Name(theory, "", theory)
     2.5        def is_theory: Boolean = theory.nonEmpty
     2.6  
     2.7 -      def theory_qualifier: String = Long_Name.qualifier(theory)
     2.8        def theory_base_name: String = Long_Name.base_name(theory)
     2.9  
    2.10        override def toString: String = if (is_theory) theory else node
     3.1 --- a/src/Pure/PIDE/protocol.scala	Sat Apr 08 21:35:04 2017 +0200
     3.2 +++ b/src/Pure/PIDE/protocol.scala	Sat Apr 08 22:36:32 2017 +0200
     3.3 @@ -359,14 +359,13 @@
     3.4            { case Document.Node.Edits(a) => (Nil, list(pair(option(id), option(id)))(a)) },
     3.5            { case Document.Node.Deps(header) =>
     3.6                val master_dir = File.standard_url(name.master_dir)
     3.7 -              val theory = name.theory_base_name  // FIXME
     3.8                val imports = header.imports.map({ case (a, _) => a.node })
     3.9                val keywords =
    3.10                  header.keywords.map({ case (a, Keyword.Spec(b, c, d)) => (a, ((b, c), d)) })
    3.11                (Nil,
    3.12                  pair(string, pair(string, pair(list(string), pair(list(pair(string,
    3.13                      pair(pair(string, list(string)), list(string)))), list(string)))))(
    3.14 -                (master_dir, (theory, (imports, (keywords, header.errors)))))) },
    3.15 +                (master_dir, (name.theory, (imports, (keywords, header.errors)))))) },
    3.16            { case Document.Node.Perspective(a, b, c) =>
    3.17                (bool_atom(a) :: b.commands.map(cmd => long_atom(cmd.id)),
    3.18                  list(pair(id, pair(string, list(string))))(c.dest)) }))
     4.1 --- a/src/Pure/PIDE/resources.ML	Sat Apr 08 21:35:04 2017 +0200
     4.2 +++ b/src/Pure/PIDE/resources.ML	Sat Apr 08 22:36:32 2017 +0200
     4.3 @@ -19,7 +19,8 @@
     4.4    val master_directory: theory -> Path.T
     4.5    val imports_of: theory -> (string * Position.T) list
     4.6    val thy_path: Path.T -> Path.T
     4.7 -  val import_name: Path.T -> Path.T -> {node_name: Path.T, theory_name: string}
     4.8 +  val theory_qualifier: string -> string
     4.9 +  val import_name: string -> Path.T -> Path.T -> {node_name: Path.T, theory_name: string}
    4.10    val check_thy: Path.T -> string ->
    4.11     {master: Path.T * SHA1.digest, text: string, theory_pos: Position.T,
    4.12      imports: (string * Position.T) list, keywords: Thy_Header.keywords}
    4.13 @@ -39,7 +40,7 @@
    4.14  (* session base *)
    4.15  
    4.16  val init_session_base =
    4.17 -  {default_qualifier = "",
    4.18 +  {default_qualifier = "Draft",
    4.19     global_theories = Symtab.make_set [],
    4.20     loaded_theories = Symtab.empty: Path.T Symtab.table,
    4.21     known_theories = Symtab.empty: Path.T Symtab.table};
    4.22 @@ -50,7 +51,9 @@
    4.23  fun set_session_base {default_qualifier, global_theories, loaded_theories, known_theories} =
    4.24    Synchronized.change global_session_base
    4.25      (fn _ =>
    4.26 -      {default_qualifier = default_qualifier,
    4.27 +      {default_qualifier =
    4.28 +        if default_qualifier <> "" then default_qualifier
    4.29 +        else #default_qualifier init_session_base,
    4.30         global_theories = Symtab.make_set global_theories,
    4.31         loaded_theories = Symtab.make (map (apsnd Path.explode) loaded_theories),
    4.32         known_theories = Symtab.make (map (apsnd Path.explode) known_theories)});
    4.33 @@ -99,12 +102,16 @@
    4.34  
    4.35  val thy_path = Path.ext "thy";
    4.36  
    4.37 -fun import_name dir path =
    4.38 +fun theory_qualifier theory =
    4.39 +  Long_Name.qualifier theory;
    4.40 +
    4.41 +fun import_name qualifier dir path =
    4.42    let
    4.43      val theory0 = Path.implode (Path.base path);
    4.44      val theory =
    4.45 -      if Long_Name.is_qualified theory0 orelse global_theory theory0 then theory0
    4.46 -      else Long_Name.qualify (default_qualifier ()) theory0;
    4.47 +      if Long_Name.is_qualified theory0 orelse global_theory theory0
    4.48 +        orelse true (* FIXME *) then theory0
    4.49 +      else Long_Name.qualify qualifier theory0;
    4.50      val node_name =
    4.51        the (get_first (fn e => e ())
    4.52          [fn () => loaded_theory theory,
     5.1 --- a/src/Pure/PIDE/resources.scala	Sat Apr 08 21:35:04 2017 +0200
     5.2 +++ b/src/Pure/PIDE/resources.scala	Sat Apr 08 22:36:32 2017 +0200
     5.3 @@ -15,7 +15,7 @@
     5.4  
     5.5  class Resources(
     5.6    val session_base: Sessions.Base,
     5.7 -  val default_qualifier: String = "",
     5.8 +  val default_qualifier: String = Sessions.DRAFT,
     5.9    val log: Logger = No_Logger)
    5.10  {
    5.11    val thy_info = new Thy_Info(this)
    5.12 @@ -67,12 +67,16 @@
    5.13      }
    5.14      else Nil
    5.15  
    5.16 -  def import_name(dir: String, s: String): Document.Node.Name =
    5.17 +  def theory_qualifier(name: Document.Node.Name): String =
    5.18 +    Long_Name.qualifier(name.theory)
    5.19 +
    5.20 +  def import_name(qualifier: String, dir: String, s: String): Document.Node.Name =
    5.21    {
    5.22      val theory0 = Thy_Header.base_name(s)
    5.23      val theory =
    5.24 -      if (Long_Name.is_qualified(theory0) || session_base.global_theories.contains(theory0)) theory0
    5.25 -      else Long_Name.qualify(default_qualifier, theory0)
    5.26 +      if (Long_Name.is_qualified(theory0) || session_base.global_theories.contains(theory0)
    5.27 +        || true /* FIXME */) theory0
    5.28 +      else theory0 // FIXME Long_Name.qualify(qualifier, theory0)
    5.29  
    5.30      session_base.loaded_theories.get(theory) orElse
    5.31      session_base.loaded_theories.get(theory0) orElse
    5.32 @@ -109,7 +113,8 @@
    5.33              Completion.report_names(pos, 1, List((base_name, ("theory", base_name)))))
    5.34  
    5.35          val imports =
    5.36 -          header.imports.map({ case (s, pos) => (import_name(node_name.master_dir, s), pos) })
    5.37 +          header.imports.map({ case (s, pos) =>
    5.38 +            (import_name(theory_qualifier(node_name), node_name.master_dir, s), pos) })
    5.39          Document.Node.Header(imports, header.keywords, header.abbrevs)
    5.40        }
    5.41        catch { case exn: Throwable => Document.Node.bad_header(Exn.message(exn)) }
    5.42 @@ -125,13 +130,20 @@
    5.43    /* special header */
    5.44  
    5.45    def special_header(name: Document.Node.Name): Option[Document.Node.Header] =
    5.46 -    if (Thy_Header.is_ml_root(name.theory))
    5.47 -      Some(Document.Node.Header(
    5.48 -        List((import_name(name.master_dir, Thy_Header.ML_BOOTSTRAP), Position.none))))
    5.49 -    else if (Thy_Header.is_bootstrap(name.theory))
    5.50 -      Some(Document.Node.Header(
    5.51 -        List((import_name(name.master_dir, Thy_Header.PURE), Position.none))))
    5.52 -    else None
    5.53 +  {
    5.54 +    val qualifier = theory_qualifier(name)
    5.55 +    val dir = name.master_dir
    5.56 +
    5.57 +    val imports =
    5.58 +      if (Thy_Header.is_ml_root(name.theory))
    5.59 +        List(import_name(qualifier, dir, Thy_Header.ML_BOOTSTRAP))
    5.60 +      else if (Thy_Header.is_bootstrap(name.theory))
    5.61 +        List(import_name(qualifier, dir, Thy_Header.PURE))
    5.62 +      else Nil
    5.63 +
    5.64 +    if (imports.isEmpty) None
    5.65 +    else Some(Document.Node.Header(imports.map((_, Position.none))))
    5.66 +  }
    5.67  
    5.68  
    5.69    /* blobs */
     6.1 --- a/src/Pure/Thy/sessions.scala	Sat Apr 08 21:35:04 2017 +0200
     6.2 +++ b/src/Pure/Thy/sessions.scala	Sat Apr 08 22:36:32 2017 +0200
     6.3 @@ -19,6 +19,8 @@
     6.4  {
     6.5    /* base info and source dependencies */
     6.6  
     6.7 +  val DRAFT = "Draft"
     6.8 +
     6.9    def is_pure(name: String): Boolean = name == Thy_Header.PURE
    6.10  
    6.11    object Base
    6.12 @@ -108,7 +110,8 @@
    6.13            {
    6.14              val root_theories =
    6.15                info.theories.flatMap({ case (_, thys) =>
    6.16 -                thys.map(thy => (resources.import_name(info.dir.implode, thy), info.pos))
    6.17 +                thys.map(thy =>
    6.18 +                  (resources.import_name(session_name, info.dir.implode, thy), info.pos))
    6.19                })
    6.20              val thy_deps = resources.thy_info.dependencies(root_theories)
    6.21  
    6.22 @@ -450,7 +453,7 @@
    6.23          try {
    6.24            val name = entry.name
    6.25  
    6.26 -          if (name == "") error("Bad session name")
    6.27 +          if (name == "" || name == DRAFT) error("Bad session name")
    6.28            if (is_pure(name) && entry.parent.isDefined) error("Illegal parent session")
    6.29            if (!is_pure(name) && !entry.parent.isDefined) error("Missing parent session")
    6.30  
     7.1 --- a/src/Pure/Thy/thy_info.ML	Sat Apr 08 21:35:04 2017 +0200
     7.2 +++ b/src/Pure/Thy/thy_info.ML	Sat Apr 08 22:36:32 2017 +0200
     7.3 @@ -17,6 +17,7 @@
     7.4      {document: bool,
     7.5       symbols: HTML.symbols,
     7.6       last_timing: Toplevel.transition -> Time.time,
     7.7 +     qualifier: string,
     7.8       master_dir: Path.T} -> (string * Position.T) list -> unit
     7.9    val use_thy: string -> unit
    7.10    val script_thy: Position.T -> string -> theory -> theory
    7.11 @@ -285,12 +286,13 @@
    7.12  
    7.13  in
    7.14  
    7.15 -fun require_thys document symbols last_timing initiators dir strs tasks =
    7.16 -      fold_map (require_thy document symbols last_timing initiators dir) strs tasks |>> forall I
    7.17 -and require_thy document symbols last_timing initiators dir (str, require_pos) tasks =
    7.18 +fun require_thys document symbols last_timing initiators qualifier dir strs tasks =
    7.19 +      fold_map (require_thy document symbols last_timing initiators qualifier dir) strs tasks
    7.20 +      |>> forall I
    7.21 +and require_thy document symbols last_timing initiators qualifier dir (str, require_pos) tasks =
    7.22    let
    7.23      val path = Path.expand (Path.explode str);
    7.24 -    val {node_name, theory_name} = Resources.import_name dir path;
    7.25 +    val {node_name, theory_name} = Resources.import_name qualifier dir path;
    7.26      fun check_entry (Task (node_name', _, _)) =
    7.27            if op = (apply2 File.platform_path (node_name, node_name'))
    7.28            then ()
    7.29 @@ -317,6 +319,7 @@
    7.30            val parents = map (base_name o #1) imports;
    7.31            val (parents_current, tasks') =
    7.32              require_thys document symbols last_timing (theory_name :: initiators)
    7.33 +              (Resources.theory_qualifier theory_name)
    7.34                (Path.append dir (master_dir (Option.map #1 deps))) imports tasks;
    7.35  
    7.36            val all_current = current andalso parents_current;
    7.37 @@ -342,14 +345,16 @@
    7.38  
    7.39  (* use theories *)
    7.40  
    7.41 -fun use_theories {document, symbols, last_timing, master_dir} imports =
    7.42 -  schedule_tasks
    7.43 -    (snd (require_thys document symbols last_timing [] master_dir imports String_Graph.empty));
    7.44 +fun use_theories {document, symbols, last_timing, qualifier, master_dir} imports =
    7.45 +  let
    7.46 +    val (_, tasks) =
    7.47 +      require_thys document symbols last_timing [] qualifier master_dir imports String_Graph.empty;
    7.48 +  in schedule_tasks tasks end;
    7.49  
    7.50  fun use_thy name =
    7.51    use_theories
    7.52      {document = false, symbols = HTML.no_symbols, last_timing = K Time.zeroTime,
    7.53 -      master_dir = Path.current}
    7.54 +     qualifier = Resources.default_qualifier (), master_dir = Path.current}
    7.55      [(name, Position.none)];
    7.56  
    7.57  
     8.1 --- a/src/Pure/Tools/build.ML	Sat Apr 08 21:35:04 2017 +0200
     8.2 +++ b/src/Pure/Tools/build.ML	Sat Apr 08 22:36:32 2017 +0200
     8.3 @@ -101,7 +101,7 @@
     8.4  
     8.5  (* build theories *)
     8.6  
     8.7 -fun build_theories symbols last_timing master_dir (options, thys) =
     8.8 +fun build_theories symbols last_timing qualifier master_dir (options, thys) =
     8.9    let
    8.10      val condition = space_explode "," (Options.string options "condition");
    8.11      val conds = filter_out (can getenv_strict) condition;
    8.12 @@ -115,6 +115,7 @@
    8.13            document = Present.document_enabled (Options.string options "document"),
    8.14            symbols = symbols,
    8.15            last_timing = last_timing,
    8.16 +          qualifier = qualifier,
    8.17            master_dir = master_dir}
    8.18          |>
    8.19            (case Options.string options "profiling" of
    8.20 @@ -180,7 +181,7 @@
    8.21  
    8.22      val _ =
    8.23        Resources.set_session_base
    8.24 -        {default_qualifier = "" (* FIXME *),
    8.25 +        {default_qualifier = name,
    8.26           global_theories = global_theories,
    8.27           loaded_theories = loaded_theories,
    8.28           known_theories = known_theories};
    8.29 @@ -204,7 +205,7 @@
    8.30  
    8.31      val res1 =
    8.32        theories |>
    8.33 -        (List.app (build_theories symbols last_timing master_dir)
    8.34 +        (List.app (build_theories symbols last_timing name master_dir)
    8.35            |> session_timing name verbose
    8.36            |> Exn.capture);
    8.37      val res2 = Exn.capture Session.finish ();