src/Tools/VSCode/src/server.scala
changeset 64679 b2bf280b7e13
parent 64673 b5965890e54d
child 64682 7e119f32276a
     1.1 --- a/src/Tools/VSCode/src/server.scala	Wed Dec 28 11:28:31 2016 +0100
     1.2 +++ b/src/Tools/VSCode/src/server.scala	Wed Dec 28 16:45:00 2016 +0100
     1.3 @@ -88,7 +88,8 @@
     1.4  
     1.5    sealed case class State(
     1.6      session: Option[Session] = None,
     1.7 -    models: Map[String, Document_Model] = Map.empty)
     1.8 +    models: Map[String, Document_Model] = Map.empty,
     1.9 +    pending_output: Set[Document.Node.Name] = Set.empty)
    1.10  }
    1.11  
    1.12  class Server(
    1.13 @@ -109,11 +110,68 @@
    1.14    def rendering_offset(node_pos: Line.Node_Position): Option[(VSCode_Rendering, Text.Offset)] =
    1.15      for {
    1.16        model <- state.value.models.get(node_pos.name)
    1.17 -      rendering = model.rendering(options, text_length)
    1.18 +      rendering = model.rendering(options)
    1.19        offset <- model.doc.offset(node_pos.pos, text_length)
    1.20      } yield (rendering, offset)
    1.21  
    1.22  
    1.23 +  /* input from client */
    1.24 +
    1.25 +  private val delay_input =
    1.26 +    Standard_Thread.delay_last(options.seconds("editor_input_delay")) {
    1.27 +      state.change(st =>
    1.28 +        {
    1.29 +          val changed = (for { entry <- st.models.iterator if entry._2.changed } yield entry).toList
    1.30 +          val edits = for { (_, model) <- changed; edit <- model.node_edits(resources) } yield edit
    1.31 +          session.update(Document.Blobs.empty, edits)
    1.32 +          st.copy(
    1.33 +            models = (st.models /: changed)({ case (ms, (uri, m)) => ms + (uri -> m.unchanged) }))
    1.34 +        })
    1.35 +    }
    1.36 +
    1.37 +  def update_document(uri: String, text: String)
    1.38 +  {
    1.39 +    state.change(st =>
    1.40 +      {
    1.41 +        val node_name = resources.node_name(uri)
    1.42 +        val model = Document_Model(session, Line.Document(text), node_name, text_length)
    1.43 +        st.copy(models = st.models + (uri -> model))
    1.44 +      })
    1.45 +    delay_input.invoke()
    1.46 +  }
    1.47 +
    1.48 +
    1.49 +  /* output to client */
    1.50 +
    1.51 +  private val commands_changed =
    1.52 +    Session.Consumer[Session.Commands_Changed](getClass.getName) {
    1.53 +      case changed =>
    1.54 +        state.change(st => st.copy(pending_output = st.pending_output ++ changed.nodes))
    1.55 +        delay_output.invoke()
    1.56 +    }
    1.57 +
    1.58 +  private val delay_output =
    1.59 +    Standard_Thread.delay_last(options.seconds("editor_update_delay")) {
    1.60 +      state.change(st =>
    1.61 +        {
    1.62 +          val changed_iterator =
    1.63 +            for {
    1.64 +              node_name <- st.pending_output.iterator
    1.65 +              uri = node_name.node
    1.66 +              model <- st.models.get(uri)
    1.67 +              rendering = model.rendering(options)
    1.68 +              (diagnostics, model1) <- model.publish_diagnostics(rendering)
    1.69 +            } yield {
    1.70 +              channel.diagnostics(uri, rendering.diagnostics_output(diagnostics))
    1.71 +              (uri, model1)
    1.72 +            }
    1.73 +          st.copy(
    1.74 +            models = (st.models /: changed_iterator) { case (ms, (uri, m)) => ms + (uri -> m) },
    1.75 +            pending_output = Set.empty)
    1.76 +        })
    1.77 +    }
    1.78 +
    1.79 +
    1.80    /* init and exit */
    1.81  
    1.82    def init(id: Protocol.Id)
    1.83 @@ -156,6 +214,8 @@
    1.84          }
    1.85        session.phase_changed += session_phase
    1.86  
    1.87 +      session.commands_changed += commands_changed
    1.88 +
    1.89        session.start(receiver =>
    1.90          Isabelle_Process(options = options, logic = session_name, dirs = session_dirs,
    1.91            modes = modes, receiver = receiver))
    1.92 @@ -181,7 +241,10 @@
    1.93                case _ =>
    1.94              }
    1.95            session.phase_changed += session_phase
    1.96 +          session.commands_changed -= commands_changed
    1.97            session.stop()
    1.98 +          delay_input.revoke()
    1.99 +          delay_output.revoke()
   1.100            st.copy(session = None)
   1.101        })
   1.102    }
   1.103 @@ -192,35 +255,6 @@
   1.104    }
   1.105  
   1.106  
   1.107 -  /* document management */
   1.108 -
   1.109 -  private val delay_flush =
   1.110 -    Standard_Thread.delay_last(options.seconds("editor_input_delay")) {
   1.111 -      state.change(st =>
   1.112 -        {
   1.113 -          val models = st.models
   1.114 -          val changed = (for { entry <- models.iterator if entry._2.changed } yield entry).toList
   1.115 -          val edits = for { (_, model) <- changed; edit <- model.node_edits(resources) } yield edit
   1.116 -          val models1 =
   1.117 -            (models /: changed)({ case (m, (uri, model)) => m + (uri -> model.unchanged) })
   1.118 -
   1.119 -          session.update(Document.Blobs.empty, edits)
   1.120 -          st.copy(models = models1)
   1.121 -        })
   1.122 -    }
   1.123 -
   1.124 -  def update_document(uri: String, text: String)
   1.125 -  {
   1.126 -    state.change(st =>
   1.127 -      {
   1.128 -        val node_name = resources.node_name(uri)
   1.129 -        val model = Document_Model(session, Line.Document(text), node_name)
   1.130 -        st.copy(models = st.models + (uri -> model))
   1.131 -      })
   1.132 -    delay_flush.invoke()
   1.133 -  }
   1.134 -
   1.135 -
   1.136    /* hover */
   1.137  
   1.138    def hover(id: Protocol.Id, node_pos: Line.Node_Position)
   1.139 @@ -231,10 +265,9 @@
   1.140          info <- rendering.tooltip(Text.Range(offset, offset + 1))
   1.141        } yield {
   1.142          val doc = rendering.model.doc
   1.143 -        val start = doc.position(info.range.start, text_length)
   1.144 -        val stop = doc.position(info.range.stop, text_length)
   1.145 +        val range = doc.range(info.range, text_length)
   1.146          val s = Pretty.string_of(info.info, margin = rendering.tooltip_margin)
   1.147 -        (Line.Range(start, stop), List("```\n" + s + "\n```"))  // FIXME proper content format
   1.148 +        (range, List("```\n" + s + "\n```"))  // FIXME proper content format
   1.149        }
   1.150      channel.write(Protocol.Hover.reply(id, result))
   1.151    }