tuned signature;
authorwenzelm
Mon Jan 09 20:26:59 2017 +0100 (2017-01-09)
changeset 64854f5aa712e6250
parent 64853 9178214b3588
child 64855 8fcc23e8e1d9
tuned signature;
src/Pure/PIDE/batch_session.scala
src/Pure/PIDE/document.scala
src/Pure/PIDE/resources.scala
src/Pure/PIDE/session.scala
src/Pure/Thy/thy_header.scala
src/Pure/Thy/thy_info.scala
src/Pure/Thy/thy_syntax.scala
src/Pure/Tools/build.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/plugin.scala
src/Tools/jEdit/src/theories_dockable.scala
src/Tools/jEdit/src/timing_dockable.scala
     1.1 --- a/src/Pure/PIDE/batch_session.scala	Mon Jan 09 19:34:16 2017 +0100
     1.2 +++ b/src/Pure/PIDE/batch_session.scala	Mon Jan 09 20:26:59 2017 +0100
     1.3 @@ -29,11 +29,7 @@
     1.4        new RuntimeException
     1.5  
     1.6      val deps = Build.dependencies(verbose = verbose, tree = session_tree)
     1.7 -    val resources =
     1.8 -    {
     1.9 -      val content = deps(parent_session)
    1.10 -      new Resources(content.loaded_theories, content.known_theories, content.syntax)
    1.11 -    }
    1.12 +    val resources = new Resources(deps(parent_session))
    1.13  
    1.14      val progress = new Console_Progress(verbose = verbose)
    1.15  
     2.1 --- a/src/Pure/PIDE/document.scala	Mon Jan 09 19:34:16 2017 +0100
     2.2 +++ b/src/Pure/PIDE/document.scala	Mon Jan 09 20:26:59 2017 +0100
     2.3 @@ -488,7 +488,7 @@
     2.4            case None =>
     2.5              List(
     2.6                Document.Node.Deps(
     2.7 -                if (session.resources.loaded_theories(node_name.theory))
     2.8 +                if (session.resources.base.loaded_theories(node_name.theory))
     2.9                    node_header.error("Cannot update finished theory " + quote(node_name.theory))
    2.10                  else node_header),
    2.11                Document.Node.Edits(text_edits), perspective)
     3.1 --- a/src/Pure/PIDE/resources.scala	Mon Jan 09 19:34:16 2017 +0100
     3.2 +++ b/src/Pure/PIDE/resources.scala	Mon Jan 09 20:26:59 2017 +0100
     3.3 @@ -17,14 +17,10 @@
     3.4  {
     3.5    def thy_path(path: Path): Path = path.ext("thy")
     3.6  
     3.7 -  val empty: Resources = new Resources(Set.empty, Map.empty, Outer_Syntax.empty)
     3.8 +  val empty: Resources = new Resources(Build.Session_Content.empty)
     3.9  }
    3.10  
    3.11 -class Resources(
    3.12 -  val loaded_theories: Set[String],
    3.13 -  val known_theories: Map[String, Document.Node.Name],
    3.14 -  val base_syntax: Outer_Syntax,
    3.15 -  val log: Logger = No_Logger)
    3.16 +class Resources(val base: Build.Session_Content, val log: Logger = No_Logger)
    3.17  {
    3.18    val thy_info = new Thy_Info(this)
    3.19  
    3.20 @@ -94,10 +90,10 @@
    3.21      val no_qualifier = "" // FIXME
    3.22      val thy1 = Thy_Header.base_name(s)
    3.23      val thy2 = if (Long_Name.is_qualified(thy1)) thy1 else Long_Name.qualify(no_qualifier, thy1)
    3.24 -    (known_theories.get(thy1) orElse
    3.25 -     known_theories.get(thy2) orElse
    3.26 -     known_theories.get(Long_Name.base_name(thy1))) match {
    3.27 -      case Some(name) if loaded_theories(name.theory) => dummy_name(name.theory)
    3.28 +    (base.known_theories.get(thy1) orElse
    3.29 +     base.known_theories.get(thy2) orElse
    3.30 +     base.known_theories.get(Long_Name.base_name(thy1))) match {
    3.31 +      case Some(name) if base.loaded_theories(name.theory) => dummy_name(name.theory)
    3.32        case Some(name) => name
    3.33        case None =>
    3.34          val path = Path.explode(s)
    3.35 @@ -164,7 +160,7 @@
    3.36    def undefined_blobs(nodes: Document.Nodes): List[Document.Node.Name] =
    3.37      (for {
    3.38        (node_name, node) <- nodes.iterator
    3.39 -      if !loaded_theories(node_name.theory)
    3.40 +      if !base.loaded_theories(node_name.theory)
    3.41        cmd <- node.load_commands.iterator
    3.42        name <- cmd.blobs_undefined.iterator
    3.43      } yield name).toList
     4.1 --- a/src/Pure/PIDE/session.scala	Mon Jan 09 19:34:16 2017 +0100
     4.2 +++ b/src/Pure/PIDE/session.scala	Mon Jan 09 20:26:59 2017 +0100
     4.3 @@ -239,7 +239,7 @@
     4.4  
     4.5    def recent_syntax(name: Document.Node.Name): Outer_Syntax =
     4.6      global_state.value.recent_finished.version.get_finished.nodes(name).syntax getOrElse
     4.7 -    resources.base_syntax
     4.8 +    resources.base.syntax
     4.9  
    4.10  
    4.11    /* pipelined change parsing */
     5.1 --- a/src/Pure/Thy/thy_header.scala	Mon Jan 09 19:34:16 2017 +0100
     5.2 +++ b/src/Pure/Thy/thy_header.scala	Mon Jan 09 20:26:59 2017 +0100
     5.3 @@ -37,7 +37,7 @@
     5.4    val AND = "and"
     5.5    val BEGIN = "begin"
     5.6  
     5.7 -  private val bootstrap_header: Keywords =
     5.8 +  val bootstrap_header: Keywords =
     5.9      List(
    5.10        ("%", Keyword.no_spec),
    5.11        ("(", Keyword.no_spec),
     6.1 --- a/src/Pure/Thy/thy_info.scala	Mon Jan 09 19:34:16 2017 +0100
     6.2 +++ b/src/Pure/Thy/thy_info.scala	Mon Jan 09 20:26:59 2017 +0100
     6.3 @@ -71,7 +71,7 @@
     6.4        val import_errors =
     6.5          (for {
     6.6            (theory, names) <- seen_names.iterator_list
     6.7 -          if !resources.loaded_theories(theory)
     6.8 +          if !resources.base.loaded_theories(theory)
     6.9            if names.length > 1
    6.10          } yield
    6.11            "Incoherent imports for theory " + quote(theory) + ":\n" +
    6.12 @@ -83,10 +83,10 @@
    6.13      }
    6.14  
    6.15      lazy val syntax: Outer_Syntax =
    6.16 -      resources.base_syntax.add_keywords(keywords).add_abbrevs(abbrevs)
    6.17 +      resources.base.syntax.add_keywords(keywords).add_abbrevs(abbrevs)
    6.18  
    6.19      def loaded_theories: Set[String] =
    6.20 -      (resources.loaded_theories /: rev_deps) { case (loaded, dep) => loaded + dep.name.theory }
    6.21 +      (resources.base.loaded_theories /: rev_deps) { case (loaded, dep) => loaded + dep.name.theory }
    6.22  
    6.23      def loaded_files: List[Path] =
    6.24      {
    6.25 @@ -118,7 +118,7 @@
    6.26          required_by(initiators) + Position.here(require_pos)
    6.27  
    6.28      val required1 = required + thy
    6.29 -    if (required.seen(name) || resources.loaded_theories(name.theory)) required1
    6.30 +    if (required.seen(name) || resources.base.loaded_theories(name.theory)) required1
    6.31      else {
    6.32        try {
    6.33          if (initiators.contains(name)) error(cycle_msg(initiators))
     7.1 --- a/src/Pure/Thy/thy_syntax.scala	Mon Jan 09 19:34:16 2017 +0100
     7.2 +++ b/src/Pure/Thy/thy_syntax.scala	Mon Jan 09 20:26:59 2017 +0100
     7.3 @@ -101,7 +101,7 @@
     7.4          else {
     7.5            val header = node.header
     7.6            val imports_syntax = header.imports.flatMap(a => nodes(a._1).syntax)
     7.7 -          Some((resources.base_syntax /: imports_syntax)(_ ++ _)
     7.8 +          Some((resources.base.syntax /: imports_syntax)(_ ++ _)
     7.9              .add_keywords(header.keywords).add_abbrevs(header.abbrevs))
    7.10          }
    7.11        nodes += (name -> node.update_syntax(syntax))
    7.12 @@ -297,7 +297,7 @@
    7.13        doc_blobs.get(name) orElse previous.nodes(name).get_blob
    7.14  
    7.15      def can_import(name: Document.Node.Name): Boolean =
    7.16 -      resources.loaded_theories(name.theory) || nodes0(name).has_header
    7.17 +      resources.base.loaded_theories(name.theory) || nodes0(name).has_header
    7.18  
    7.19      val (doc_edits, version) =
    7.20        if (edits.isEmpty) (Nil, Document.Version.make(previous.nodes))
    7.21 @@ -321,7 +321,7 @@
    7.22          node_edits foreach {
    7.23            case (name, edits) =>
    7.24              val node = nodes(name)
    7.25 -            val syntax = node.syntax getOrElse resources.base_syntax
    7.26 +            val syntax = node.syntax getOrElse resources.base.syntax
    7.27              val commands = node.commands
    7.28  
    7.29              val node1 =
     8.1 --- a/src/Pure/Tools/build.scala	Mon Jan 09 19:34:16 2017 +0100
     8.2 +++ b/src/Pure/Tools/build.scala	Mon Jan 09 20:26:59 2017 +0100
     8.3 @@ -98,7 +98,12 @@
     8.4    object Session_Content
     8.5    {
     8.6      def empty: Session_Content =
     8.7 -      Session_Content(Set.empty, Map.empty, Nil, Outer_Syntax.empty, Nil, Graph_Display.empty_graph)
     8.8 +      Session_Content(Set.empty, Map.empty, Nil, Outer_Syntax.empty,
     8.9 +        Nil, Graph_Display.empty_graph)
    8.10 +
    8.11 +    def bootstrap: Session_Content =
    8.12 +      Session_Content(Set.empty, Map.empty, Thy_Header.bootstrap_header,
    8.13 +        Thy_Header.bootstrap_syntax, Nil, Graph_Display.empty_graph)
    8.14    }
    8.15  
    8.16    sealed case class Session_Content(
    8.17 @@ -128,15 +133,12 @@
    8.18            if (progress.stopped) throw Exn.Interrupt()
    8.19  
    8.20            try {
    8.21 -            val (loaded_theories0, known_theories0, syntax0) =
    8.22 -              info.parent.map(deps(_)) match {
    8.23 -                case None =>
    8.24 -                  (Set.empty[String], Map.empty[String, Document.Node.Name],
    8.25 -                    Thy_Header.bootstrap_syntax)
    8.26 -                case Some(parent) =>
    8.27 -                  (parent.loaded_theories, parent.known_theories, parent.syntax)
    8.28 +            val base =
    8.29 +              info.parent match {
    8.30 +                case None => Session_Content.bootstrap
    8.31 +                case Some(parent) => deps(parent)
    8.32                }
    8.33 -            val resources = new Resources(loaded_theories0, known_theories0, syntax0)
    8.34 +            val resources = new Resources(base)
    8.35  
    8.36              if (verbose || list_files) {
    8.37                val groups =
    8.38 @@ -163,7 +165,7 @@
    8.39              }
    8.40  
    8.41              val known_theories =
    8.42 -              (known_theories0 /: thy_deps.deps)({ case (known, dep) =>
    8.43 +              (base.known_theories /: thy_deps.deps)({ case (known, dep) =>
    8.44                  val name = dep.name
    8.45                  known.get(name.theory) match {
    8.46                    case Some(name1) if name != name1 =>
    8.47 @@ -201,7 +203,7 @@
    8.48              val sources = all_files.map(p => (p, SHA1.digest(p.file)))
    8.49  
    8.50              val session_graph =
    8.51 -              Present.session_graph(info.parent getOrElse "", loaded_theories0, thy_deps.deps)
    8.52 +              Present.session_graph(info.parent getOrElse "", base.loaded_theories, thy_deps.deps)
    8.53  
    8.54              val content =
    8.55                Session_Content(loaded_theories, known_theories, keywords, syntax,
     9.1 --- a/src/Tools/VSCode/src/server.scala	Mon Jan 09 19:34:16 2017 +0100
     9.2 +++ b/src/Tools/VSCode/src/server.scala	Mon Jan 09 20:26:59 2017 +0100
     9.3 @@ -199,10 +199,10 @@
     9.4            }
     9.5          }
     9.6  
     9.7 -        val content = Build.session_content(options, false, session_dirs, session_name)
     9.8          val resources =
     9.9 -          new VSCode_Resources(options, text_length, content.loaded_theories,
    9.10 -              content.known_theories, content.syntax, log) {
    9.11 +          new VSCode_Resources(options, text_length,
    9.12 +            Build.session_content(options, false, session_dirs, session_name), log)
    9.13 +          {
    9.14              override def commit(change: Session.Change): Unit =
    9.15                if (change.deps_changed || undefined_blobs(change.version.nodes).nonEmpty)
    9.16                  delay_load.invoke()
    10.1 --- a/src/Tools/VSCode/src/vscode_resources.scala	Mon Jan 09 19:34:16 2017 +0100
    10.2 +++ b/src/Tools/VSCode/src/vscode_resources.scala	Mon Jan 09 20:26:59 2017 +0100
    10.3 @@ -33,13 +33,10 @@
    10.4  }
    10.5  
    10.6  class VSCode_Resources(
    10.7 -    val options: Options,
    10.8 -    val text_length: Text.Length,
    10.9 -    loaded_theories: Set[String],
   10.10 -    known_theories: Map[String, Document.Node.Name],
   10.11 -    base_syntax: Outer_Syntax,
   10.12 -    log: Logger = No_Logger)
   10.13 -  extends Resources(loaded_theories, known_theories, base_syntax, log)
   10.14 +  val options: Options,
   10.15 +  val text_length: Text.Length,
   10.16 +  base: Build.Session_Content,
   10.17 +  log: Logger = No_Logger) extends Resources(base, log)
   10.18  {
   10.19    private val state = Synchronized(VSCode_Resources.State())
   10.20  
    11.1 --- a/src/Tools/jEdit/src/isabelle.scala	Mon Jan 09 19:34:16 2017 +0100
    11.2 +++ b/src/Tools/jEdit/src/isabelle.scala	Mon Jan 09 20:26:59 2017 +0100
    11.3 @@ -50,7 +50,7 @@
    11.4  
    11.5    def mode_syntax(mode: String): Option[Outer_Syntax] =
    11.6      mode match {
    11.7 -      case "isabelle" => Some(PIDE.resources.base_syntax)
    11.8 +      case "isabelle" => Some(PIDE.resources.base.syntax)
    11.9        case "isabelle-options" => Some(Options.options_syntax)
   11.10        case "isabelle-root" => Some(Sessions.root_syntax)
   11.11        case "isabelle-ml" => Some(ml_syntax)
    12.1 --- a/src/Tools/jEdit/src/jedit_resources.scala	Mon Jan 09 19:34:16 2017 +0100
    12.2 +++ b/src/Tools/jEdit/src/jedit_resources.scala	Mon Jan 09 20:26:59 2017 +0100
    12.3 @@ -23,15 +23,10 @@
    12.4  
    12.5  object JEdit_Resources
    12.6  {
    12.7 -  val empty: JEdit_Resources =
    12.8 -    new JEdit_Resources(Set.empty, Map.empty, Outer_Syntax.empty)
    12.9 +  val empty: JEdit_Resources = new JEdit_Resources(Build.Session_Content.empty)
   12.10  }
   12.11  
   12.12 -class JEdit_Resources(
   12.13 -    loaded_theories: Set[String],
   12.14 -    known_theories: Map[String, Document.Node.Name],
   12.15 -    base_syntax: Outer_Syntax)
   12.16 -  extends Resources(loaded_theories, known_theories, base_syntax)
   12.17 +class JEdit_Resources(base: Build.Session_Content) extends Resources(base)
   12.18  {
   12.19    /* document node name */
   12.20  
    13.1 --- a/src/Tools/jEdit/src/plugin.scala	Mon Jan 09 19:34:16 2017 +0100
    13.2 +++ b/src/Tools/jEdit/src/plugin.scala	Mon Jan 09 20:26:59 2017 +0100
    13.3 @@ -386,9 +386,7 @@
    13.4  
    13.5        JEdit_Lib.jedit_text_areas.foreach(Completion_Popup.Text_Area.init _)
    13.6  
    13.7 -      val content = JEdit_Sessions.session_content(false)
    13.8 -      val resources =
    13.9 -        new JEdit_Resources(content.loaded_theories, content.known_theories, content.syntax)
   13.10 +      val resources = new JEdit_Resources(JEdit_Sessions.session_content(false))
   13.11  
   13.12        PIDE.session.stop()
   13.13        PIDE.session = new Session(resources) {
    14.1 --- a/src/Tools/jEdit/src/theories_dockable.scala	Mon Jan 09 19:34:16 2017 +0100
    14.2 +++ b/src/Tools/jEdit/src/theories_dockable.scala	Mon Jan 09 20:26:59 2017 +0100
    14.3 @@ -188,7 +188,7 @@
    14.4        }
    14.5      val nodes_status1 =
    14.6        (nodes_status /: iterator)({ case (status, (name, node)) =>
    14.7 -          if (!name.is_theory || PIDE.resources.loaded_theories(name.theory) || node.is_empty)
    14.8 +          if (!name.is_theory || PIDE.resources.base.loaded_theories(name.theory) || node.is_empty)
    14.9              status
   14.10            else status + (name -> Protocol.node_status(snapshot.state, snapshot.version, node)) })
   14.11  
    15.1 --- a/src/Tools/jEdit/src/timing_dockable.scala	Mon Jan 09 19:34:16 2017 +0100
    15.2 +++ b/src/Tools/jEdit/src/timing_dockable.scala	Mon Jan 09 20:26:59 2017 +0100
    15.3 @@ -187,7 +187,7 @@
    15.4        }
    15.5      val nodes_timing1 =
    15.6        (nodes_timing /: iterator)({ case (timing1, (name, node)) =>
    15.7 -          if (PIDE.resources.loaded_theories(name.theory)) timing1
    15.8 +          if (PIDE.resources.base.loaded_theories(name.theory)) timing1
    15.9            else {
   15.10              val node_timing =
   15.11                Protocol.node_timing(snapshot.state, snapshot.version, node, timing_threshold)