equal
deleted
inserted
replaced
79 } |
79 } |
80 |
80 |
81 private val state = Synchronized(State()) // owned by GUI thread |
81 private val state = Synchronized(State()) // owned by GUI thread |
82 |
82 |
83 def get_models(): Map[Document.Node.Name, Document_Model] = state.value.models |
83 def get_models(): Map[Document.Node.Name, Document_Model] = state.value.models |
84 def get(name: Document.Node.Name): Option[Document_Model] = get_models.get(name) |
84 def get(name: Document.Node.Name): Option[Document_Model] = get_models().get(name) |
85 def get(buffer: JEditBuffer): Option[Buffer_Model] = state.value.buffer_models.get(buffer) |
85 def get(buffer: JEditBuffer): Option[Buffer_Model] = state.value.buffer_models.get(buffer) |
86 |
86 |
87 def document_blobs(): Document.Blobs = state.value.document_blobs |
87 def document_blobs(): Document.Blobs = state.value.document_blobs |
88 |
88 |
89 |
89 |
311 val preview_root = http_root + "/preview" |
311 val preview_root = http_root + "/preview" |
312 |
312 |
313 val preview = |
313 val preview = |
314 HTTP.get(preview_root, arg => |
314 HTTP.get(preview_root, arg => |
315 for { |
315 for { |
316 query <- Library.try_unprefix(preview_root + "?", arg.uri.toString).map(Url.decode(_)) |
316 query <- Library.try_unprefix(preview_root + "?", arg.uri.toString).map(Url.decode) |
317 name = Library.perhaps_unprefix(plain_text_prefix, query) |
317 name = Library.perhaps_unprefix(plain_text_prefix, query) |
318 model <- get(PIDE.resources.node_name(name)) |
318 model <- get(PIDE.resources.node_name(name)) |
319 } |
319 } |
320 yield { |
320 yield { |
321 val snapshot = model.await_stable_snapshot() |
321 val snapshot = model.await_stable_snapshot() |
346 val reparse = snapshot.node.load_commands_changed(doc_blobs) |
346 val reparse = snapshot.node.load_commands_changed(doc_blobs) |
347 val perspective = |
347 val perspective = |
348 if (hidden) Text.Perspective.empty |
348 if (hidden) Text.Perspective.empty |
349 else { |
349 else { |
350 val view_ranges = document_view_ranges(snapshot) |
350 val view_ranges = document_view_ranges(snapshot) |
351 val load_ranges = snapshot.commands_loading_ranges(PIDE.editor.visible_node(_)) |
351 val load_ranges = snapshot.commands_loading_ranges(PIDE.editor.visible_node) |
352 Text.Perspective(view_ranges ::: load_ranges) |
352 Text.Perspective(view_ranges ::: load_ranges) |
353 } |
353 } |
354 val overlays = PIDE.editor.node_overlays(node_name) |
354 val overlays = PIDE.editor.node_overlays(node_name) |
355 |
355 |
356 (reparse, Document.Node.Perspective(node_required, perspective, overlays)) |
356 (reparse, Document.Node.Perspective(node_required, perspective, overlays)) |
587 val edits = get_edits |
587 val edits = get_edits |
588 val (reparse, perspective) = node_perspective(doc_blobs, hidden) |
588 val (reparse, perspective) = node_perspective(doc_blobs, hidden) |
589 if (reparse || edits.nonEmpty || last_perspective != perspective) { |
589 if (reparse || edits.nonEmpty || last_perspective != perspective) { |
590 pending.clear |
590 pending.clear |
591 last_perspective = perspective |
591 last_perspective = perspective |
592 node_edits(node_header, edits, perspective) |
592 node_edits(node_header(), edits, perspective) |
593 } |
593 } |
594 else Nil |
594 else Nil |
595 } |
595 } |
596 |
596 |
597 def edit(edits: List[Text.Edit]): Unit = synchronized |
597 def edit(edits: List[Text.Edit]): Unit = synchronized |