tuned signature;
authorwenzelm
Mon Apr 03 17:00:36 2017 +0200 (2017-04-03)
changeset 65361ecefb68dc21d
parent 65360 3ff88fece1f6
child 65362 908a27a4b9c9
tuned signature;
src/Pure/PIDE/document.scala
src/Pure/PIDE/resources.scala
src/Pure/PIDE/session.scala
src/Pure/Thy/thy_info.scala
src/Pure/Thy/thy_syntax.scala
src/Tools/VSCode/src/server.scala
src/Tools/VSCode/src/vscode_resources.scala
src/Tools/jEdit/src/isabelle.scala
src/Tools/jEdit/src/jedit_resources.scala
src/Tools/jEdit/src/theories_dockable.scala
src/Tools/jEdit/src/timing_dockable.scala
     1.1 --- a/src/Pure/PIDE/document.scala	Mon Apr 03 16:50:44 2017 +0200
     1.2 +++ b/src/Pure/PIDE/document.scala	Mon Apr 03 17:00:36 2017 +0200
     1.3 @@ -504,7 +504,7 @@
     1.4            case None =>
     1.5              List(
     1.6                Node.Deps(
     1.7 -                if (session.resources.base.loaded_theory(node_name))
     1.8 +                if (session.resources.session_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                Node.Edits(text_edits), perspective)
     2.1 --- a/src/Pure/PIDE/resources.scala	Mon Apr 03 16:50:44 2017 +0200
     2.2 +++ b/src/Pure/PIDE/resources.scala	Mon Apr 03 17:00:36 2017 +0200
     2.3 @@ -15,7 +15,7 @@
     2.4  
     2.5  class Resources(
     2.6    val session_name: String,
     2.7 -  val base: Sessions.Base,
     2.8 +  val session_base: Sessions.Base,
     2.9    val log: Logger = No_Logger)
    2.10  {
    2.11    val thy_info = new Thy_Info(this)
    2.12 @@ -81,10 +81,10 @@
    2.13    {
    2.14      val thy1 = Thy_Header.base_name(s)
    2.15      val thy2 = if (Long_Name.is_qualified(thy1)) thy1 else Long_Name.qualify(session_name, thy1)
    2.16 -    (base.known_theories.get(thy1) orElse
    2.17 -     base.known_theories.get(thy2) orElse
    2.18 -     base.known_theories.get(Long_Name.base_name(thy1))) match {
    2.19 -      case Some(name) if base.loaded_theory(name) => Document.Node.Name.theory(name.theory)
    2.20 +    (session_base.known_theories.get(thy1) orElse
    2.21 +     session_base.known_theories.get(thy2) orElse
    2.22 +     session_base.known_theories.get(Long_Name.base_name(thy1))) match {
    2.23 +      case Some(name) if session_base.loaded_theory(name) => Document.Node.Name.theory(name.theory)
    2.24        case Some(name) => name
    2.25        case None =>
    2.26          val path = Path.explode(s)
    2.27 @@ -150,7 +150,7 @@
    2.28    def undefined_blobs(nodes: Document.Nodes): List[Document.Node.Name] =
    2.29      (for {
    2.30        (node_name, node) <- nodes.iterator
    2.31 -      if !base.loaded_theory(node_name)
    2.32 +      if !session_base.loaded_theory(node_name)
    2.33        cmd <- node.load_commands.iterator
    2.34        name <- cmd.blobs_undefined.iterator
    2.35      } yield name).toList
     3.1 --- a/src/Pure/PIDE/session.scala	Mon Apr 03 16:50:44 2017 +0200
     3.2 +++ b/src/Pure/PIDE/session.scala	Mon Apr 03 17:00:36 2017 +0200
     3.3 @@ -191,7 +191,7 @@
     3.4  
     3.5    def recent_syntax(name: Document.Node.Name): Outer_Syntax =
     3.6      global_state.value.recent_finished.version.get_finished.nodes(name).syntax getOrElse
     3.7 -    resources.base.syntax
     3.8 +    resources.session_base.syntax
     3.9  
    3.10  
    3.11    /* pipelined change parsing */
     4.1 --- a/src/Pure/Thy/thy_info.scala	Mon Apr 03 16:50:44 2017 +0200
     4.2 +++ b/src/Pure/Thy/thy_info.scala	Mon Apr 03 17:00:36 2017 +0200
     4.3 @@ -71,7 +71,7 @@
     4.4        val import_errors =
     4.5          (for {
     4.6            (theory, names) <- seen_names.iterator_list
     4.7 -          if !resources.base.loaded_theories(theory)
     4.8 +          if !resources.session_base.loaded_theories(theory)
     4.9            if names.length > 1
    4.10          } yield
    4.11            "Incoherent imports for theory " + quote(theory) + ":\n" +
    4.12 @@ -83,10 +83,12 @@
    4.13      }
    4.14  
    4.15      lazy val syntax: Outer_Syntax =
    4.16 -      resources.base.syntax.add_keywords(keywords).add_abbrevs(abbrevs)
    4.17 +      resources.session_base.syntax.add_keywords(keywords).add_abbrevs(abbrevs)
    4.18  
    4.19      def loaded_theories: Set[String] =
    4.20 -      (resources.base.loaded_theories /: rev_deps) { case (loaded, dep) => loaded + dep.name.theory }
    4.21 +      (resources.session_base.loaded_theories /: rev_deps) {
    4.22 +        case (loaded, dep) => loaded + dep.name.theory
    4.23 +      }
    4.24  
    4.25      def loaded_files: List[Path] =
    4.26      {
    4.27 @@ -118,7 +120,7 @@
    4.28          required_by(initiators) + Position.here(require_pos)
    4.29  
    4.30      val required1 = required + thy
    4.31 -    if (required.seen(name) || resources.base.loaded_theory(name)) required1
    4.32 +    if (required.seen(name) || resources.session_base.loaded_theory(name)) required1
    4.33      else {
    4.34        try {
    4.35          if (initiators.contains(name)) error(cycle_msg(initiators))
     5.1 --- a/src/Pure/Thy/thy_syntax.scala	Mon Apr 03 16:50:44 2017 +0200
     5.2 +++ b/src/Pure/Thy/thy_syntax.scala	Mon Apr 03 17:00:36 2017 +0200
     5.3 @@ -101,7 +101,7 @@
     5.4          else {
     5.5            val header = node.header
     5.6            val imports_syntax = header.imports.flatMap(a => nodes(a._1).syntax)
     5.7 -          Some((resources.base.syntax /: imports_syntax)(_ ++ _)
     5.8 +          Some((resources.session_base.syntax /: imports_syntax)(_ ++ _)
     5.9              .add_keywords(header.keywords).add_abbrevs(header.abbrevs))
    5.10          }
    5.11        nodes += (name -> node.update_syntax(syntax))
    5.12 @@ -300,7 +300,7 @@
    5.13        doc_blobs.get(name) orElse previous.nodes(name).get_blob
    5.14  
    5.15      def can_import(name: Document.Node.Name): Boolean =
    5.16 -      resources.base.loaded_theory(name) || nodes0(name).has_header
    5.17 +      resources.session_base.loaded_theory(name) || nodes0(name).has_header
    5.18  
    5.19      val (doc_edits, version) =
    5.20        if (edits.isEmpty) (Nil, Document.Version.make(previous.nodes))
    5.21 @@ -324,7 +324,7 @@
    5.22          node_edits foreach {
    5.23            case (name, edits) =>
    5.24              val node = nodes(name)
    5.25 -            val syntax = node.syntax getOrElse resources.base.syntax
    5.26 +            val syntax = node.syntax getOrElse resources.session_base.syntax
    5.27              val commands = node.commands
    5.28  
    5.29              val node1 =
     6.1 --- a/src/Tools/VSCode/src/server.scala	Mon Apr 03 16:50:44 2017 +0200
     6.2 +++ b/src/Tools/VSCode/src/server.scala	Mon Apr 03 17:00:36 2017 +0200
     6.3 @@ -225,8 +225,8 @@
     6.4            }
     6.5          }
     6.6  
     6.7 -        val base = Sessions.session_base(options, session_name, session_dirs)
     6.8 -        val resources = new VSCode_Resources(options, base, log)
     6.9 +        val session_base = Sessions.session_base(options, session_name, session_dirs)
    6.10 +        val resources = new VSCode_Resources(options, session_base, log)
    6.11            {
    6.12              override def commit(change: Session.Change): Unit =
    6.13                if (change.deps_changed || undefined_blobs(change.version.nodes).nonEmpty)
     7.1 --- a/src/Tools/VSCode/src/vscode_resources.scala	Mon Apr 03 16:50:44 2017 +0200
     7.2 +++ b/src/Tools/VSCode/src/vscode_resources.scala	Mon Apr 03 17:00:36 2017 +0200
     7.3 @@ -40,9 +40,10 @@
     7.4  }
     7.5  
     7.6  class VSCode_Resources(
     7.7 -  val options: Options,
     7.8 -  base: Sessions.Base,
     7.9 -  log: Logger = No_Logger) extends Resources(session_name = "", base, log)
    7.10 +    val options: Options,
    7.11 +    session_base: Sessions.Base,
    7.12 +    log: Logger = No_Logger)
    7.13 +  extends Resources(session_name = "", session_base, log)
    7.14  {
    7.15    private val state = Synchronized(VSCode_Resources.State())
    7.16  
     8.1 --- a/src/Tools/jEdit/src/isabelle.scala	Mon Apr 03 16:50:44 2017 +0200
     8.2 +++ b/src/Tools/jEdit/src/isabelle.scala	Mon Apr 03 17:00:36 2017 +0200
     8.3 @@ -50,7 +50,7 @@
     8.4  
     8.5    def mode_syntax(mode: String): Option[Outer_Syntax] =
     8.6      mode match {
     8.7 -      case "isabelle" => Some(PIDE.resources.base.syntax)
     8.8 +      case "isabelle" => Some(PIDE.resources.session_base.syntax)
     8.9        case "isabelle-options" => Some(Options.options_syntax)
    8.10        case "isabelle-root" => Some(Sessions.root_syntax)
    8.11        case "isabelle-ml" => Some(ml_syntax)
     9.1 --- a/src/Tools/jEdit/src/jedit_resources.scala	Mon Apr 03 16:50:44 2017 +0200
     9.2 +++ b/src/Tools/jEdit/src/jedit_resources.scala	Mon Apr 03 17:00:36 2017 +0200
     9.3 @@ -21,7 +21,8 @@
     9.4  import org.gjt.sp.jedit.bufferio.BufferIORequest
     9.5  
     9.6  
     9.7 -class JEdit_Resources(base: Sessions.Base) extends Resources(session_name = "", base)
     9.8 +class JEdit_Resources(session_base: Sessions.Base)
     9.9 +  extends Resources(session_name = "", session_base)
    9.10  {
    9.11    /* document node name */
    9.12  
    10.1 --- a/src/Tools/jEdit/src/theories_dockable.scala	Mon Apr 03 16:50:44 2017 +0200
    10.2 +++ b/src/Tools/jEdit/src/theories_dockable.scala	Mon Apr 03 17:00:36 2017 +0200
    10.3 @@ -192,7 +192,7 @@
    10.4        }
    10.5      val nodes_status1 =
    10.6        (nodes_status /: iterator)({ case (status, (name, node)) =>
    10.7 -          if (!name.is_theory || PIDE.resources.base.loaded_theory(name) || node.is_empty)
    10.8 +          if (!name.is_theory || PIDE.resources.session_base.loaded_theory(name) || node.is_empty)
    10.9              status
   10.10            else status + (name -> Protocol.node_status(snapshot.state, snapshot.version, node)) })
   10.11  
    11.1 --- a/src/Tools/jEdit/src/timing_dockable.scala	Mon Apr 03 16:50:44 2017 +0200
    11.2 +++ b/src/Tools/jEdit/src/timing_dockable.scala	Mon Apr 03 17:00:36 2017 +0200
    11.3 @@ -187,7 +187,7 @@
    11.4        }
    11.5      val nodes_timing1 =
    11.6        (nodes_timing /: iterator)({ case (timing1, (name, node)) =>
    11.7 -          if (PIDE.resources.base.loaded_theory(name)) timing1
    11.8 +          if (PIDE.resources.session_base.loaded_theory(name)) timing1
    11.9            else {
   11.10              val node_timing =
   11.11                Protocol.node_timing(snapshot.state, snapshot.version, node, timing_threshold)