tuned signature;
authorwenzelm
Mon Apr 03 12:41:06 2017 +0200 (2017-04-03)
changeset 65355403eabd73c9a
parent 65347 d27f9b4e027d
child 65356 b96cf915de75
tuned signature;
src/Pure/PIDE/document.scala
src/Pure/PIDE/resources.scala
src/Pure/Thy/sessions.scala
src/Pure/Thy/thy_info.scala
src/Pure/Thy/thy_syntax.scala
src/Tools/jEdit/src/theories_dockable.scala
src/Tools/jEdit/src/timing_dockable.scala
     1.1 --- a/src/Pure/PIDE/document.scala	Sat Apr 01 23:48:28 2017 +0200
     1.2 +++ b/src/Pure/PIDE/document.scala	Mon Apr 03 12:41:06 2017 +0200
     1.3 @@ -503,7 +503,7 @@
     1.4            case None =>
     1.5              List(
     1.6                Document.Node.Deps(
     1.7 -                if (session.resources.base.loaded_theories(node_name.theory))
     1.8 +                if (session.resources.base.loaded_theory(node_name))
     1.9                    node_header.error("Cannot update finished theory " + quote(node_name.theory))
    1.10                  else node_header),
    1.11                Document.Node.Edits(text_edits), perspective)
     2.1 --- a/src/Pure/PIDE/resources.scala	Sat Apr 01 23:48:28 2017 +0200
     2.2 +++ b/src/Pure/PIDE/resources.scala	Mon Apr 03 12:41:06 2017 +0200
     2.3 @@ -88,7 +88,7 @@
     2.4      (base.known_theories.get(thy1) orElse
     2.5       base.known_theories.get(thy2) orElse
     2.6       base.known_theories.get(Long_Name.base_name(thy1))) match {
     2.7 -      case Some(name) if base.loaded_theories(name.theory) => dummy_name(name.theory)
     2.8 +      case Some(name) if base.loaded_theory(name) => dummy_name(name.theory)
     2.9        case Some(name) => name
    2.10        case None =>
    2.11          val path = Path.explode(s)
    2.12 @@ -155,7 +155,7 @@
    2.13    def undefined_blobs(nodes: Document.Nodes): List[Document.Node.Name] =
    2.14      (for {
    2.15        (node_name, node) <- nodes.iterator
    2.16 -      if !base.loaded_theories(node_name.theory)
    2.17 +      if !base.loaded_theory(node_name)
    2.18        cmd <- node.load_commands.iterator
    2.19        name <- cmd.blobs_undefined.iterator
    2.20      } yield name).toList
     3.1 --- a/src/Pure/Thy/sessions.scala	Sat Apr 01 23:48:28 2017 +0200
     3.2 +++ b/src/Pure/Thy/sessions.scala	Mon Apr 03 12:41:06 2017 +0200
     3.3 @@ -47,6 +47,10 @@
     3.4      syntax: Outer_Syntax = Outer_Syntax.empty,
     3.5      sources: List[(Path, SHA1.Digest)] = Nil,
     3.6      session_graph: Graph_Display.Graph = Graph_Display.empty_graph)
     3.7 +  {
     3.8 +    def loaded_theory(name: Document.Node.Name): Boolean =
     3.9 +      loaded_theories.contains(name.theory)
    3.10 +  }
    3.11  
    3.12    sealed case class Deps(deps: Map[String, Base])
    3.13    {
     4.1 --- a/src/Pure/Thy/thy_info.scala	Sat Apr 01 23:48:28 2017 +0200
     4.2 +++ b/src/Pure/Thy/thy_info.scala	Mon Apr 03 12:41:06 2017 +0200
     4.3 @@ -118,7 +118,7 @@
     4.4          required_by(initiators) + Position.here(require_pos)
     4.5  
     4.6      val required1 = required + thy
     4.7 -    if (required.seen(name) || resources.base.loaded_theories(name.theory)) required1
     4.8 +    if (required.seen(name) || resources.base.loaded_theory(name)) required1
     4.9      else {
    4.10        try {
    4.11          if (initiators.contains(name)) error(cycle_msg(initiators))
     5.1 --- a/src/Pure/Thy/thy_syntax.scala	Sat Apr 01 23:48:28 2017 +0200
     5.2 +++ b/src/Pure/Thy/thy_syntax.scala	Mon Apr 03 12:41:06 2017 +0200
     5.3 @@ -300,7 +300,7 @@
     5.4        doc_blobs.get(name) orElse previous.nodes(name).get_blob
     5.5  
     5.6      def can_import(name: Document.Node.Name): Boolean =
     5.7 -      resources.base.loaded_theories(name.theory) || nodes0(name).has_header
     5.8 +      resources.base.loaded_theory(name) || nodes0(name).has_header
     5.9  
    5.10      val (doc_edits, version) =
    5.11        if (edits.isEmpty) (Nil, Document.Version.make(previous.nodes))
     6.1 --- a/src/Tools/jEdit/src/theories_dockable.scala	Sat Apr 01 23:48:28 2017 +0200
     6.2 +++ b/src/Tools/jEdit/src/theories_dockable.scala	Mon Apr 03 12:41:06 2017 +0200
     6.3 @@ -192,7 +192,7 @@
     6.4        }
     6.5      val nodes_status1 =
     6.6        (nodes_status /: iterator)({ case (status, (name, node)) =>
     6.7 -          if (!name.is_theory || PIDE.resources.base.loaded_theories(name.theory) || node.is_empty)
     6.8 +          if (!name.is_theory || PIDE.resources.base.loaded_theory(name) || node.is_empty)
     6.9              status
    6.10            else status + (name -> Protocol.node_status(snapshot.state, snapshot.version, node)) })
    6.11  
     7.1 --- a/src/Tools/jEdit/src/timing_dockable.scala	Sat Apr 01 23:48:28 2017 +0200
     7.2 +++ b/src/Tools/jEdit/src/timing_dockable.scala	Mon Apr 03 12:41:06 2017 +0200
     7.3 @@ -187,7 +187,7 @@
     7.4        }
     7.5      val nodes_timing1 =
     7.6        (nodes_timing /: iterator)({ case (timing1, (name, node)) =>
     7.7 -          if (PIDE.resources.base.loaded_theories(name.theory)) timing1
     7.8 +          if (PIDE.resources.base.loaded_theory(name)) timing1
     7.9            else {
    7.10              val node_timing =
    7.11                Protocol.node_timing(snapshot.state, snapshot.version, node, timing_threshold)