clarified boundary cases of Document.Node.Name;
authorwenzelm
Tue Nov 19 12:57:56 2013 +0100 (2013-11-19)
changeset 54515570ba266f5b5
parent 54514 6428dfab6520
child 54516 2a7f9e79cb28
clarified boundary cases of Document.Node.Name;
src/Pure/PIDE/document.scala
src/Pure/PIDE/protocol.scala
src/Pure/Thy/thy_info.scala
src/Pure/Thy/thy_load.scala
src/Pure/Thy/thy_syntax.scala
src/Tools/jEdit/src/isabelle_sidekick.scala
src/Tools/jEdit/src/jedit_thy_load.scala
src/Tools/jEdit/src/rendering.scala
     1.1 --- a/src/Pure/PIDE/document.scala	Mon Nov 18 23:46:59 2013 +0100
     1.2 +++ b/src/Pure/PIDE/document.scala	Tue Nov 19 12:57:56 2013 +0100
     1.3 @@ -68,7 +68,7 @@
     1.4  
     1.5      object Name
     1.6      {
     1.7 -      val empty = Name("", "", "")
     1.8 +      val empty = Name("")
     1.9  
    1.10        object Ordering extends scala.math.Ordering[Name]
    1.11        {
    1.12 @@ -76,7 +76,7 @@
    1.13        }
    1.14      }
    1.15  
    1.16 -    sealed case class Name(node: String, dir: String, theory: String)
    1.17 +    sealed case class Name(node: String, master_dir: String = "", theory: String = "")
    1.18      {
    1.19        override def hashCode: Int = node.hashCode
    1.20        override def equals(that: Any): Boolean =
     2.1 --- a/src/Pure/PIDE/protocol.scala	Mon Nov 18 23:46:59 2013 +0100
     2.2 +++ b/src/Pure/PIDE/protocol.scala	Tue Nov 19 12:57:56 2013 +0100
     2.3 @@ -339,7 +339,7 @@
     2.4            { case Document.Node.Clear() => (Nil, Nil) },  // FIXME unused !?
     2.5            { case Document.Node.Edits(a) => (Nil, list(pair(option(id), option(id)))(a)) },
     2.6            { case Document.Node.Deps(header) =>
     2.7 -              val dir = Isabelle_System.posix_path(name.dir)
     2.8 +              val master_dir = Isabelle_System.posix_path(name.master_dir)
     2.9                val imports = header.imports.map(_.node)
    2.10                val keywords = header.keywords.map({ case (a, b, _) => (a, b) })
    2.11                (Nil,
    2.12 @@ -347,7 +347,7 @@
    2.13                    pair(list(pair(Encode.string,
    2.14                      option(pair(pair(Encode.string, list(Encode.string)), list(Encode.string))))),
    2.15                    list(Encode.string)))))(
    2.16 -                (dir, (name.theory, (imports, (keywords, header.errors)))))) },
    2.17 +                (master_dir, (name.theory, (imports, (keywords, header.errors)))))) },
    2.18            { case Document.Node.Perspective(a, b, c) =>
    2.19                (bool_atom(a) :: b.commands.map(cmd => long_atom(cmd.id)),
    2.20                  list(pair(id, pair(Encode.string, list(Encode.string))))(c.dest)) }))
     3.1 --- a/src/Pure/Thy/thy_info.scala	Mon Nov 18 23:46:59 2013 +0100
     3.2 +++ b/src/Pure/Thy/thy_info.scala	Tue Nov 19 12:57:56 2013 +0100
     3.3 @@ -68,7 +68,7 @@
     3.4        val dep_files =
     3.5          rev_deps.par.map(dep =>
     3.6            Exn.capture {
     3.7 -            dep.load_files(syntax).map(a => Path.explode(dep.name.dir) + Path.explode(a))
     3.8 +            dep.load_files(syntax).map(a => Path.explode(dep.name.master_dir) + Path.explode(a))
     3.9            }).toList
    3.10        ((Nil: List[Path]) /: dep_files) {
    3.11          case (acc_files, files) => Exn.release(files) ::: acc_files
     4.1 --- a/src/Pure/Thy/thy_load.scala	Mon Nov 18 23:46:59 2013 +0100
     4.2 +++ b/src/Pure/Thy/thy_load.scala	Tue Nov 19 12:57:56 2013 +0100
     4.3 @@ -32,9 +32,9 @@
     4.4    {
     4.5      val path = raw_path.expand
     4.6      val node = path.implode
     4.7 -    val dir = path.dir.implode
     4.8      val theory = Thy_Header.thy_name(node).getOrElse("")
     4.9 -    Document.Node.Name(node, dir, theory)
    4.10 +    val master_dir = if (theory == "") "" else path.dir.implode
    4.11 +    Document.Node.Name(node, master_dir, theory)
    4.12    }
    4.13  
    4.14  
    4.15 @@ -68,12 +68,12 @@
    4.16    def import_name(master: Document.Node.Name, s: String): Document.Node.Name =
    4.17    {
    4.18      val theory = Thy_Header.base_name(s)
    4.19 -    if (loaded_theories(theory)) Document.Node.Name(theory, "", theory)
    4.20 +    if (loaded_theories(theory)) Document.Node.Name(theory + ".thy", "", theory)
    4.21      else {
    4.22        val path = Path.explode(s)
    4.23 -      val node = append(master.dir, Thy_Load.thy_path(path))
    4.24 -      val dir = append(master.dir, path.dir)
    4.25 -      Document.Node.Name(node, dir, theory)
    4.26 +      val node = append(master.master_dir, Thy_Load.thy_path(path))
    4.27 +      val master_dir = append(master.master_dir, path.dir)
    4.28 +      Document.Node.Name(node, master_dir, theory)
    4.29      }
    4.30    }
    4.31  
     5.1 --- a/src/Pure/Thy/thy_syntax.scala	Mon Nov 18 23:46:59 2013 +0100
     5.2 +++ b/src/Pure/Thy/thy_syntax.scala	Tue Nov 19 12:57:56 2013 +0100
     5.3 @@ -33,7 +33,7 @@
     5.4  
     5.5        def buffer(): mutable.ListBuffer[Entry] = new mutable.ListBuffer[Entry]
     5.6        var stack: List[(Int, String, mutable.ListBuffer[Entry])] =
     5.7 -        List((0, node_name.theory, buffer()))
     5.8 +        List((0, node_name.toString, buffer()))
     5.9  
    5.10        @tailrec def close(level: Int => Boolean)
    5.11        {
    5.12 @@ -260,7 +260,7 @@
    5.13      val files = span_files(syntax, span)
    5.14      files.map(file => {
    5.15        // FIXME proper thy_load append
    5.16 -      val file_name = Document.Node.Name(name.dir + file, name.dir, "")
    5.17 +      val file_name = Document.Node.Name(name.master_dir + file)
    5.18        (file_name, all_blobs.get(file_name).map(_.sha1_digest))
    5.19      })
    5.20    }
     6.1 --- a/src/Tools/jEdit/src/isabelle_sidekick.scala	Mon Nov 18 23:46:59 2013 +0100
     6.2 +++ b/src/Tools/jEdit/src/isabelle_sidekick.scala	Tue Nov 19 12:57:56 2013 +0100
     6.3 @@ -137,11 +137,11 @@
     6.4  
     6.5  
     6.6  class Isabelle_Sidekick_Options extends
     6.7 -  Isabelle_Sidekick_Structure("isabelle-options", b => Some(PIDE.thy_load.dummy_node_name(b)))
     6.8 +  Isabelle_Sidekick_Structure("isabelle-options", _ => Some(Document.Node.Name("options")))
     6.9  
    6.10  
    6.11  class Isabelle_Sidekick_Root extends
    6.12 -  Isabelle_Sidekick_Structure("isabelle-root", b => Some(PIDE.thy_load.dummy_node_name(b)))
    6.13 +  Isabelle_Sidekick_Structure("isabelle-root", _ => Some(Document.Node.Name("ROOT")))
    6.14  
    6.15  
    6.16  class Isabelle_Sidekick_Markup extends Isabelle_Sidekick("isabelle-markup")
     7.1 --- a/src/Tools/jEdit/src/jedit_thy_load.scala	Mon Nov 18 23:46:59 2013 +0100
     7.2 +++ b/src/Tools/jEdit/src/jedit_thy_load.scala	Tue Nov 19 12:57:56 2013 +0100
     7.3 @@ -22,13 +22,12 @@
     7.4  {
     7.5    /* document node names */
     7.6  
     7.7 -  def dummy_node_name(buffer: Buffer): Document.Node.Name =
     7.8 -    Document.Node.Name(JEdit_Lib.buffer_name(buffer), buffer.getDirectory, buffer.getName)
     7.9 -
    7.10    def node_name(buffer: Buffer): Document.Node.Name =
    7.11    {
    7.12 -    val name = JEdit_Lib.buffer_name(buffer)
    7.13 -    Document.Node.Name(name, buffer.getDirectory, Thy_Header.thy_name(name).getOrElse(""))
    7.14 +    val node = JEdit_Lib.buffer_name(buffer)
    7.15 +    val theory = Thy_Header.thy_name(node).getOrElse("")
    7.16 +    val master_dir = if (theory == "") "" else buffer.getDirectory
    7.17 +    Document.Node.Name(node, master_dir, theory)
    7.18    }
    7.19  
    7.20    def theory_node_name(buffer: Buffer): Option[Document.Node.Name] =
     8.1 --- a/src/Tools/jEdit/src/rendering.scala	Mon Nov 18 23:46:59 2013 +0100
     8.2 +++ b/src/Tools/jEdit/src/rendering.scala	Tue Nov 19 12:57:56 2013 +0100
     8.3 @@ -226,7 +226,7 @@
     8.4          {
     8.5            case (links, Text.Info(info_range, XML.Elem(Markup.Path(name), _)))
     8.6            if Path.is_ok(name) =>
     8.7 -            val jedit_file = PIDE.thy_load.append(snapshot.node_name.dir, Path.explode(name))
     8.8 +            val jedit_file = PIDE.thy_load.append(snapshot.node_name.master_dir, Path.explode(name))
     8.9              val link = PIDE.editor.hyperlink_file(jedit_file)
    8.10              Some(Text.Info(snapshot.convert(info_range), link) :: links)
    8.11  
    8.12 @@ -369,7 +369,7 @@
    8.13              Some(add(prev, r, (true, XML.Text(txt1 + txt2))))
    8.14            case (prev, Text.Info(r, XML.Elem(Markup.Path(name), _)))
    8.15            if Path.is_ok(name) =>
    8.16 -            val jedit_file = PIDE.thy_load.append(snapshot.node_name.dir, Path.explode(name))
    8.17 +            val jedit_file = PIDE.thy_load.append(snapshot.node_name.master_dir, Path.explode(name))
    8.18              Some(add(prev, r, (true, XML.Text("file " + quote(jedit_file)))))
    8.19            case (prev, Text.Info(r, XML.Elem(Markup(name, _), body)))
    8.20            if name == Markup.SORTING || name == Markup.TYPING =>