clarified signature: prefer Document.Snapshot;
authorwenzelm
Sun Jun 03 20:37:16 2018 +0200 (13 months ago)
changeset 68365f9379279f98c
parent 68364 5c579bb9adb1
child 68366 cd387c55e085
clarified signature: prefer Document.Snapshot;
src/Pure/PIDE/document.scala
src/Pure/Thy/thy_resources.scala
src/Pure/Tools/dump.scala
src/Pure/Tools/server_commands.scala
     1.1 --- a/src/Pure/PIDE/document.scala	Sun Jun 03 19:06:56 2018 +0200
     1.2 +++ b/src/Pure/PIDE/document.scala	Sun Jun 03 20:37:16 2018 +0200
     1.3 @@ -537,6 +537,8 @@
     1.4      def current_command(other_node_name: Node.Name, offset: Text.Offset): Option[Command]
     1.5  
     1.6      def markup_to_XML(range: Text.Range, elements: Markup.Elements): XML.Body
     1.7 +    def messages: List[(XML.Tree, Position.T)]
     1.8 +    def exports: List[Export.Entry]
     1.9  
    1.10      def find_command(id: Document_ID.Generic): Option[(Node, Command)]
    1.11      def find_command_position(id: Document_ID.Generic, offset: Symbol.Offset)
    1.12 @@ -1006,6 +1008,22 @@
    1.13          def markup_to_XML(range: Text.Range, elements: Markup.Elements): XML.Body =
    1.14            state.markup_to_XML(version, node_name, range, elements)
    1.15  
    1.16 +        def messages: List[(XML.Tree, Position.T)] =
    1.17 +          (for {
    1.18 +            (command, start) <-
    1.19 +              Document.Node.Commands.starts_pos(
    1.20 +                node.commands.iterator, Token.Pos.file(node_name.node))
    1.21 +            pos = command.span.keyword_pos(start).position(command.span.name)
    1.22 +            (_, tree) <- state.command_results(version, command).iterator
    1.23 +           } yield (tree, pos)).toList
    1.24 +
    1.25 +        def exports: List[Export.Entry] =
    1.26 +          Command.Exports.merge(
    1.27 +            for {
    1.28 +              command <- node.commands.iterator
    1.29 +              st <- state.command_states(version, command).iterator
    1.30 +            } yield st.exports).iterator.map(_._2).toList
    1.31 +
    1.32  
    1.33          /* find command */
    1.34  
     2.1 --- a/src/Pure/Thy/thy_resources.scala	Sun Jun 03 19:06:56 2018 +0200
     2.2 +++ b/src/Pure/Thy/thy_resources.scala	Sun Jun 03 20:37:16 2018 +0200
     2.3 @@ -55,7 +55,7 @@
     2.4      }
     2.5    }
     2.6  
     2.7 -  sealed case class Theories_Result(
     2.8 +  class Theories_Result private[Thy_Resources](
     2.9      val state: Document.State,
    2.10      val version: Document.Version,
    2.11      val nodes: List[(Document.Node.Name, Protocol.Node_Status)])
    2.12 @@ -63,32 +63,11 @@
    2.13      def node_names: List[Document.Node.Name] = nodes.map(_._1)
    2.14      def ok: Boolean = nodes.forall({ case (_, st) => st.ok })
    2.15  
    2.16 -    def messages(node_name: Document.Node.Name): List[(XML.Tree, Position.T)] =
    2.17 +    def snapshot(node_name: Document.Node.Name): Document.Snapshot =
    2.18      {
    2.19 -      val node = version.nodes(node_name)
    2.20 -      (for {
    2.21 -        (command, start) <-
    2.22 -          Document.Node.Commands.starts_pos(node.commands.iterator, Token.Pos.file(node_name.node))
    2.23 -        pos = command.span.keyword_pos(start).position(command.span.name)
    2.24 -        (_, tree) <- state.command_results(version, command).iterator
    2.25 -       } yield (tree, pos)).toList
    2.26 -    }
    2.27 -
    2.28 -    def markup_to_XML(node_name: Document.Node.Name,
    2.29 -      range: Text.Range = Text.Range.full,
    2.30 -      elements: Markup.Elements = Markup.Elements.full): XML.Body =
    2.31 -    {
    2.32 -      state.markup_to_XML(version, node_name, range, elements)
    2.33 -    }
    2.34 -
    2.35 -    def exports(node_name: Document.Node.Name): List[Export.Entry] =
    2.36 -    {
    2.37 -      val node = version.nodes(node_name)
    2.38 -      Command.Exports.merge(
    2.39 -        for {
    2.40 -          command <- node.commands.iterator
    2.41 -          st <- state.command_states(version, command).iterator
    2.42 -        } yield st.exports).iterator.map(_._2).toList
    2.43 +      val snapshot = state.snapshot(node_name)
    2.44 +      assert(version.id == snapshot.version.id)
    2.45 +      snapshot
    2.46      }
    2.47    }
    2.48  
    2.49 @@ -134,7 +113,7 @@
    2.50              val nodes =
    2.51                for (name <- dep_theories)
    2.52                yield (name -> Protocol.node_status(state, version, name))
    2.53 -            try { result.fulfill(Theories_Result(state, version, nodes)) }
    2.54 +            try { result.fulfill(new Theories_Result(state, version, nodes)) }
    2.55              catch { case _: IllegalStateException => }
    2.56            case _ =>
    2.57          }
     3.1 --- a/src/Pure/Tools/dump.scala	Sun Jun 03 19:06:56 2018 +0200
     3.2 +++ b/src/Pure/Tools/dump.scala	Sun Jun 03 20:37:16 2018 +0200
     3.3 @@ -14,22 +14,24 @@
     3.4    sealed case class Aspect_Args(
     3.5      options: Options,
     3.6      progress: Progress,
     3.7 +    deps: Sessions.Deps,
     3.8      output_dir: Path,
     3.9 -    deps: Sessions.Deps,
    3.10 -    result: Thy_Resources.Theories_Result)
    3.11 +    node_name: Document.Node.Name,
    3.12 +    node_status: Protocol.Node_Status,
    3.13 +    snapshot: Document.Snapshot)
    3.14    {
    3.15 -    def write(node_name: Document.Node.Name, file_name: Path, bytes: Bytes)
    3.16 +    def write(file_name: Path, bytes: Bytes)
    3.17      {
    3.18        val path = output_dir + Path.basic(node_name.theory) + file_name
    3.19        Isabelle_System.mkdirs(path.dir)
    3.20        Bytes.write(path, bytes)
    3.21      }
    3.22  
    3.23 -    def write(node_name: Document.Node.Name, file_name: Path, text: String): Unit =
    3.24 -      write(node_name, file_name, Bytes(text))
    3.25 +    def write(file_name: Path, text: String): Unit =
    3.26 +      write(file_name, Bytes(text))
    3.27  
    3.28 -    def write(node_name: Document.Node.Name, file_name: Path, body: XML.Body): Unit =
    3.29 -      write(node_name, file_name, Symbol.encode(YXML.string_of_body(body)))
    3.30 +    def write(file_name: Path, body: XML.Body): Unit =
    3.31 +      write(file_name, Symbol.encode(YXML.string_of_body(body)))
    3.32    }
    3.33  
    3.34    sealed case class Aspect(name: String, description: String, operation: Aspect_Args => Unit,
    3.35 @@ -40,35 +42,27 @@
    3.36  
    3.37    val known_aspects =
    3.38      List(
    3.39 +      Aspect("markup", "PIDE markup (YXML format)",
    3.40 +        { case args =>
    3.41 +            args.write(Path.explode("markup.yxml"),
    3.42 +              args.snapshot.markup_to_XML(Text.Range.full, Markup.Elements.full))
    3.43 +        }),
    3.44        Aspect("messages", "output messages (YXML format)",
    3.45          { case args =>
    3.46 -            for (node_name <- args.result.node_names) {
    3.47 -              args.write(node_name, Path.explode("messages.yxml"),
    3.48 -                args.result.messages(node_name).iterator.map(_._1).toList)
    3.49 -            }
    3.50 -        }),
    3.51 -      Aspect("markup", "PIDE markup (YXML format)",
    3.52 -        { case args =>
    3.53 -            for (node_name <- args.result.node_names) {
    3.54 -              args.write(node_name, Path.explode("markup.yxml"),
    3.55 -                args.result.markup_to_XML(node_name))
    3.56 -            }
    3.57 +            args.write(Path.explode("messages.yxml"),
    3.58 +              args.snapshot.messages.iterator.map(_._1).toList)
    3.59          }),
    3.60        Aspect("latex", "generated LaTeX source",
    3.61          { case args =>
    3.62 -            for {
    3.63 -              node_name <- args.result.node_names
    3.64 -              entry <- args.result.exports(node_name)
    3.65 -              if entry.name == "document.tex"
    3.66 -            } args.write(node_name, Path.explode(entry.name), entry.uncompressed())
    3.67 +            for (entry <- args.snapshot.exports if entry.name == "document.tex")
    3.68 +              args.write(Path.explode(entry.name), entry.uncompressed())
    3.69          }, options = List("editor_presentation")),
    3.70        Aspect("theory", "foundational theory content",
    3.71          { case args =>
    3.72              for {
    3.73 -              node_name <- args.result.node_names
    3.74 -              entry <- args.result.exports(node_name)
    3.75 +              entry <- args.snapshot.exports
    3.76                if entry.name.startsWith(Export_Theory.export_prefix)
    3.77 -            } args.write(node_name, Path.explode(entry.name), entry.uncompressed())
    3.78 +            } args.write(Path.explode(entry.name), entry.uncompressed())
    3.79          }, options = List("editor_presentation", "export_theory"))
    3.80      ).sortBy(_.name)
    3.81  
    3.82 @@ -129,8 +123,12 @@
    3.83  
    3.84      /* dump aspects */
    3.85  
    3.86 -    val aspect_args = Aspect_Args(dump_options, progress, output_dir, deps, theories_result)
    3.87 -    aspects.foreach(_.operation(aspect_args))
    3.88 +    for ((node_name, node_status) <- theories_result.nodes) {
    3.89 +      val snapshot = theories_result.snapshot(node_name)
    3.90 +      val aspect_args =
    3.91 +        Aspect_Args(dump_options, progress, deps, output_dir, node_name, node_status, snapshot)
    3.92 +      aspects.foreach(_.operation(aspect_args))
    3.93 +    }
    3.94  
    3.95      session_result
    3.96    }
     4.1 --- a/src/Pure/Tools/server_commands.scala	Sun Jun 03 19:06:56 2018 +0200
     4.2 +++ b/src/Pure/Tools/server_commands.scala	Sun Jun 03 20:37:16 2018 +0200
     4.3 @@ -205,25 +205,27 @@
     4.4            "errors" ->
     4.5              (for {
     4.6                (name, status) <- result.nodes if !status.ok
     4.7 -              (tree, pos) <- result.messages(name) if Protocol.is_error(tree)
     4.8 +              (tree, pos) <- result.snapshot(name).messages if Protocol.is_error(tree)
     4.9              } yield output_message(tree, pos)),
    4.10            "nodes" ->
    4.11 -            (for ((name, status) <- result.nodes) yield
    4.12 +            (for ((name, status) <- result.nodes) yield {
    4.13 +              val snapshot = result.snapshot(name)
    4.14                name.json +
    4.15                  ("status" -> status.json) +
    4.16                  ("messages" ->
    4.17                    (for {
    4.18 -                    (tree, pos) <- result.messages(name) if Protocol.is_exported(tree)
    4.19 +                    (tree, pos) <- snapshot.messages if Protocol.is_exported(tree)
    4.20                    } yield output_message(tree, pos))) +
    4.21                  ("exports" ->
    4.22                    (if (args.export_pattern == "") Nil else {
    4.23                      val matcher = Export.make_matcher(args.export_pattern)
    4.24 -                    for { entry <- result.exports(name) if matcher(entry.theory_name, entry.name) }
    4.25 +                    for { entry <- snapshot.exports if matcher(entry.theory_name, entry.name) }
    4.26                      yield {
    4.27                        val (base64, body) = entry.uncompressed().maybe_base64
    4.28                        JSON.Object("name" -> entry.name, "base64" -> base64, "body" -> body)
    4.29                      }
    4.30 -                  }))))
    4.31 +                  }))
    4.32 +            }))
    4.33  
    4.34        (result_json, result)
    4.35      }