tuned signature;
authorwenzelm
Sat Apr 08 12:31:29 2017 +0200 (2017-04-08)
changeset 65439862bfd2b4fd4
parent 65435 378175f44328
child 65440 fd147f56d9be
tuned signature;
src/Pure/PIDE/document.scala
src/Pure/PIDE/protocol.scala
src/Pure/PIDE/resources.scala
src/Pure/Thy/thy_info.scala
     1.1 --- a/src/Pure/PIDE/document.scala	Fri Apr 07 21:17:18 2017 +0200
     1.2 +++ b/src/Pure/PIDE/document.scala	Sat Apr 08 12:31:29 2017 +0200
     1.3 @@ -117,6 +117,8 @@
     1.4        def loaded_theory: Name = Name(theory, "", theory)
     1.5        def is_theory: Boolean = theory.nonEmpty
     1.6  
     1.7 +      def theory_base_name: String = Long_Name.base_name(theory)
     1.8 +
     1.9        override def toString: String = if (is_theory) theory else node
    1.10  
    1.11        def map(f: String => String): Name = copy(f(node), f(master_dir), theory)
     2.1 --- a/src/Pure/PIDE/protocol.scala	Fri Apr 07 21:17:18 2017 +0200
     2.2 +++ b/src/Pure/PIDE/protocol.scala	Sat Apr 08 12:31:29 2017 +0200
     2.3 @@ -359,7 +359,7 @@
     2.4            { case Document.Node.Edits(a) => (Nil, list(pair(option(id), option(id)))(a)) },
     2.5            { case Document.Node.Deps(header) =>
     2.6                val master_dir = File.standard_url(name.master_dir)
     2.7 -              val theory = Long_Name.base_name(name.theory)
     2.8 +              val theory = name.theory_base_name  // FIXME
     2.9                val imports = header.imports.map({ case (a, _) => a.node })
    2.10                val keywords =
    2.11                  header.keywords.map({ case (a, Keyword.Spec(b, c, d)) => (a, ((b, c), d)) })
     3.1 --- a/src/Pure/PIDE/resources.scala	Fri Apr 07 21:17:18 2017 +0200
     3.2 +++ b/src/Pure/PIDE/resources.scala	Sat Apr 08 12:31:29 2017 +0200
     3.3 @@ -101,7 +101,7 @@
     3.4        try {
     3.5          val header = Thy_Header.read(reader, start, strict).decode_symbols
     3.6  
     3.7 -        val base_name = Long_Name.base_name(node_name.theory)
     3.8 +        val base_name = node_name.theory_base_name
     3.9          val (name, pos) = header.name
    3.10          if (base_name != name)
    3.11            error("Bad theory name " + quote(name) +
     4.1 --- a/src/Pure/Thy/thy_info.scala	Fri Apr 07 21:17:18 2017 +0200
     4.2 +++ b/src/Pure/Thy/thy_info.scala	Sat Apr 08 12:31:29 2017 +0200
     4.3 @@ -85,7 +85,7 @@
     4.4          case (loaded, dep) =>
     4.5            val name = dep.name.loaded_theory
     4.6            loaded + (name.theory -> name) +
     4.7 -            (Long_Name.base_name(name.theory) -> name)  // legacy
     4.8 +            (name.theory_base_name -> name)  // legacy
     4.9        }
    4.10  
    4.11      def loaded_files: List[Path] =
    4.12 @@ -108,7 +108,7 @@
    4.13  
    4.14        def node(name: Document.Node.Name): Graph_Display.Node =
    4.15          if (parent_base.loaded_theory(name)) parent_session_node
    4.16 -        else Graph_Display.Node(Long_Name.base_name(name.theory), "theory." + name.theory)
    4.17 +        else Graph_Display.Node(name.theory_base_name, "theory." + name.theory)
    4.18  
    4.19        (Graph_Display.empty_graph /: deps) {
    4.20          case (g, dep) =>