clarified modules;
authorwenzelm
Fri Jun 16 21:04:39 2017 +0200 (2017-06-16)
changeset 660985aa9cb83e70e
parent 66097 ee4c2d5b650e
child 66099 d1639e7877cc
clarified modules;
src/Pure/build-jars
src/Tools/VSCode/extension/src/extension.ts
src/Tools/VSCode/src/preview.scala
src/Tools/VSCode/src/preview_panel.scala
src/Tools/VSCode/src/server.scala
src/Tools/VSCode/src/state.scala
src/Tools/VSCode/src/state_panel.scala
     1.1 --- a/src/Pure/build-jars	Fri Jun 16 20:44:36 2017 +0200
     1.2 +++ b/src/Pure/build-jars	Fri Jun 16 21:04:39 2017 +0200
     1.3 @@ -168,10 +168,10 @@
     1.4    ../Tools/VSCode/src/document_model.scala
     1.5    ../Tools/VSCode/src/dynamic_output.scala
     1.6    ../Tools/VSCode/src/grammar.scala
     1.7 -  ../Tools/VSCode/src/preview.scala
     1.8 +  ../Tools/VSCode/src/preview_panel.scala
     1.9    ../Tools/VSCode/src/protocol.scala
    1.10    ../Tools/VSCode/src/server.scala
    1.11 -  ../Tools/VSCode/src/state.scala
    1.12 +  ../Tools/VSCode/src/state_panel.scala
    1.13    ../Tools/VSCode/src/vscode_rendering.scala
    1.14    ../Tools/VSCode/src/vscode_resources.scala
    1.15  )
     2.1 --- a/src/Tools/VSCode/extension/src/extension.ts	Fri Jun 16 20:44:36 2017 +0200
     2.2 +++ b/src/Tools/VSCode/extension/src/extension.ts	Fri Jun 16 21:04:39 2017 +0200
     2.3 @@ -4,9 +4,9 @@
     2.4  import * as fs from 'fs';
     2.5  import * as library from './library'
     2.6  import * as decorations from './decorations';
     2.7 -import * as preview from './preview';
     2.8 +import * as preview_panel from './preview_panel';
     2.9  import * as protocol from './protocol';
    2.10 -import * as state from './state';
    2.11 +import * as state_panel from './state_panel';
    2.12  import * as symbol from './symbol';
    2.13  import * as completion from './completion';
    2.14  import { ExtensionContext, workspace, window, commands, languages } from 'vscode';
    2.15 @@ -102,25 +102,25 @@
    2.16      })
    2.17  
    2.18  
    2.19 -    /* state */
    2.20 +    /* state panel */
    2.21  
    2.22      context.subscriptions.push(
    2.23 -      commands.registerCommand("isabelle.state", uri => state.init(uri)),
    2.24 -      commands.registerCommand("_isabelle.state-locate", state.locate),
    2.25 -      commands.registerCommand("_isabelle.state-update", state.update))
    2.26 +      commands.registerCommand("isabelle.state", uri => state_panel.init(uri)),
    2.27 +      commands.registerCommand("_isabelle.state-locate", state_panel.locate),
    2.28 +      commands.registerCommand("_isabelle.state-update", state_panel.update))
    2.29  
    2.30 -    language_client.onReady().then(() => state.setup(context, language_client))
    2.31 +    language_client.onReady().then(() => state_panel.setup(context, language_client))
    2.32  
    2.33  
    2.34 -    /* preview */
    2.35 +    /* preview panel */
    2.36  
    2.37      context.subscriptions.push(
    2.38 -      commands.registerCommand("isabelle.preview", uri => preview.request(uri, false)),
    2.39 -      commands.registerCommand("isabelle.preview-split", uri => preview.request(uri, true)),
    2.40 -      commands.registerCommand("isabelle.preview-source", preview.source),
    2.41 -      commands.registerCommand("isabelle.preview-update", preview.update))
    2.42 +      commands.registerCommand("isabelle.preview", uri => preview_panel.request(uri, false)),
    2.43 +      commands.registerCommand("isabelle.preview-split", uri => preview_panel.request(uri, true)),
    2.44 +      commands.registerCommand("isabelle.preview-source", preview_panel.source),
    2.45 +      commands.registerCommand("isabelle.preview-update", preview_panel.update))
    2.46  
    2.47 -    language_client.onReady().then(() => preview.setup(context, language_client))
    2.48 +    language_client.onReady().then(() => preview_panel.setup(context, language_client))
    2.49  
    2.50  
    2.51      /* Isabelle symbols */
     3.1 --- a/src/Tools/VSCode/src/preview.scala	Fri Jun 16 20:44:36 2017 +0200
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,56 +0,0 @@
     3.4 -/*  Title:      Tools/VSCode/src/preview.scala
     3.5 -    Author:     Makarius
     3.6 -
     3.7 -HTML document preview.
     3.8 -*/
     3.9 -
    3.10 -package isabelle.vscode
    3.11 -
    3.12 -
    3.13 -import isabelle._
    3.14 -
    3.15 -import java.io.{File => JFile}
    3.16 -
    3.17 -
    3.18 -class Preview(resources: VSCode_Resources)
    3.19 -{
    3.20 -  private val pending = Synchronized(Map.empty[JFile, Int])
    3.21 -
    3.22 -  def request(file: JFile, column: Int): Unit =
    3.23 -    pending.change(map => map + (file -> column))
    3.24 -
    3.25 -  def flush(channel: Channel): Boolean =
    3.26 -  {
    3.27 -    pending.change_result(map =>
    3.28 -    {
    3.29 -      val map1 =
    3.30 -        (map /: map.iterator)({ case (m, (file, column)) =>
    3.31 -          resources.get_model(file) match {
    3.32 -            case Some(model) =>
    3.33 -              val snapshot = model.snapshot()
    3.34 -              if (snapshot.is_outdated) m
    3.35 -              else {
    3.36 -                val (label, content) = make_preview(model, snapshot)
    3.37 -                channel.write(Protocol.Preview_Response(file, column, label, content))
    3.38 -                m - file
    3.39 -              }
    3.40 -            case None => m - file
    3.41 -          }
    3.42 -        })
    3.43 -      (map1.nonEmpty, map1)
    3.44 -    })
    3.45 -  }
    3.46 -
    3.47 -  def make_preview(model: Document_Model, snapshot: Document.Snapshot): (String, String) =
    3.48 -  {
    3.49 -    val label = "Preview " + quote(model.node_name.toString)
    3.50 -    val content =
    3.51 -      HTML.output_document(
    3.52 -        List(HTML.style(HTML.fonts_css()), HTML.style_file(Url.print_file(HTML.isabelle_css.file))),
    3.53 -        List(
    3.54 -          HTML.chapter("Theory " + quote(model.node_name.theory_base_name)),
    3.55 -          HTML.source(Present.theory_document(snapshot))),
    3.56 -        css = "")
    3.57 -    (label, content)
    3.58 -  }
    3.59 -}
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/Tools/VSCode/src/preview_panel.scala	Fri Jun 16 21:04:39 2017 +0200
     4.3 @@ -0,0 +1,56 @@
     4.4 +/*  Title:      Tools/VSCode/src/preview_panel.scala
     4.5 +    Author:     Makarius
     4.6 +
     4.7 +HTML document preview.
     4.8 +*/
     4.9 +
    4.10 +package isabelle.vscode
    4.11 +
    4.12 +
    4.13 +import isabelle._
    4.14 +
    4.15 +import java.io.{File => JFile}
    4.16 +
    4.17 +
    4.18 +class Preview_Panel(resources: VSCode_Resources)
    4.19 +{
    4.20 +  private val pending = Synchronized(Map.empty[JFile, Int])
    4.21 +
    4.22 +  def request(file: JFile, column: Int): Unit =
    4.23 +    pending.change(map => map + (file -> column))
    4.24 +
    4.25 +  def flush(channel: Channel): Boolean =
    4.26 +  {
    4.27 +    pending.change_result(map =>
    4.28 +    {
    4.29 +      val map1 =
    4.30 +        (map /: map.iterator)({ case (m, (file, column)) =>
    4.31 +          resources.get_model(file) match {
    4.32 +            case Some(model) =>
    4.33 +              val snapshot = model.snapshot()
    4.34 +              if (snapshot.is_outdated) m
    4.35 +              else {
    4.36 +                val (label, content) = make_preview(model, snapshot)
    4.37 +                channel.write(Protocol.Preview_Response(file, column, label, content))
    4.38 +                m - file
    4.39 +              }
    4.40 +            case None => m - file
    4.41 +          }
    4.42 +        })
    4.43 +      (map1.nonEmpty, map1)
    4.44 +    })
    4.45 +  }
    4.46 +
    4.47 +  def make_preview(model: Document_Model, snapshot: Document.Snapshot): (String, String) =
    4.48 +  {
    4.49 +    val label = "Preview " + quote(model.node_name.toString)
    4.50 +    val content =
    4.51 +      HTML.output_document(
    4.52 +        List(HTML.style(HTML.fonts_css()), HTML.style_file(Url.print_file(HTML.isabelle_css.file))),
    4.53 +        List(
    4.54 +          HTML.chapter("Theory " + quote(model.node_name.theory_base_name)),
    4.55 +          HTML.source(Present.theory_document(snapshot))),
    4.56 +        css = "")
    4.57 +    (label, content)
    4.58 +  }
    4.59 +}
     5.1 --- a/src/Tools/VSCode/src/server.scala	Fri Jun 16 20:44:36 2017 +0200
     5.2 +++ b/src/Tools/VSCode/src/server.scala	Fri Jun 16 21:04:39 2017 +0200
     5.3 @@ -181,17 +181,17 @@
     5.4  
     5.5    /* preview */
     5.6  
     5.7 -  private lazy val preview = new Preview(resources)
     5.8 +  private lazy val preview_panel = new Preview_Panel(resources)
     5.9  
    5.10    private lazy val delay_preview: Standard_Thread.Delay =
    5.11      Standard_Thread.delay_last(options.seconds("vscode_output_delay"), channel.Error_Logger)
    5.12      {
    5.13 -      if (preview.flush(channel)) delay_preview.invoke()
    5.14 +      if (preview_panel.flush(channel)) delay_preview.invoke()
    5.15      }
    5.16  
    5.17    private def request_preview(file: JFile, column: Int)
    5.18    {
    5.19 -    preview.request(file, column)
    5.20 +    preview_panel.request(file, column)
    5.21      delay_preview.invoke()
    5.22    }
    5.23  
    5.24 @@ -400,10 +400,10 @@
    5.25            case Protocol.GotoDefinition(id, node_pos) => goto_definition(id, node_pos)
    5.26            case Protocol.DocumentHighlights(id, node_pos) => document_highlights(id, node_pos)
    5.27            case Protocol.Caret_Update(caret) => update_caret(caret)
    5.28 -          case Protocol.State_Init(()) => State.init(server)
    5.29 -          case Protocol.State_Exit(id) => State.exit(id)
    5.30 -          case Protocol.State_Locate(id) => State.locate(id)
    5.31 -          case Protocol.State_Update(id) => State.update(id)
    5.32 +          case Protocol.State_Init(()) => State_Panel.init(server)
    5.33 +          case Protocol.State_Exit(id) => State_Panel.exit(id)
    5.34 +          case Protocol.State_Locate(id) => State_Panel.locate(id)
    5.35 +          case Protocol.State_Update(id) => State_Panel.update(id)
    5.36            case Protocol.Preview_Request(file, column) => request_preview(file, column)
    5.37            case Protocol.Symbols_Request(()) => channel.write(Protocol.Symbols())
    5.38            case _ => log("### IGNORED")
     6.1 --- a/src/Tools/VSCode/src/state.scala	Fri Jun 16 20:44:36 2017 +0200
     6.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.3 @@ -1,118 +0,0 @@
     6.4 -/*  Title:      Tools/VSCode/src/state.scala
     6.5 -    Author:     Makarius
     6.6 -
     6.7 -Show proof state.
     6.8 -*/
     6.9 -
    6.10 -package isabelle.vscode
    6.11 -
    6.12 -
    6.13 -import isabelle._
    6.14 -
    6.15 -
    6.16 -object State
    6.17 -{
    6.18 -  private val make_id = Counter.make()
    6.19 -  private val instances = Synchronized(Map.empty[Counter.ID, State])
    6.20 -
    6.21 -  def init(server: Server)
    6.22 -  {
    6.23 -    val instance = new State(server)
    6.24 -    instances.change(_ + (instance.id -> instance))
    6.25 -    instance.init()
    6.26 -  }
    6.27 -
    6.28 -  def exit(id: Counter.ID)
    6.29 -  {
    6.30 -    instances.change(map =>
    6.31 -      map.get(id) match {
    6.32 -        case None => map
    6.33 -        case Some(instance) => instance.exit(); map - id
    6.34 -      })
    6.35 -  }
    6.36 -
    6.37 -  def locate(id: Counter.ID): Unit =
    6.38 -    instances.value.get(id).foreach(state =>
    6.39 -      state.server.editor.send_dispatcher(state.locate()))
    6.40 -
    6.41 -  def update(id: Counter.ID): Unit =
    6.42 -    instances.value.get(id).foreach(state =>
    6.43 -      state.server.editor.send_dispatcher(state.update()))
    6.44 -}
    6.45 -
    6.46 -
    6.47 -class State private(val server: Server)
    6.48 -{
    6.49 -  /* output */
    6.50 -
    6.51 -  val id: Counter.ID = State.make_id()
    6.52 -
    6.53 -  private def output(content: String): Unit =
    6.54 -    server.channel.write(Protocol.State_Output(id, content))
    6.55 -
    6.56 -
    6.57 -  /* query operation */
    6.58 -
    6.59 -  private val print_state =
    6.60 -    new Query_Operation(server.editor, (), "print_state", _ => (),
    6.61 -      (snapshot, results, body) =>
    6.62 -        {
    6.63 -          val text = server.resources.output_pretty_message(Pretty.separate(body))
    6.64 -          val content =
    6.65 -            HTML.output_document(
    6.66 -              List(HTML.style(HTML.fonts_css()),
    6.67 -                HTML.style_file(Url.print_file(HTML.isabelle_css.file))),
    6.68 -              List(
    6.69 -                HTML.chapter("Proof state"),
    6.70 -                HTML.source(text)),
    6.71 -              css = "")
    6.72 -          output(content)
    6.73 -        })
    6.74 -
    6.75 -  def locate() { print_state.locate_query() }
    6.76 -
    6.77 -  def update()
    6.78 -  {
    6.79 -    server.editor.current_node_snapshot(()) match {
    6.80 -      case Some(snapshot) =>
    6.81 -        (server.editor.current_command((), snapshot), print_state.get_location) match {
    6.82 -          case (Some(command1), Some(command2)) if command1.id == command2.id =>
    6.83 -          case _ => print_state.apply_query(Nil)
    6.84 -        }
    6.85 -      case None =>
    6.86 -    }
    6.87 -  }
    6.88 -
    6.89 -
    6.90 -  /* auto update */
    6.91 -
    6.92 -  private val auto_update_enabled = Synchronized(true)
    6.93 -
    6.94 -  def set_auto_update(b: Boolean) { auto_update_enabled.change(_ => b); if (b) update() }
    6.95 -
    6.96 -  def auto_update(): Unit = if (auto_update_enabled.value) update()
    6.97 -
    6.98 -
    6.99 -  /* main */
   6.100 -
   6.101 -  private val main =
   6.102 -    Session.Consumer[Any](getClass.getName) {
   6.103 -      case changed: Session.Commands_Changed => if (changed.assignment) auto_update()
   6.104 -      case Session.Caret_Focus => auto_update()
   6.105 -    }
   6.106 -
   6.107 -  def init()
   6.108 -  {
   6.109 -    server.session.commands_changed += main
   6.110 -    server.session.caret_focus += main
   6.111 -    server.editor.send_wait_dispatcher { print_state.activate() }
   6.112 -    server.editor.send_dispatcher { auto_update() }
   6.113 -  }
   6.114 -
   6.115 -  def exit()
   6.116 -  {
   6.117 -    server.editor.send_wait_dispatcher { print_state.deactivate() }
   6.118 -    server.session.commands_changed -= main
   6.119 -    server.session.caret_focus -= main
   6.120 -  }
   6.121 -}
     7.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.2 +++ b/src/Tools/VSCode/src/state_panel.scala	Fri Jun 16 21:04:39 2017 +0200
     7.3 @@ -0,0 +1,118 @@
     7.4 +/*  Title:      Tools/VSCode/src/state_panel.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_Panel
    7.17 +{
    7.18 +  private val make_id = Counter.make()
    7.19 +  private val instances = Synchronized(Map.empty[Counter.ID, State_Panel])
    7.20 +
    7.21 +  def init(server: Server)
    7.22 +  {
    7.23 +    val instance = new State_Panel(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_Panel private(val server: Server)
    7.48 +{
    7.49 +  /* output */
    7.50 +
    7.51 +  val id: Counter.ID = State_Panel.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 +}