clarified error for bad session-qualified imports;
authorwenzelm
Fri Oct 06 21:14:00 2017 +0200 (18 months ago)
changeset 66771925d10a7a610
parent 66770 122df1fde073
child 66772 a66f11a0b5b1
clarified error for bad session-qualified imports;
src/Pure/PIDE/resources.ML
src/Pure/PIDE/resources.scala
src/Pure/Thy/thy_header.ML
     1.1 --- a/src/Pure/PIDE/resources.ML	Fri Oct 06 17:13:57 2017 +0200
     1.2 +++ b/src/Pure/PIDE/resources.ML	Fri Oct 06 21:14:00 2017 +0200
     1.3 @@ -123,7 +123,10 @@
     1.4        let val node_name =
     1.5          (case known_theory theory of
     1.6            SOME node_name => node_name
     1.7 -        | NONE => File.full_path dir (thy_path (Path.expand (Path.explode s))))
     1.8 +        | NONE =>
     1.9 +            if Thy_Header.is_base_name s andalso Long_Name.is_qualified s
    1.10 +            then Path.explode s
    1.11 +            else File.full_path dir (thy_path (Path.expand (Path.explode s))))
    1.12        in {master_dir = Path.dir node_name, theory_name = theory} end);
    1.13  
    1.14  fun check_file dir file = File.check_file (File.full_path dir file);
     2.1 --- a/src/Pure/PIDE/resources.scala	Fri Oct 06 17:13:57 2017 +0200
     2.2 +++ b/src/Pure/PIDE/resources.scala	Fri Oct 06 21:14:00 2017 +0200
     2.3 @@ -105,10 +105,14 @@
     2.4          session_base.known_theory(theory) match {
     2.5            case Some(node_name) => node_name
     2.6            case None =>
     2.7 -            val path = Path.explode(s)
     2.8 -            val node = append(dir, thy_path(path))
     2.9 -            val master_dir = append(dir, path.dir)
    2.10 -            Document.Node.Name(node, master_dir, theory)
    2.11 +            if (Thy_Header.is_base_name(s) && Long_Name.is_qualified(s))
    2.12 +              Document.Node.Name.loaded_theory(theory)
    2.13 +            else {
    2.14 +              val path = Path.explode(s)
    2.15 +              val node = append(dir, thy_path(path))
    2.16 +              val master_dir = append(dir, path.dir)
    2.17 +              Document.Node.Name(node, master_dir, theory)
    2.18 +            }
    2.19          }
    2.20      }
    2.21  
    2.22 @@ -136,9 +140,14 @@
    2.23  
    2.24    def with_thy_reader[A](name: Document.Node.Name, f: Reader[Char] => A): A =
    2.25    {
    2.26 -    val path = File.check_file(name.path)
    2.27 -    val reader = Scan.byte_reader(path.file)
    2.28 -    try { f(reader) } finally { reader.close }
    2.29 +    val path = name.path
    2.30 +    if (path.is_file) {
    2.31 +      val reader = Scan.byte_reader(path.file)
    2.32 +      try { f(reader) } finally { reader.close }
    2.33 +    }
    2.34 +    else if (name.node == name.theory)
    2.35 +      error("Cannot load theory " + quote(name.theory))
    2.36 +    else error ("Cannot load theory file " + path)
    2.37    }
    2.38  
    2.39    def check_thy_reader(node_name: Document.Node.Name, reader: Reader[Char],
     3.1 --- a/src/Pure/Thy/thy_header.ML	Fri Oct 06 17:13:57 2017 +0200
     3.2 +++ b/src/Pure/Thy/thy_header.ML	Fri Oct 06 21:14:00 2017 +0200
     3.3 @@ -20,6 +20,7 @@
     3.4    val ml_bootstrapN: string
     3.5    val ml_roots: string list
     3.6    val bootstrap_thys: string list
     3.7 +  val is_base_name: string -> bool
     3.8    val import_name: string -> string
     3.9    val args: header parser
    3.10    val read: Position.T -> string -> header
    3.11 @@ -114,6 +115,9 @@
    3.12  val ml_roots = ["ML_Root0", "ML_Root"];
    3.13  val bootstrap_thys = ["Bootstrap_Pure", "Bootstrap_ML_Bootstrap"];
    3.14  
    3.15 +fun is_base_name s =
    3.16 +  s <> "" andalso not (exists_string (member (op =) ["/", "\\", ":"]) s)
    3.17 +
    3.18  val import_name = Path.base_name o Path.explode;
    3.19  
    3.20