clarified signature;
authorwenzelm
Mon Apr 10 11:29:47 2017 +0200 (2017-04-10)
changeset 654529e9750a7932c
parent 65451 5febea96902f
child 65453 b2562bdda54e
clarified signature;
src/Pure/PIDE/resources.scala
src/Pure/Thy/thy_header.ML
src/Pure/Thy/thy_header.scala
src/Pure/Thy/thy_info.ML
src/Tools/VSCode/src/vscode_resources.scala
src/Tools/jEdit/src/jedit_resources.scala
     1.1 --- a/src/Pure/PIDE/resources.scala	Sun Apr 09 21:06:19 2017 +0200
     1.2 +++ b/src/Pure/PIDE/resources.scala	Mon Apr 10 11:29:47 2017 +0200
     1.3 @@ -72,7 +72,7 @@
     1.4  
     1.5    def import_name(qualifier: String, dir: String, s: String): Document.Node.Name =
     1.6    {
     1.7 -    val theory0 = Thy_Header.base_name(s)
     1.8 +    val theory0 = Thy_Header.import_name(s)
     1.9      val theory =
    1.10        if (Long_Name.is_qualified(theory0) || session_base.global_theories.contains(theory0)
    1.11          || true /* FIXME */) theory0
     2.1 --- a/src/Pure/Thy/thy_header.ML	Sun Apr 09 21:06:19 2017 +0200
     2.2 +++ b/src/Pure/Thy/thy_header.ML	Mon Apr 10 11:29:47 2017 +0200
     2.3 @@ -20,6 +20,7 @@
     2.4    val ml_bootstrapN: string
     2.5    val ml_roots: string list
     2.6    val bootstrap_thys: string list
     2.7 +  val import_name: string -> string
     2.8    val args: header parser
     2.9    val read: Position.T -> string -> header
    2.10    val read_tokens: Token.T list -> header
    2.11 @@ -113,6 +114,7 @@
    2.12  val ml_roots = ["ML_Root0", "ML_Root"];
    2.13  val bootstrap_thys = ["Bootstrap_Pure", "Bootstrap_ML_Bootstrap"];
    2.14  
    2.15 +val import_name = Path.implode o Path.base o Path.explode;
    2.16  
    2.17  
    2.18  (* header args *)
     3.1 --- a/src/Pure/Thy/thy_header.scala	Sun Apr 09 21:06:19 2017 +0200
     3.2 +++ b/src/Pure/Thy/thy_header.scala	Mon Apr 10 11:29:47 2017 +0200
     3.3 @@ -77,21 +77,19 @@
     3.4    val ml_roots = List("ROOT0.ML" -> "ML_Root0", "ROOT.ML" -> ML_ROOT)
     3.5    val bootstrap_thys = List(PURE, ML_BOOTSTRAP).map(a => a -> ("Bootstrap_" + a))
     3.6  
     3.7 -  private val Base_Name = new Regex(""".*?([^/\\:]+)""")
     3.8 -  private val Thy_Name = new Regex(""".*?([^/\\:]+)\.thy""")
     3.9 +  private val Thy_File_Name = new Regex(""".*?([^/\\:]+)\.thy""")
    3.10 +  private val Import_Name = new Regex(""".*?([^/\\:]+)""")
    3.11  
    3.12 -  def base_name(s: String): String =
    3.13 -    s match { case Base_Name(name) => name case _ => error("Malformed import: " + quote(s)) }
    3.14 +  def import_name(s: String): String =
    3.15 +    s match { case Import_Name(name) => name case _ => error("Malformed import: " + quote(s)) }
    3.16  
    3.17 -  def thy_name(s: String): Option[String] =
    3.18 -    s match { case Thy_Name(name) => Some(name) case _ => None }
    3.19 -
    3.20 -  def thy_name_bootstrap(s: String): Option[String] =
    3.21 +  def theory_name(s: String): String =
    3.22      s match {
    3.23 -      case Thy_Name(name) =>
    3.24 -        Some(bootstrap_thys.collectFirst({ case (a, b) if a == name => b }).getOrElse(name))
    3.25 -      case Base_Name(name) => ml_roots.collectFirst({ case (a, b) if a == name => b })
    3.26 -      case _ => None
    3.27 +      case Thy_File_Name(name) =>
    3.28 +        bootstrap_thys.collectFirst({ case (a, b) if a == name => b }).getOrElse(name)
    3.29 +      case Import_Name(name) =>
    3.30 +        ml_roots.collectFirst({ case (a, b) if a == name => b }).getOrElse("")
    3.31 +      case _ => ""
    3.32      }
    3.33  
    3.34    def is_ml_root(theory: String): Boolean =
     4.1 --- a/src/Pure/Thy/thy_info.ML	Sun Apr 09 21:06:19 2017 +0200
     4.2 +++ b/src/Pure/Thy/thy_info.ML	Mon Apr 10 11:29:47 2017 +0200
     4.3 @@ -57,8 +57,6 @@
     4.4  fun master_dir (d: deps option) =
     4.5    the_default Path.current (Option.map (Path.dir o #1 o #master) d);
     4.6  
     4.7 -fun base_name s = Path.implode (Path.base (Path.explode s));
     4.8 -
     4.9  local
    4.10    val global_thys =
    4.11      Synchronized.var "Thy_Info.thys"
    4.12 @@ -316,7 +314,7 @@
    4.13                  ("The error(s) above occurred for theory " ^ quote theory_name ^
    4.14                    Position.here require_pos ^ required_by "\n" initiators);
    4.15  
    4.16 -          val parents = map (base_name o #1) imports;
    4.17 +          val parents = map (Thy_Header.import_name o #1) imports;
    4.18            val (parents_current, tasks') =
    4.19              require_thys document symbols last_timing (theory_name :: initiators)
    4.20                (Resources.theory_qualifier theory_name)
     5.1 --- a/src/Tools/VSCode/src/vscode_resources.scala	Sun Apr 09 21:06:19 2017 +0200
     5.2 +++ b/src/Tools/VSCode/src/vscode_resources.scala	Mon Apr 10 11:29:47 2017 +0200
     5.3 @@ -63,7 +63,7 @@
     5.4    def node_name(file: JFile): Document.Node.Name =
     5.5    {
     5.6      val node = file.getPath
     5.7 -    val theory = Thy_Header.thy_name_bootstrap(node).getOrElse("")
     5.8 +    val theory = Thy_Header.theory_name(node)
     5.9      val master_dir = if (theory == "") "" else file.getParent
    5.10      Document.Node.Name(node, master_dir, theory)
    5.11    }
     6.1 --- a/src/Tools/jEdit/src/jedit_resources.scala	Sun Apr 09 21:06:19 2017 +0200
     6.2 +++ b/src/Tools/jEdit/src/jedit_resources.scala	Mon Apr 10 11:29:47 2017 +0200
     6.3 @@ -28,7 +28,7 @@
     6.4    def node_name(buffer: Buffer): Document.Node.Name =
     6.5    {
     6.6      val node = JEdit_Lib.buffer_name(buffer)
     6.7 -    val theory = Thy_Header.thy_name_bootstrap(node).getOrElse("")
     6.8 +    val theory = Thy_Header.theory_name(node)
     6.9      val master_dir = if (theory == "") "" else buffer.getDirectory
    6.10      Document.Node.Name(node, master_dir, theory)
    6.11    }
    6.12 @@ -37,7 +37,7 @@
    6.13    {
    6.14      val vfs = VFSManager.getVFSForPath(path)
    6.15      val node = if (vfs.isInstanceOf[FileVFS]) MiscUtilities.resolveSymlinks(path) else path
    6.16 -    val theory = Thy_Header.thy_name_bootstrap(node).getOrElse("")
    6.17 +    val theory = Thy_Header.theory_name(node)
    6.18      val master_dir = if (theory == "") "" else vfs.getParentOfPath(path)
    6.19      Document.Node.Name(node, master_dir, theory)
    6.20    }