src/Tools/VSCode/src/vscode_resources.scala
changeset 64708 dd7f1a7e03f4
parent 64707 7157685b71e3
child 64709 5e6566ab78bf
equal deleted inserted replaced
64707:7157685b71e3 64708:dd7f1a7e03f4
    27 
    27 
    28   /* internal state */
    28   /* internal state */
    29 
    29 
    30   sealed case class State(
    30   sealed case class State(
    31     models: Map[String, Document_Model] = Map.empty,
    31     models: Map[String, Document_Model] = Map.empty,
    32     pending_input: Set[Document.Node.Name] = Set.empty,
    32     pending_input: Set[String] = Set.empty,
    33     pending_output: Set[Document.Node.Name] = Set.empty)
    33     pending_output: Set[String] = Set.empty)
    34 }
    34 }
    35 
    35 
    36 class VSCode_Resources(
    36 class VSCode_Resources(
    37     val options: Options,
    37     val options: Options,
    38     val text_length: Text.Length,
    38     val text_length: Text.Length,
    62 
    62 
    63   def update_model(model: Document_Model)
    63   def update_model(model: Document_Model)
    64   {
    64   {
    65     state.change(st =>
    65     state.change(st =>
    66       st.copy(
    66       st.copy(
    67         models = st.models + (model.node_name.node -> model),
    67         models = st.models + (model.uri -> model),
    68         pending_input = st.pending_input + model.node_name))
    68         pending_input = st.pending_input + model.uri))
    69   }
    69   }
    70 
    70 
    71 
    71 
    72   /* pending input */
    72   /* pending input */
    73 
    73 
    75   {
    75   {
    76     state.change(st =>
    76     state.change(st =>
    77       {
    77       {
    78         val changed =
    78         val changed =
    79           (for {
    79           (for {
    80             node_name <- st.pending_input.iterator
    80             uri <- st.pending_input.iterator
    81             model <- st.models.get(node_name.node)
    81             model <- st.models.get(uri)
    82             res <- model.flush_edits
    82             res <- model.flush_edits
    83           } yield res).toList
    83           } yield res).toList
    84 
    84 
    85         session.update(Document.Blobs.empty, changed.flatMap(_._1))
    85         session.update(Document.Blobs.empty, changed.flatMap(_._1))
    86         st.copy(
    86         st.copy(
    90   }
    90   }
    91 
    91 
    92 
    92 
    93   /* pending output */
    93   /* pending output */
    94 
    94 
    95   def update_output(changed_nodes: Set[Document.Node.Name]): Unit =
    95   def update_output(changed_nodes: List[String]): Unit =
    96     state.change(st => st.copy(pending_output = st.pending_output ++ changed_nodes))
    96     state.change(st => st.copy(pending_output = st.pending_output ++ changed_nodes))
    97 
    97 
    98   def flush_output(channel: Channel)
    98   def flush_output(channel: Channel)
    99   {
    99   {
   100     state.change(st =>
   100     state.change(st =>
   101       {
   101       {
   102         val changed_iterator =
   102         val changed_iterator =
   103           for {
   103           for {
   104             node_name <- st.pending_output.iterator
   104             uri <- st.pending_output.iterator
   105             model <- st.models.get(node_name.node)
   105             model <- st.models.get(uri)
   106             rendering = model.rendering()
   106             rendering = model.rendering()
   107             (diagnostics, model1) <- model.publish_diagnostics(rendering)
   107             (diagnostics, model1) <- model.publish_diagnostics(rendering)
   108           } yield {
   108           } yield {
   109             channel.diagnostics(model1.uri, rendering.diagnostics_output(diagnostics))
   109             channel.diagnostics(model1.uri, rendering.diagnostics_output(diagnostics))
   110             model1
   110             model1