tuned signature -- avoid intrusion of module Path in generic PIDE concepts;
authorwenzelm
Sun Nov 25 20:31:49 2012 +0100 (2012-11-25 ago)
changeset 50204daeb1674fb91
parent 50203 00d8ad713e32
child 50205 788c8263e634
tuned signature -- avoid intrusion of module Path in generic PIDE concepts;
src/Pure/PIDE/document.scala
src/Pure/System/build.scala
src/Pure/Thy/thy_load.scala
     1.1 --- a/src/Pure/PIDE/document.scala	Sun Nov 25 20:17:04 2012 +0100
     1.2 +++ b/src/Pure/PIDE/document.scala	Sun Nov 25 20:31:49 2012 +0100
     1.3 @@ -51,14 +51,6 @@
     1.4      object Name
     1.5      {
     1.6        val empty = Name("", "", "")
     1.7 -      def apply(raw_path: Path): Name =
     1.8 -      {
     1.9 -        val path = raw_path.expand
    1.10 -        val node = path.implode
    1.11 -        val dir = path.dir.implode
    1.12 -        val theory = Thy_Header.thy_name(node) getOrElse error("Bad theory file name: " + path)
    1.13 -        Name(node, dir, theory)
    1.14 -      }
    1.15  
    1.16        object Ordering extends scala.math.Ordering[Name]
    1.17        {
     2.1 --- a/src/Pure/System/build.scala	Sun Nov 25 20:17:04 2012 +0100
     2.2 +++ b/src/Pure/System/build.scala	Sun Nov 25 20:31:49 2012 +0100
     2.3 @@ -358,7 +358,7 @@
     2.4            val thy_deps =
     2.5              thy_info.dependencies(inlined_files,
     2.6                info.theories.map(_._2).flatten.
     2.7 -                map(thy => Document.Node.Name(info.dir + Thy_Load.thy_path(thy))))
     2.8 +                map(thy => Thy_Load.external_node(info.dir + Thy_Load.thy_path(thy))))
     2.9  
    2.10            val loaded_theories = thy_deps.loaded_theories
    2.11            val syntax = thy_deps.make_syntax
     3.1 --- a/src/Pure/Thy/thy_load.scala	Sun Nov 25 20:17:04 2012 +0100
     3.2 +++ b/src/Pure/Thy/thy_load.scala	Sun Nov 25 20:31:49 2012 +0100
     3.3 @@ -14,11 +14,25 @@
     3.4  
     3.5  object Thy_Load
     3.6  {
     3.7 +  /* paths */
     3.8 +
     3.9    def thy_path(path: Path): Path = path.ext("thy")
    3.10  
    3.11    def is_ok(str: String): Boolean =
    3.12      try { thy_path(Path.explode(str)); true }
    3.13      catch { case ERROR(_) => false }
    3.14 +
    3.15 +
    3.16 +  /* node names */
    3.17 +
    3.18 +  def external_node(raw_path: Path): Document.Node.Name =
    3.19 +  {
    3.20 +    val path = raw_path.expand
    3.21 +    val node = path.implode
    3.22 +    val dir = path.dir.implode
    3.23 +    val theory = Thy_Header.thy_name(node) getOrElse error("Bad theory file name: " + path)
    3.24 +    Document.Node.Name(node, dir, theory)
    3.25 +  }
    3.26  }
    3.27  
    3.28