session-qualified theory names are mandatory;
authorwenzelm
Thu Sep 28 15:11:32 2017 +0200 (20 months ago)
changeset 667124c98c929a12a
parent 66711 80fa1401cf76
child 66713 afba7ffd6492
session-qualified theory names are mandatory;
NEWS
src/Pure/ML/ml_process.scala
src/Pure/PIDE/protocol.ML
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.scala
src/Pure/Tools/build.ML
src/Pure/Tools/build.scala
     1.1 --- a/NEWS	Thu Sep 28 11:53:55 2017 +0200
     1.2 +++ b/NEWS	Thu Sep 28 15:11:32 2017 +0200
     1.3 @@ -7,6 +7,14 @@
     1.4  New in this Isabelle version
     1.5  ----------------------------
     1.6  
     1.7 +*** General ***
     1.8 +
     1.9 +* Session-qualified theory names are mandatory: it is no longer possible
    1.10 +to refer to unqualified theories from the parent session.
    1.11 +INCOMPATIBILITY for old developments that have not been updated to
    1.12 +Isabelle2017 yet (using the "isabelle imports" tool).
    1.13 +
    1.14 +
    1.15  *** HOL ***
    1.16  
    1.17  * SMT module:
     2.1 --- a/src/Pure/ML/ml_process.scala	Thu Sep 28 11:53:55 2017 +0200
     2.2 +++ b/src/Pure/ML/ml_process.scala	Thu Sep 28 15:11:32 2017 +0200
     2.3 @@ -99,9 +99,11 @@
     2.4              ML_Syntax.print_list(
     2.5                ML_Syntax.print_pair(
     2.6                  ML_Syntax.print_string, ML_Syntax.print_string))(table)
     2.7 +          def print_list(list: List[String]): String =
     2.8 +            ML_Syntax.print_list(ML_Syntax.print_string)(list)
     2.9            List("Resources.init_session_base" +
    2.10              " {global_theories = " + print_table(base.global_theories.toList) +
    2.11 -            ", loaded_theories = " + print_table(base.loaded_theories.toList) +
    2.12 +            ", loaded_theories = " + print_list(base.loaded_theories.toList) +
    2.13              ", known_theories = " + print_table(base.dest_known_theories) + "}")
    2.14        }
    2.15  
     3.1 --- a/src/Pure/PIDE/protocol.ML	Thu Sep 28 11:53:55 2017 +0200
     3.2 +++ b/src/Pure/PIDE/protocol.ML	Thu Sep 28 15:11:32 2017 +0200
     3.3 @@ -22,10 +22,11 @@
     3.4      (fn [global_theories_yxml, loaded_theories_yxml, known_theories_yxml] =>
     3.5        let
     3.6          val decode_table = YXML.parse_body #> let open XML.Decode in list (pair string string) end;
     3.7 +        val decode_list = YXML.parse_body #> let open XML.Decode in list string end;
     3.8        in
     3.9          Resources.init_session_base
    3.10            {global_theories = decode_table global_theories_yxml,
    3.11 -           loaded_theories = decode_table loaded_theories_yxml,
    3.12 +           loaded_theories = decode_list loaded_theories_yxml,
    3.13             known_theories = decode_table known_theories_yxml}
    3.14        end);
    3.15  
     4.1 --- a/src/Pure/PIDE/protocol.scala	Thu Sep 28 11:53:55 2017 +0200
     4.2 +++ b/src/Pure/PIDE/protocol.scala	Thu Sep 28 15:11:32 2017 +0200
     4.3 @@ -316,12 +316,18 @@
     4.4      Symbol.encode_yxml(list(pair(string, string))(table))
     4.5    }
     4.6  
     4.7 +  private def encode_list(lst: List[String]): String =
     4.8 +  {
     4.9 +    import XML.Encode._
    4.10 +    Symbol.encode_yxml(list(string)(lst))
    4.11 +  }
    4.12 +
    4.13    def session_base(resources: Resources)
    4.14    {
    4.15      val base = resources.session_base.standard_path
    4.16      protocol_command("Prover.session_base",
    4.17        encode_table(base.global_theories.toList),
    4.18 -      encode_table(base.loaded_theories.toList),
    4.19 +      encode_list(base.loaded_theories.toList),
    4.20        encode_table(base.dest_known_theories))
    4.21    }
    4.22  
     5.1 --- a/src/Pure/PIDE/resources.ML	Thu Sep 28 11:53:55 2017 +0200
     5.2 +++ b/src/Pure/PIDE/resources.ML	Thu Sep 28 15:11:32 2017 +0200
     5.3 @@ -9,11 +9,11 @@
     5.4    val default_qualifier: string
     5.5    val init_session_base:
     5.6      {global_theories: (string * string) list,
     5.7 -     loaded_theories: (string * string) list,
     5.8 +     loaded_theories: string list,
     5.9       known_theories: (string * string) list} -> unit
    5.10    val finish_session_base: unit -> unit
    5.11    val global_theory: string -> string option
    5.12 -  val loaded_theory: string -> string option
    5.13 +  val loaded_theory: string -> bool
    5.14    val known_theory: string -> Path.T option
    5.15    val master_directory: theory -> Path.T
    5.16    val imports_of: theory -> (string * Position.T) list
    5.17 @@ -39,7 +39,7 @@
    5.18  
    5.19  val empty_session_base =
    5.20    {global_theories = Symtab.empty: string Symtab.table,
    5.21 -   loaded_theories = Symtab.empty: string Symtab.table,
    5.22 +   loaded_theories = Symtab.empty: unit Symtab.table,
    5.23     known_theories = Symtab.empty: Path.T Symtab.table};
    5.24  
    5.25  val global_session_base =
    5.26 @@ -49,7 +49,7 @@
    5.27    Synchronized.change global_session_base
    5.28      (fn _ =>
    5.29        {global_theories = Symtab.make global_theories,
    5.30 -       loaded_theories = Symtab.make loaded_theories,
    5.31 +       loaded_theories = Symtab.make_set loaded_theories,
    5.32         known_theories = Symtab.make (map (apsnd Path.explode) known_theories)});
    5.33  
    5.34  fun finish_session_base () =
    5.35 @@ -62,7 +62,7 @@
    5.36  fun get_session_base f = f (Synchronized.value global_session_base);
    5.37  
    5.38  fun global_theory a = Symtab.lookup (get_session_base #global_theories) a;
    5.39 -fun loaded_theory a = Symtab.lookup (get_session_base #loaded_theories) a;
    5.40 +fun loaded_theory a = Symtab.defined (get_session_base #loaded_theories) a;
    5.41  fun known_theory a = Symtab.lookup (get_session_base #known_theories) a;
    5.42  
    5.43  
    5.44 @@ -107,15 +107,14 @@
    5.45      SOME qualifier => qualifier
    5.46    | NONE => Long_Name.qualifier theory);
    5.47  
    5.48 -fun theory_name qualifier theory0 =
    5.49 -  (case loaded_theory theory0 of
    5.50 -    SOME theory => (true, theory)
    5.51 -  | NONE =>
    5.52 -      let val theory =
    5.53 -        if Long_Name.is_qualified theory0 orelse is_some (global_theory theory0)
    5.54 -        then theory0
    5.55 -        else Long_Name.qualify qualifier theory0
    5.56 -      in (false, theory) end);
    5.57 +fun theory_name qualifier theory =
    5.58 +  if loaded_theory theory then (true, theory)
    5.59 +  else
    5.60 +    let val theory' =
    5.61 +      if Long_Name.is_qualified theory orelse is_some (global_theory theory)
    5.62 +      then theory
    5.63 +      else Long_Name.qualify qualifier theory
    5.64 +    in (false, theory') end;
    5.65  
    5.66  fun import_name qualifier dir s =
    5.67    (case theory_name qualifier (Thy_Header.import_name s) of
     6.1 --- a/src/Pure/PIDE/resources.scala	Thu Sep 28 11:53:55 2017 +0200
     6.2 +++ b/src/Pure/PIDE/resources.scala	Thu Sep 28 15:11:32 2017 +0200
     6.3 @@ -88,15 +88,14 @@
     6.4    def theory_qualifier(name: Document.Node.Name): String =
     6.5      session_base.global_theories.getOrElse(name.theory, Long_Name.qualifier(name.theory))
     6.6  
     6.7 -  def theory_name(qualifier: String, theory0: String): (Boolean, String) =
     6.8 -    session_base.loaded_theories.get(theory0) match {
     6.9 -      case Some(theory) => (true, theory)
    6.10 -      case None =>
    6.11 -        val theory =
    6.12 -          if (Long_Name.is_qualified(theory0) || session_base.global_theories.isDefinedAt(theory0))
    6.13 -            theory0
    6.14 -          else Long_Name.qualify(qualifier, theory0)
    6.15 -        (false, theory)
    6.16 +  def theory_name(qualifier: String, theory: String): (Boolean, String) =
    6.17 +    if (session_base.loaded_theory(theory)) (true, theory)
    6.18 +    else {
    6.19 +      val theory1 =
    6.20 +        if (Long_Name.is_qualified(theory) || session_base.global_theories.isDefinedAt(theory))
    6.21 +          theory
    6.22 +        else Long_Name.qualify(qualifier, theory)
    6.23 +      (false, theory1)
    6.24      }
    6.25  
    6.26    def import_name(qualifier: String, dir: String, s: String): Document.Node.Name =
     7.1 --- a/src/Pure/Thy/sessions.scala	Thu Sep 28 11:53:55 2017 +0200
     7.2 +++ b/src/Pure/Thy/sessions.scala	Thu Sep 28 15:11:32 2017 +0200
     7.3 @@ -115,7 +115,7 @@
     7.4    sealed case class Base(
     7.5      pos: Position.T = Position.none,
     7.6      global_theories: Map[String, String] = Map.empty,
     7.7 -    loaded_theories: Map[String, String] = Map.empty,
     7.8 +    loaded_theories: Set[String] = Set.empty,
     7.9      known: Known = Known.empty,
    7.10      keywords: Thy_Header.Keywords = Nil,
    7.11      syntax: Outer_Syntax = Outer_Syntax.empty,
    7.12 @@ -127,8 +127,8 @@
    7.13      def platform_path: Base = copy(known = known.platform_path)
    7.14      def standard_path: Base = copy(known = known.standard_path)
    7.15  
    7.16 -    def loaded_theory(name: Document.Node.Name): Boolean =
    7.17 -      loaded_theories.isDefinedAt(name.theory)
    7.18 +    def loaded_theory(name: String): Boolean = loaded_theories.contains(name)
    7.19 +    def loaded_theory(name: Document.Node.Name): Boolean = loaded_theory(name.theory)
    7.20  
    7.21      def known_theory(name: String): Option[Document.Node.Name] =
    7.22        known.theories.get(name)
     8.1 --- a/src/Pure/Thy/thy_info.scala	Thu Sep 28 11:53:55 2017 +0200
     8.2 +++ b/src/Pure/Thy/thy_info.scala	Thu Sep 28 15:11:32 2017 +0200
     8.3 @@ -61,13 +61,8 @@
     8.4      lazy val syntax: Outer_Syntax =
     8.5        resources.session_base.syntax.add_keywords(keywords).add_abbrevs(abbrevs)
     8.6  
     8.7 -    def loaded_theories: Map[String, String] =
     8.8 -      (resources.session_base.loaded_theories /: rev_deps) {
     8.9 -        case (loaded, dep) =>
    8.10 -          val name = dep.name
    8.11 -          loaded + (name.theory -> name.theory) +
    8.12 -            (name.theory_base_name -> name.theory)  // legacy
    8.13 -      }
    8.14 +    def loaded_theories: Set[String] =
    8.15 +      resources.session_base.loaded_theories ++ rev_deps.map(dep => dep.name.theory)
    8.16  
    8.17      def loaded_files: List[(String, List[Path])] =
    8.18      {
     9.1 --- a/src/Pure/Tools/build.ML	Thu Sep 28 11:53:55 2017 +0200
     9.2 +++ b/src/Pure/Tools/build.ML	Thu Sep 28 15:11:32 2017 +0200
     9.3 @@ -147,7 +147,7 @@
     9.4    master_dir: Path.T,
     9.5    theories: (Options.T * (string * Position.T) list) list,
     9.6    global_theories: (string * string) list,
     9.7 -  loaded_theories: (string * string) list,
     9.8 +  loaded_theories: string list,
     9.9    known_theories: (string * string) list};
    9.10  
    9.11  fun decode_args yxml =
    9.12 @@ -162,7 +162,7 @@
    9.13            (pair string
    9.14              (pair (((list (pair Options.decode (list (pair string position))))))
    9.15                (pair (list (pair string string))
    9.16 -                (pair (list (pair string string)) (list (pair string string)))))))))))))))
    9.17 +                (pair (list string) (list (pair string string)))))))))))))))
    9.18        (YXML.parse_body yxml);
    9.19    in
    9.20      Args {symbol_codes = symbol_codes, command_timings = command_timings, do_output = do_output,
    10.1 --- a/src/Pure/Tools/build.scala	Thu Sep 28 11:53:55 2017 +0200
    10.2 +++ b/src/Pure/Tools/build.scala	Thu Sep 28 15:11:32 2017 +0200
    10.3 @@ -209,7 +209,7 @@
    10.4                  pair(Path.encode, pair(list(pair(Path.encode, Path.encode)), pair(string,
    10.5                  pair(string, pair(string, pair(string, pair(Path.encode,
    10.6                  pair(list(pair(Options.encode, list(pair(string, properties)))),
    10.7 -                pair(list(pair(string, string)), pair(list(pair(string, string)),
    10.8 +                pair(list(pair(string, string)), pair(list(string),
    10.9                  list(pair(string, string))))))))))))))))(
   10.10                (Symbol.codes, (command_timings, (do_output, (verbose,
   10.11                  (store.browser_info, (info.document_files, (File.standard_path(graph_file),