proper import qualifier for global theories;
authorwenzelm
Mon Apr 10 16:43:12 2017 +0200 (2017-04-10)
changeset 654572bf0d2fcd506
parent 65456 31e8a86971a8
child 65458 cf504b7a7aa7
proper import qualifier for global theories;
clarified uniqueness;
src/Pure/PIDE/resources.ML
src/Pure/PIDE/resources.scala
src/Pure/Thy/sessions.scala
src/Pure/Tools/build.ML
src/Pure/Tools/build.scala
src/Pure/Tools/ml_process.scala
     1.1 --- a/src/Pure/PIDE/resources.ML	Mon Apr 10 13:30:55 2017 +0200
     1.2 +++ b/src/Pure/PIDE/resources.ML	Mon Apr 10 16:43:12 2017 +0200
     1.3 @@ -8,12 +8,12 @@
     1.4  sig
     1.5    val set_session_base:
     1.6      {default_qualifier: string,
     1.7 -     global_theories: string list,
     1.8 +     global_theories: (string * string) list,
     1.9       loaded_theories: (string * string) list,
    1.10       known_theories: (string * string) list} -> unit
    1.11    val reset_session_base: unit -> unit
    1.12    val default_qualifier: unit -> string
    1.13 -  val global_theory: string -> bool
    1.14 +  val global_theory: string -> string option
    1.15    val loaded_theory: string -> Path.T option
    1.16    val known_theory: string -> Path.T option
    1.17    val master_directory: theory -> Path.T
    1.18 @@ -42,7 +42,7 @@
    1.19  
    1.20  val init_session_base =
    1.21    {default_qualifier = "Draft",
    1.22 -   global_theories = Symtab.make_set [],
    1.23 +   global_theories = Symtab.empty: string Symtab.table,
    1.24     loaded_theories = Symtab.empty: Path.T Symtab.table,
    1.25     known_theories = Symtab.empty: Path.T Symtab.table};
    1.26  
    1.27 @@ -55,7 +55,7 @@
    1.28        {default_qualifier =
    1.29          if default_qualifier <> "" then default_qualifier
    1.30          else #default_qualifier init_session_base,
    1.31 -       global_theories = Symtab.make_set global_theories,
    1.32 +       global_theories = Symtab.make global_theories,
    1.33         loaded_theories = Symtab.make (map (apsnd Path.explode) loaded_theories),
    1.34         known_theories = Symtab.make (map (apsnd Path.explode) known_theories)});
    1.35  
    1.36 @@ -65,7 +65,7 @@
    1.37  fun get_session_base f = f (Synchronized.value global_session_base);
    1.38  
    1.39  fun default_qualifier () = get_session_base #default_qualifier;
    1.40 -fun global_theory a = Symtab.defined (get_session_base #global_theories) a;
    1.41 +fun global_theory a = Symtab.lookup (get_session_base #global_theories) a;
    1.42  fun loaded_theory a = Symtab.lookup (get_session_base #loaded_theories) a;
    1.43  fun known_theory a = Symtab.lookup (get_session_base #known_theories) a;
    1.44  
    1.45 @@ -104,13 +104,15 @@
    1.46  val thy_path = Path.ext "thy";
    1.47  
    1.48  fun theory_qualifier theory =
    1.49 -  Long_Name.qualifier theory;
    1.50 +  (case global_theory theory of
    1.51 +    SOME qualifier => qualifier
    1.52 +  | NONE => Long_Name.qualifier theory);
    1.53  
    1.54  fun import_name qualifier dir s =
    1.55    let
    1.56      val theory0 = Thy_Header.import_name s;
    1.57      val theory =
    1.58 -      if Long_Name.is_qualified theory0 orelse global_theory theory0
    1.59 +      if Long_Name.is_qualified theory0 orelse is_some (global_theory theory0)
    1.60          orelse true (* FIXME *) then theory0
    1.61        else Long_Name.qualify qualifier theory0;
    1.62      val node_name =
     2.1 --- a/src/Pure/PIDE/resources.scala	Mon Apr 10 13:30:55 2017 +0200
     2.2 +++ b/src/Pure/PIDE/resources.scala	Mon Apr 10 16:43:12 2017 +0200
     2.3 @@ -68,13 +68,13 @@
     2.4      else Nil
     2.5  
     2.6    def theory_qualifier(name: Document.Node.Name): String =
     2.7 -    Long_Name.qualifier(name.theory)
     2.8 +    session_base.global_theories.getOrElse(name.theory, Long_Name.qualifier(name.theory))
     2.9  
    2.10    def import_name(qualifier: String, dir: String, s: String): Document.Node.Name =
    2.11    {
    2.12      val theory0 = Thy_Header.import_name(s)
    2.13      val theory =
    2.14 -      if (Long_Name.is_qualified(theory0) || session_base.global_theories.contains(theory0)
    2.15 +      if (Long_Name.is_qualified(theory0) || session_base.global_theories.isDefinedAt(theory0)
    2.16          || true /* FIXME */) theory0
    2.17        else theory0 // FIXME Long_Name.qualify(qualifier, theory0)
    2.18  
     3.1 --- a/src/Pure/Thy/sessions.scala	Mon Apr 10 13:30:55 2017 +0200
     3.2 +++ b/src/Pure/Thy/sessions.scala	Mon Apr 10 16:43:12 2017 +0200
     3.3 @@ -49,7 +49,7 @@
     3.4    }
     3.5  
     3.6    sealed case class Base(
     3.7 -    global_theories: Set[String] = Set.empty,
     3.8 +    global_theories: Map[String, String] = Map.empty,
     3.9      loaded_theories: Map[String, Document.Node.Name] = Map.empty,
    3.10      known_theories: Map[String, Document.Node.Name] = Map.empty,
    3.11      keywords: Thy_Header.Keywords = Nil,
    3.12 @@ -85,7 +85,7 @@
    3.13        verbose: Boolean = false,
    3.14        list_files: Boolean = false,
    3.15        check_keywords: Set[String] = Set.empty,
    3.16 -      global_theories: Set[String] = Set.empty): Deps =
    3.17 +      global_theories: Map[String, String] = Map.empty): Deps =
    3.18    {
    3.19      Deps((Map.empty[String, Base] /: sessions.imports_topological_order)({
    3.20        case (sessions, (session_name, info)) =>
    3.21 @@ -98,7 +98,7 @@
    3.22                case Some(parent) => sessions(parent)
    3.23              }
    3.24            val resources = new Resources(parent_base,
    3.25 -            default_qualifier = info.theory_qualifier getOrElse session_name)
    3.26 +            default_qualifier = info.theory_qualifier(session_name))
    3.27  
    3.28            if (verbose || list_files) {
    3.29              val groups =
    3.30 @@ -211,10 +211,10 @@
    3.31    {
    3.32      def timeout: Time = Time.seconds(options.real("timeout") * options.real("timeout_scale"))
    3.33  
    3.34 -    def theory_qualifier: Option[String] =
    3.35 +    def theory_qualifier(default_qualifier: String): String =
    3.36        options.string("theory_qualifier") match {
    3.37 -        case "" => None
    3.38 -        case qualifier => Some(qualifier)
    3.39 +        case "" => default_qualifier
    3.40 +        case qualifier => qualifier
    3.41        }
    3.42    }
    3.43  
    3.44 @@ -324,17 +324,19 @@
    3.45      def get(name: String): Option[Info] =
    3.46        if (imports_graph.defined(name)) Some(imports_graph.get_node(name)) else None
    3.47  
    3.48 -    def global_theories: Set[String] =
    3.49 -      (Set.empty[String] /:
    3.50 +    def global_theories: Map[String, String] =
    3.51 +      (Map.empty[String, String] /:
    3.52          (for {
    3.53 -          (_, (info, _)) <- imports_graph.iterator
    3.54 -          thy <- info.global_theories.iterator }
    3.55 -         yield (thy, info.pos)))(
    3.56 -          { case (set, (thy, pos)) =>
    3.57 -             if (set.contains(thy))
    3.58 -               error("Duplicate declaration of global theory " + quote(thy) + Position.here(pos))
    3.59 -             else set + thy
    3.60 -           })
    3.61 +          (session_name, (info, _)) <- imports_graph.iterator
    3.62 +          thy <- info.global_theories.iterator } yield (thy, session_name, info)))({
    3.63 +            case (global, (thy, session_name, info)) =>
    3.64 +              val qualifier = info.theory_qualifier(session_name)
    3.65 +              global.get(thy) match {
    3.66 +                case Some(qualifier1) if qualifier != qualifier1 =>
    3.67 +                  error("Duplicate global theory " + quote(thy) + Position.here(info.pos))
    3.68 +                case _ => global + (thy -> qualifier)
    3.69 +              }
    3.70 +          })
    3.71  
    3.72      def selection(select: Selection): (List[String], T) =
    3.73      {
     4.1 --- a/src/Pure/Tools/build.ML	Mon Apr 10 13:30:55 2017 +0200
     4.2 +++ b/src/Pure/Tools/build.ML	Mon Apr 10 16:43:12 2017 +0200
     4.3 @@ -146,7 +146,7 @@
     4.4    name: string,
     4.5    master_dir: Path.T,
     4.6    theories: (Options.T * (string * Position.T) list) list,
     4.7 -  global_theories: string list,
     4.8 +  global_theories: (string * string) list,
     4.9    loaded_theories: (string * string) list,
    4.10    known_theories: (string * string) list};
    4.11  
    4.12 @@ -160,7 +160,7 @@
    4.13          (pair (list (pair string string)) (pair string (pair string (pair string (pair string
    4.14            (pair string
    4.15              (pair (((list (pair Options.decode (list (string #> rpair Position.none))))))
    4.16 -              (pair (list string)
    4.17 +              (pair (list (pair string string))
    4.18                  (pair (list (pair string string)) (list (pair string string)))))))))))))))
    4.19        (YXML.parse_body yxml);
    4.20    in
     5.1 --- a/src/Pure/Tools/build.scala	Mon Apr 10 13:30:55 2017 +0200
     5.2 +++ b/src/Pure/Tools/build.scala	Mon Apr 10 16:43:12 2017 +0200
     5.3 @@ -205,7 +205,7 @@
     5.4                  pair(Path.encode, pair(list(pair(Path.encode, Path.encode)), pair(string,
     5.5                  pair(string, pair(string, pair(string, pair(Path.encode,
     5.6                  pair(list(pair(Options.encode, list(string))),
     5.7 -                pair(list(string),
     5.8 +                pair(list(pair(string, string)),
     5.9                  pair(list(pair(string, string)), list(pair(string, string))))))))))))))))(
    5.10                (Symbol.codes, (command_timings, (do_output, (verbose,
    5.11                  (store.browser_info, (info.document_files, (File.standard_path(graph_file),
    5.12 @@ -224,8 +224,8 @@
    5.13              ML_Syntax.print_string0(File.platform_path(output))
    5.14  
    5.15          if (pide && !Sessions.is_pure(name)) {
    5.16 -          val resources = new Resources(deps(parent),
    5.17 -            default_qualifier = info.theory_qualifier getOrElse name)
    5.18 +          val resources =
    5.19 +            new Resources(deps(parent), default_qualifier = info.theory_qualifier(name))
    5.20            val session = new Session(options, resources)
    5.21            val handler = new Handler(progress, session, name)
    5.22            session.init_protocol_handler(handler)
     6.1 --- a/src/Pure/Tools/ml_process.scala	Mon Apr 10 13:30:55 2017 +0200
     6.2 +++ b/src/Pure/Tools/ml_process.scala	Mon Apr 10 16:43:12 2017 +0200
     6.3 @@ -100,8 +100,7 @@
     6.4                ML_Syntax.print_pair(
     6.5                  ML_Syntax.print_string, ML_Syntax.print_string))(table)
     6.6            List("Resources.set_session_base {default_qualifier = \"\"" +
     6.7 -            ", global_theories = " +
     6.8 -              ML_Syntax.print_list(ML_Syntax.print_string)(base.global_theories.toList) +
     6.9 +            ", global_theories = " + print_table(base.global_theories.toList) +
    6.10              ", loaded_theories = " + print_table(base.dest_loaded_theories) +
    6.11              ", known_theories = " + print_table(base.dest_known_theories) + "}")
    6.12        }