# HG changeset patch
# User wenzelm
# Date 1491816587 -7200
# Node ID 9e9750a7932c2b893334ba94b02a8e83e38effa5
# Parent  5febea96902fc350b3b096b0eb35b516a07988e8
clarified signature;

diff -r 5febea96902f -r 9e9750a7932c src/Pure/PIDE/resources.scala
--- a/src/Pure/PIDE/resources.scala	Sun Apr 09 21:06:19 2017 +0200
+++ b/src/Pure/PIDE/resources.scala	Mon Apr 10 11:29:47 2017 +0200
@@ -72,7 +72,7 @@
 
   def import_name(qualifier: String, dir: String, s: String): Document.Node.Name =
   {
-    val theory0 = Thy_Header.base_name(s)
+    val theory0 = Thy_Header.import_name(s)
     val theory =
       if (Long_Name.is_qualified(theory0) || session_base.global_theories.contains(theory0)
         || true /* FIXME */) theory0
diff -r 5febea96902f -r 9e9750a7932c src/Pure/Thy/thy_header.ML
--- a/src/Pure/Thy/thy_header.ML	Sun Apr 09 21:06:19 2017 +0200
+++ b/src/Pure/Thy/thy_header.ML	Mon Apr 10 11:29:47 2017 +0200
@@ -20,6 +20,7 @@
   val ml_bootstrapN: string
   val ml_roots: string list
   val bootstrap_thys: string list
+  val import_name: string -> string
   val args: header parser
   val read: Position.T -> string -> header
   val read_tokens: Token.T list -> header
@@ -113,6 +114,7 @@
 val ml_roots = ["ML_Root0", "ML_Root"];
 val bootstrap_thys = ["Bootstrap_Pure", "Bootstrap_ML_Bootstrap"];
 
+val import_name = Path.implode o Path.base o Path.explode;
 
 
 (* header args *)
diff -r 5febea96902f -r 9e9750a7932c src/Pure/Thy/thy_header.scala
--- a/src/Pure/Thy/thy_header.scala	Sun Apr 09 21:06:19 2017 +0200
+++ b/src/Pure/Thy/thy_header.scala	Mon Apr 10 11:29:47 2017 +0200
@@ -77,21 +77,19 @@
   val ml_roots = List("ROOT0.ML" -> "ML_Root0", "ROOT.ML" -> ML_ROOT)
   val bootstrap_thys = List(PURE, ML_BOOTSTRAP).map(a => a -> ("Bootstrap_" + a))
 
-  private val Base_Name = new Regex(""".*?([^/\\:]+)""")
-  private val Thy_Name = new Regex(""".*?([^/\\:]+)\.thy""")
+  private val Thy_File_Name = new Regex(""".*?([^/\\:]+)\.thy""")
+  private val Import_Name = new Regex(""".*?([^/\\:]+)""")
 
-  def base_name(s: String): String =
-    s match { case Base_Name(name) => name case _ => error("Malformed import: " + quote(s)) }
+  def import_name(s: String): String =
+    s match { case Import_Name(name) => name case _ => error("Malformed import: " + quote(s)) }
 
-  def thy_name(s: String): Option[String] =
-    s match { case Thy_Name(name) => Some(name) case _ => None }
-
-  def thy_name_bootstrap(s: String): Option[String] =
+  def theory_name(s: String): String =
     s match {
-      case Thy_Name(name) =>
-        Some(bootstrap_thys.collectFirst({ case (a, b) if a == name => b }).getOrElse(name))
-      case Base_Name(name) => ml_roots.collectFirst({ case (a, b) if a == name => b })
-      case _ => None
+      case Thy_File_Name(name) =>
+        bootstrap_thys.collectFirst({ case (a, b) if a == name => b }).getOrElse(name)
+      case Import_Name(name) =>
+        ml_roots.collectFirst({ case (a, b) if a == name => b }).getOrElse("")
+      case _ => ""
     }
 
   def is_ml_root(theory: String): Boolean =
diff -r 5febea96902f -r 9e9750a7932c src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Sun Apr 09 21:06:19 2017 +0200
+++ b/src/Pure/Thy/thy_info.ML	Mon Apr 10 11:29:47 2017 +0200
@@ -57,8 +57,6 @@
 fun master_dir (d: deps option) =
   the_default Path.current (Option.map (Path.dir o #1 o #master) d);
 
-fun base_name s = Path.implode (Path.base (Path.explode s));
-
 local
   val global_thys =
     Synchronized.var "Thy_Info.thys"
@@ -316,7 +314,7 @@
                 ("The error(s) above occurred for theory " ^ quote theory_name ^
                   Position.here require_pos ^ required_by "\n" initiators);
 
-          val parents = map (base_name o #1) imports;
+          val parents = map (Thy_Header.import_name o #1) imports;
           val (parents_current, tasks') =
             require_thys document symbols last_timing (theory_name :: initiators)
               (Resources.theory_qualifier theory_name)
diff -r 5febea96902f -r 9e9750a7932c src/Tools/VSCode/src/vscode_resources.scala
--- a/src/Tools/VSCode/src/vscode_resources.scala	Sun Apr 09 21:06:19 2017 +0200
+++ b/src/Tools/VSCode/src/vscode_resources.scala	Mon Apr 10 11:29:47 2017 +0200
@@ -63,7 +63,7 @@
   def node_name(file: JFile): Document.Node.Name =
   {
     val node = file.getPath
-    val theory = Thy_Header.thy_name_bootstrap(node).getOrElse("")
+    val theory = Thy_Header.theory_name(node)
     val master_dir = if (theory == "") "" else file.getParent
     Document.Node.Name(node, master_dir, theory)
   }
diff -r 5febea96902f -r 9e9750a7932c src/Tools/jEdit/src/jedit_resources.scala
--- a/src/Tools/jEdit/src/jedit_resources.scala	Sun Apr 09 21:06:19 2017 +0200
+++ b/src/Tools/jEdit/src/jedit_resources.scala	Mon Apr 10 11:29:47 2017 +0200
@@ -28,7 +28,7 @@
   def node_name(buffer: Buffer): Document.Node.Name =
   {
     val node = JEdit_Lib.buffer_name(buffer)
-    val theory = Thy_Header.thy_name_bootstrap(node).getOrElse("")
+    val theory = Thy_Header.theory_name(node)
     val master_dir = if (theory == "") "" else buffer.getDirectory
     Document.Node.Name(node, master_dir, theory)
   }
@@ -37,7 +37,7 @@
   {
     val vfs = VFSManager.getVFSForPath(path)
     val node = if (vfs.isInstanceOf[FileVFS]) MiscUtilities.resolveSymlinks(path) else path
-    val theory = Thy_Header.thy_name_bootstrap(node).getOrElse("")
+    val theory = Thy_Header.theory_name(node)
     val master_dir = if (theory == "") "" else vfs.getParentOfPath(path)
     Document.Node.Name(node, master_dir, theory)
   }