support for separate proof state output;
authorwenzelm
Fri Jun 16 16:21:17 2017 +0200 (2017-06-16)
changeset 660966187612e83c1
parent 66095 78a1aedd1761
child 66097 ee4c2d5b650e
support for separate proof state output;
src/Pure/build-jars
src/Tools/VSCode/extension/package.json
src/Tools/VSCode/extension/src/extension.ts
src/Tools/VSCode/extension/src/protocol.ts
src/Tools/VSCode/src/protocol.scala
src/Tools/VSCode/src/server.scala
src/Tools/VSCode/src/state.scala
     1.1 --- a/src/Pure/build-jars	Fri Jun 16 16:00:44 2017 +0200
     1.2 +++ b/src/Pure/build-jars	Fri Jun 16 16:21:17 2017 +0200
     1.3 @@ -171,6 +171,7 @@
     1.4    ../Tools/VSCode/src/preview.scala
     1.5    ../Tools/VSCode/src/protocol.scala
     1.6    ../Tools/VSCode/src/server.scala
     1.7 +  ../Tools/VSCode/src/state.scala
     1.8    ../Tools/VSCode/src/vscode_rendering.scala
     1.9    ../Tools/VSCode/src/vscode_resources.scala
    1.10  )
     2.1 --- a/src/Tools/VSCode/extension/package.json	Fri Jun 16 16:00:44 2017 +0200
     2.2 +++ b/src/Tools/VSCode/extension/package.json	Fri Jun 16 16:21:17 2017 +0200
     2.3 @@ -33,6 +33,11 @@
     2.4      "contributes": {
     2.5          "commands": [
     2.6              {
     2.7 +                "command": "isabelle.state",
     2.8 +                "title": "Show Proof State",
     2.9 +                "category": "Isabelle"
    2.10 +            },
    2.11 +            {
    2.12                  "command": "isabelle.preview",
    2.13                  "title": "Open Preview",
    2.14                  "category": "Isabelle",
     3.1 --- a/src/Tools/VSCode/extension/src/extension.ts	Fri Jun 16 16:00:44 2017 +0200
     3.2 +++ b/src/Tools/VSCode/extension/src/extension.ts	Fri Jun 16 16:21:17 2017 +0200
     3.3 @@ -6,6 +6,7 @@
     3.4  import * as decorations from './decorations';
     3.5  import * as preview from './preview';
     3.6  import * as protocol from './protocol';
     3.7 +import * as state from './state';
     3.8  import * as symbol from './symbol';
     3.9  import * as completion from './completion';
    3.10  import { ExtensionContext, workspace, window, commands, languages } from 'vscode';
    3.11 @@ -101,6 +102,16 @@
    3.12      })
    3.13  
    3.14  
    3.15 +    /* state */
    3.16 +
    3.17 +    context.subscriptions.push(
    3.18 +      commands.registerCommand("isabelle.state", uri => state.init(uri)),
    3.19 +      commands.registerCommand("_isabelle.state-locate", state.locate),
    3.20 +      commands.registerCommand("_isabelle.state-update", state.update))
    3.21 +
    3.22 +    language_client.onReady().then(() => state.setup(context, language_client))
    3.23 +
    3.24 +
    3.25      /* preview */
    3.26  
    3.27      context.subscriptions.push(
     4.1 --- a/src/Tools/VSCode/extension/src/protocol.ts	Fri Jun 16 16:00:44 2017 +0200
     4.2 +++ b/src/Tools/VSCode/extension/src/protocol.ts	Fri Jun 16 16:21:17 2017 +0200
     4.3 @@ -47,6 +47,28 @@
     4.4    new NotificationType<Dynamic_Output, void>("PIDE/dynamic_output")
     4.5  
     4.6  
     4.7 +/* state */
     4.8 +
     4.9 +export interface State_Output
    4.10 +{
    4.11 +  id: number
    4.12 +  content: string
    4.13 +}
    4.14 +
    4.15 +export const state_output_type =
    4.16 +  new NotificationType<State_Output, void>("PIDE/state_output")
    4.17 +
    4.18 +export interface State_Id
    4.19 +{
    4.20 +  id: number
    4.21 +}
    4.22 +
    4.23 +export const state_init_type = new NotificationType<void, void>("PIDE/state_init")
    4.24 +export const state_exit_type = new NotificationType<State_Id, void>("PIDE/state_exit")
    4.25 +export const state_locate_type = new NotificationType<State_Id, void>("PIDE/state_locate")
    4.26 +export const state_update_type = new NotificationType<State_Id, void>("PIDE/state_update")
    4.27 +
    4.28 +
    4.29  /* preview */
    4.30  
    4.31  export interface Preview_Request
     5.1 --- a/src/Tools/VSCode/src/protocol.scala	Fri Jun 16 16:00:44 2017 +0200
     5.2 +++ b/src/Tools/VSCode/src/protocol.scala	Fri Jun 16 16:21:17 2017 +0200
     5.3 @@ -467,6 +467,29 @@
     5.4    }
     5.5  
     5.6  
     5.7 +  /* state output */
     5.8 +
     5.9 +  object State_Output
    5.10 +  {
    5.11 +    def apply(id: Counter.ID, content: String): JSON.T =
    5.12 +      Notification("PIDE/state_output", Map("id" -> id, "content" -> content))
    5.13 +  }
    5.14 +
    5.15 +  class State_Id_Notification(name: String)
    5.16 +  {
    5.17 +    def unapply(json: JSON.T): Option[Counter.ID] =
    5.18 +      json match {
    5.19 +        case Notification(method, Some(params)) if method == name => JSON.long(params, "id")
    5.20 +        case _ => None
    5.21 +      }
    5.22 +  }
    5.23 +
    5.24 +  object State_Init extends Notification0("PIDE/state_init")
    5.25 +  object State_Exit extends State_Id_Notification("PIDE/state_exit")
    5.26 +  object State_Locate extends State_Id_Notification("PIDE/state_locate")
    5.27 +  object State_Update extends State_Id_Notification("PIDE/state_update")
    5.28 +
    5.29 +
    5.30    /* preview */
    5.31  
    5.32    object Preview_Request
     6.1 --- a/src/Tools/VSCode/src/server.scala	Fri Jun 16 16:00:44 2017 +0200
     6.2 +++ b/src/Tools/VSCode/src/server.scala	Fri Jun 16 16:21:17 2017 +0200
     6.3 @@ -400,6 +400,10 @@
     6.4            case Protocol.GotoDefinition(id, node_pos) => goto_definition(id, node_pos)
     6.5            case Protocol.DocumentHighlights(id, node_pos) => document_highlights(id, node_pos)
     6.6            case Protocol.Caret_Update(caret) => update_caret(caret)
     6.7 +          case Protocol.State_Init(()) => State.init(server)
     6.8 +          case Protocol.State_Exit(id) => State.exit(id)
     6.9 +          case Protocol.State_Locate(id) => State.locate(id)
    6.10 +          case Protocol.State_Update(id) => State.update(id)
    6.11            case Protocol.Preview_Request(file, column) => request_preview(file, column)
    6.12            case Protocol.Symbols_Request(()) => channel.write(Protocol.Symbols())
    6.13            case _ => log("### IGNORED")
     7.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.2 +++ b/src/Tools/VSCode/src/state.scala	Fri Jun 16 16:21:17 2017 +0200
     7.3 @@ -0,0 +1,118 @@
     7.4 +/*  Title:      Tools/VSCode/src/state.scala
     7.5 +    Author:     Makarius
     7.6 +
     7.7 +Show proof state.
     7.8 +*/
     7.9 +
    7.10 +package isabelle.vscode
    7.11 +
    7.12 +
    7.13 +import isabelle._
    7.14 +
    7.15 +
    7.16 +object State
    7.17 +{
    7.18 +  private val make_id = Counter.make()
    7.19 +  private val instances = Synchronized(Map.empty[Counter.ID, State])
    7.20 +
    7.21 +  def init(server: Server)
    7.22 +  {
    7.23 +    val instance = new State(server)
    7.24 +    instances.change(_ + (instance.id -> instance))
    7.25 +    instance.init()
    7.26 +  }
    7.27 +
    7.28 +  def exit(id: Counter.ID)
    7.29 +  {
    7.30 +    instances.change(map =>
    7.31 +      map.get(id) match {
    7.32 +        case None => map
    7.33 +        case Some(instance) => instance.exit(); map - id
    7.34 +      })
    7.35 +  }
    7.36 +
    7.37 +  def locate(id: Counter.ID): Unit =
    7.38 +    instances.value.get(id).foreach(state =>
    7.39 +      state.server.editor.send_dispatcher(state.locate()))
    7.40 +
    7.41 +  def update(id: Counter.ID): Unit =
    7.42 +    instances.value.get(id).foreach(state =>
    7.43 +      state.server.editor.send_dispatcher(state.update()))
    7.44 +}
    7.45 +
    7.46 +
    7.47 +class State private(val server: Server)
    7.48 +{
    7.49 +  /* output */
    7.50 +
    7.51 +  val id: Counter.ID = State.make_id()
    7.52 +
    7.53 +  private def output(content: String): Unit =
    7.54 +    server.channel.write(Protocol.State_Output(id, content))
    7.55 +
    7.56 +
    7.57 +  /* query operation */
    7.58 +
    7.59 +  private val print_state =
    7.60 +    new Query_Operation(server.editor, (), "print_state", _ => (),
    7.61 +      (snapshot, results, body) =>
    7.62 +        {
    7.63 +          val text = server.resources.output_pretty_message(Pretty.separate(body))
    7.64 +          val content =
    7.65 +            HTML.output_document(
    7.66 +              List(HTML.style(HTML.fonts_css()),
    7.67 +                HTML.style_file(Url.print_file(HTML.isabelle_css.file))),
    7.68 +              List(
    7.69 +                HTML.chapter("Proof state"),
    7.70 +                HTML.source(text)),
    7.71 +              css = "")
    7.72 +          output(content)
    7.73 +        })
    7.74 +
    7.75 +  def locate() { print_state.locate_query() }
    7.76 +
    7.77 +  def update()
    7.78 +  {
    7.79 +    server.editor.current_node_snapshot(()) match {
    7.80 +      case Some(snapshot) =>
    7.81 +        (server.editor.current_command((), snapshot), print_state.get_location) match {
    7.82 +          case (Some(command1), Some(command2)) if command1.id == command2.id =>
    7.83 +          case _ => print_state.apply_query(Nil)
    7.84 +        }
    7.85 +      case None =>
    7.86 +    }
    7.87 +  }
    7.88 +
    7.89 +
    7.90 +  /* auto update */
    7.91 +
    7.92 +  private val auto_update_enabled = Synchronized(true)
    7.93 +
    7.94 +  def set_auto_update(b: Boolean) { auto_update_enabled.change(_ => b); if (b) update() }
    7.95 +
    7.96 +  def auto_update(): Unit = if (auto_update_enabled.value) update()
    7.97 +
    7.98 +
    7.99 +  /* main */
   7.100 +
   7.101 +  private val main =
   7.102 +    Session.Consumer[Any](getClass.getName) {
   7.103 +      case changed: Session.Commands_Changed => if (changed.assignment) auto_update()
   7.104 +      case Session.Caret_Focus => auto_update()
   7.105 +    }
   7.106 +
   7.107 +  def init()
   7.108 +  {
   7.109 +    server.session.commands_changed += main
   7.110 +    server.session.caret_focus += main
   7.111 +    server.editor.send_wait_dispatcher { print_state.activate() }
   7.112 +    server.editor.send_dispatcher { auto_update() }
   7.113 +  }
   7.114 +
   7.115 +  def exit()
   7.116 +  {
   7.117 +    server.editor.send_wait_dispatcher { print_state.deactivate() }
   7.118 +    server.session.commands_changed -= main
   7.119 +    server.session.caret_focus -= main
   7.120 +  }
   7.121 +}