dynamic output, depending on caret focus (see also Tools/jEdit/src/output_dockable.scala);
authorwenzelm
Sat Mar 11 23:12:55 2017 +0100 (2017-03-11)
changeset 651914c9c83311cad
parent 65190 0dd2ad9dbfc2
child 65192 7b8dc3910b96
dynamic output, depending on caret focus (see also Tools/jEdit/src/output_dockable.scala);
src/Pure/build-jars
src/Tools/VSCode/extension/src/extension.ts
src/Tools/VSCode/src/document_model.scala
src/Tools/VSCode/src/dynamic_output.scala
src/Tools/VSCode/src/server.scala
src/Tools/VSCode/src/vscode_resources.scala
     1.1 --- a/src/Pure/build-jars	Sat Mar 11 22:19:22 2017 +0100
     1.2 +++ b/src/Pure/build-jars	Sat Mar 11 23:12:55 2017 +0100
     1.3 @@ -164,6 +164,7 @@
     1.4    ../Tools/VSCode/src/build_vscode.scala
     1.5    ../Tools/VSCode/src/channel.scala
     1.6    ../Tools/VSCode/src/document_model.scala
     1.7 +  ../Tools/VSCode/src/dynamic_output.scala
     1.8    ../Tools/VSCode/src/grammar.scala
     1.9    ../Tools/VSCode/src/protocol.scala
    1.10    ../Tools/VSCode/src/server.scala
     2.1 --- a/src/Tools/VSCode/extension/src/extension.ts	Sat Mar 11 22:19:22 2017 +0100
     2.2 +++ b/src/Tools/VSCode/extension/src/extension.ts	Sat Mar 11 23:12:55 2017 +0100
     2.3 @@ -37,8 +37,6 @@
     2.4  const dynamic_output_type = new NotificationType<string, void>("PIDE/dynamic_output")
     2.5  
     2.6  let last_caret_update: Caret_Update = {}
     2.7 -let dynamic_output: string = ""
     2.8 -
     2.9  
    2.10  
    2.11  /* activate extension */
    2.12 @@ -77,6 +75,11 @@
    2.13  
    2.14      /* caret handling and dynamic output */
    2.15  
    2.16 +    const dynamic_output = vscode.window.createOutputChannel("Isabelle Output")
    2.17 +    context.subscriptions.push(dynamic_output)
    2.18 +    dynamic_output.show(true)
    2.19 +    dynamic_output.hide()
    2.20 +
    2.21      function update_caret()
    2.22      {
    2.23        const editor = vscode.window.activeTextEditor
    2.24 @@ -95,7 +98,13 @@
    2.25  
    2.26      client.onReady().then(() =>
    2.27      {
    2.28 -      client.onNotification(dynamic_output_type, body => { dynamic_output = body })
    2.29 +      client.onNotification(dynamic_output_type,
    2.30 +        body => {
    2.31 +          if (body) {
    2.32 +            dynamic_output.clear()
    2.33 +            dynamic_output.appendLine(body)
    2.34 +          }
    2.35 +        })
    2.36        vscode.window.onDidChangeActiveTextEditor(_ => update_caret())
    2.37        vscode.window.onDidChangeTextEditorSelection(_ => update_caret())
    2.38        update_caret()
     3.1 --- a/src/Tools/VSCode/src/document_model.scala	Sat Mar 11 22:19:22 2017 +0100
     3.2 +++ b/src/Tools/VSCode/src/document_model.scala	Sat Mar 11 23:12:55 2017 +0100
     3.3 @@ -158,6 +158,24 @@
     3.4    }
     3.5  
     3.6  
     3.7 +  /* current command */
     3.8 +
     3.9 +  def current_command(snapshot: Document.Snapshot, current_offset: Text.Offset): Option[Command] =
    3.10 +  {
    3.11 +    if (is_theory) {
    3.12 +      val node = snapshot.version.nodes(node_name)
    3.13 +      val caret = snapshot.revert(current_offset)
    3.14 +      val caret_command_iterator = node.command_iterator(caret)
    3.15 +      if (caret_command_iterator.hasNext) {
    3.16 +        val (cmd0, _) = caret_command_iterator.next
    3.17 +        node.commands.reverse.iterator(cmd0).find(cmd => !cmd.is_ignored)
    3.18 +      }
    3.19 +      else None
    3.20 +    }
    3.21 +    else snapshot.version.nodes.commands_loading(node_name).headOption
    3.22 +  }
    3.23 +
    3.24 +
    3.25    /* prover session */
    3.26  
    3.27    def resources: VSCode_Resources = session.resources.asInstanceOf[VSCode_Resources]
    3.28 @@ -165,5 +183,7 @@
    3.29    def is_stable: Boolean = pending_edits.isEmpty
    3.30    def snapshot(): Document.Snapshot = session.snapshot(node_name, pending_edits)
    3.31  
    3.32 -  def rendering(): VSCode_Rendering = new VSCode_Rendering(this, snapshot(), resources)
    3.33 +  def rendering(snapshot: Document.Snapshot): VSCode_Rendering =
    3.34 +    new VSCode_Rendering(this, snapshot, resources)
    3.35 +  def rendering(): VSCode_Rendering = rendering(snapshot())
    3.36  }
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/Tools/VSCode/src/dynamic_output.scala	Sat Mar 11 23:12:55 2017 +0100
     4.3 @@ -0,0 +1,88 @@
     4.4 +/*  Title:      Tools/VSCode/src/dynamic_output.scala
     4.5 +    Author:     Makarius
     4.6 +
     4.7 +Dynamic output, depending on caret focus: messages, state etc.
     4.8 +*/
     4.9 +
    4.10 +package isabelle.vscode
    4.11 +
    4.12 +
    4.13 +import isabelle._
    4.14 +
    4.15 +
    4.16 +object Dynamic_Output
    4.17 +{
    4.18 +  case class State(
    4.19 +    do_update: Boolean = true,
    4.20 +    snapshot: Document.Snapshot = Document.Snapshot.init,
    4.21 +    command: Command = Command.empty,
    4.22 +    results: Command.Results = Command.Results.empty,
    4.23 +    output: List[XML.Tree] = Nil)
    4.24 +
    4.25 +  def apply(server: Server): Dynamic_Output = new Dynamic_Output(server)
    4.26 +}
    4.27 +
    4.28 +
    4.29 +class Dynamic_Output private(server: Server)
    4.30 +{
    4.31 +  private val state = Synchronized(Dynamic_Output.State())
    4.32 +
    4.33 +  private def handle_update(restriction: Option[Set[Command]])
    4.34 +  {
    4.35 +    state.change(st =>
    4.36 +      {
    4.37 +        val resources = server.resources
    4.38 +        def init_st = Dynamic_Output.State(st.do_update)
    4.39 +        val st1 =
    4.40 +          resources.caret_range() match {
    4.41 +            case None => init_st
    4.42 +            case Some((model, caret_range)) =>
    4.43 +              val snapshot = model.snapshot()
    4.44 +              if (st.do_update && !snapshot.is_outdated) {
    4.45 +                model.current_command(snapshot, caret_range.start) match {
    4.46 +                  case None => init_st
    4.47 +                  case Some(command) =>
    4.48 +                    val results = snapshot.state.command_results(snapshot.version, command)
    4.49 +                    val output =
    4.50 +                      if (!restriction.isDefined || restriction.get.contains(command))
    4.51 +                        Rendering.output_messages(results)
    4.52 +                      else st.output
    4.53 +                    st.copy(
    4.54 +                      snapshot = snapshot, command = command, results = results, output = output)
    4.55 +                }
    4.56 +              }
    4.57 +              else st
    4.58 +          }
    4.59 +        if (st1.output != st.output) {
    4.60 +          server.channel.write(Protocol.Dynamic_Output(
    4.61 +            resources.output_pretty_message(Pretty.separate(st1.output))))
    4.62 +        }
    4.63 +        st1
    4.64 +      })
    4.65 +  }
    4.66 +
    4.67 +
    4.68 +  /* main */
    4.69 +
    4.70 +  private val main =
    4.71 +    Session.Consumer[Any](getClass.getName) {
    4.72 +      case changed: Session.Commands_Changed =>
    4.73 +        handle_update(if (changed.assignment) None else Some(changed.commands))
    4.74 +
    4.75 +      case Session.Caret_Focus =>
    4.76 +        handle_update(None)
    4.77 +    }
    4.78 +
    4.79 +  def init()
    4.80 +  {
    4.81 +    server.session.commands_changed += main
    4.82 +    server.session.caret_focus += main
    4.83 +    handle_update(None)
    4.84 +  }
    4.85 +
    4.86 +  def exit()
    4.87 +  {
    4.88 +    server.session.commands_changed -= main
    4.89 +    server.session.caret_focus -= main
    4.90 +  }
    4.91 +}
     5.1 --- a/src/Tools/VSCode/src/server.scala	Sat Mar 11 22:19:22 2017 +0100
     5.2 +++ b/src/Tools/VSCode/src/server.scala	Sat Mar 11 23:12:55 2017 +0100
     5.3 @@ -87,7 +87,7 @@
     5.4  }
     5.5  
     5.6  class Server(
     5.7 -  channel: Channel,
     5.8 +  val channel: Channel,
     5.9    options: Options,
    5.10    text_length: Text.Length = Text.Length.encoding(Server.default_text_length),
    5.11    session_name: String = Server.default_logic,
    5.12 @@ -109,6 +109,8 @@
    5.13        offset <- model.content.doc.offset(node_pos.pos)
    5.14      } yield (rendering, offset)
    5.15  
    5.16 +  private val dynamic_output = Dynamic_Output(this)
    5.17 +
    5.18  
    5.19    /* input from client or file-system */
    5.20  
    5.21 @@ -238,6 +240,8 @@
    5.22        catch { case ERROR(msg) => reply(msg); None }
    5.23  
    5.24      for (session <- try_session) {
    5.25 +      session_.change(_ => Some(session))
    5.26 +
    5.27        var session_phase: Session.Consumer[Session.Phase] = null
    5.28        session_phase =
    5.29          Session.Consumer(getClass.getName) {
    5.30 @@ -255,11 +259,11 @@
    5.31        session.commands_changed += prover_output
    5.32        session.all_messages += syslog
    5.33  
    5.34 +      dynamic_output.init()
    5.35 +
    5.36        session.start(receiver =>
    5.37          Isabelle_Process(options = options, logic = session_name, dirs = session_dirs,
    5.38            modes = modes, receiver = receiver))
    5.39 -
    5.40 -      session_.change(_ => Some(session))
    5.41      }
    5.42    }
    5.43  
    5.44 @@ -269,6 +273,7 @@
    5.45  
    5.46      session_.change({
    5.47        case Some(session) =>
    5.48 +        dynamic_output.exit()
    5.49          var session_phase: Session.Consumer[Session.Phase] = null
    5.50          session_phase =
    5.51            Session.Consumer(getClass.getName) {
     6.1 --- a/src/Tools/VSCode/src/vscode_resources.scala	Sat Mar 11 22:19:22 2017 +0100
     6.2 +++ b/src/Tools/VSCode/src/vscode_resources.scala	Sat Mar 11 23:12:55 2017 +0100
     6.3 @@ -277,17 +277,19 @@
     6.4  
     6.5    /* caret handling */
     6.6  
     6.7 -  def update_caret(new_caret: Option[(JFile, Line.Position)])
     6.8 -  { state.change(_.copy(caret = new_caret)) }
     6.9 +  def update_caret(caret: Option[(JFile, Line.Position)])
    6.10 +  { state.change(_.copy(caret = caret)) }
    6.11  
    6.12 -  def caret_position: Option[(Document_Model, Line.Position)] =
    6.13 +  def caret_range(): Option[(Document_Model, Text.Range)] =
    6.14    {
    6.15      val st = state.value
    6.16      for {
    6.17        (file, pos) <- st.caret
    6.18        model <- st.models.get(file)
    6.19 +      offset <- model.content.doc.offset(pos)
    6.20 +      if offset < model.content.doc.text_range.stop
    6.21      }
    6.22 -    yield (model, pos)
    6.23 +    yield (model, Text.Range(offset, offset + 1))
    6.24    }
    6.25  
    6.26