diff -r 0e5ec80c352a -r c0c648911f1a src/Tools/jEdit/src/document_model.scala --- a/src/Tools/jEdit/src/document_model.scala Thu Jan 05 10:49:47 2017 +0100 +++ b/src/Tools/jEdit/src/document_model.scala Thu Jan 05 12:23:25 2017 +0100 @@ -119,7 +119,8 @@ } } - def node_perspective(hidden: Boolean, doc_blobs: Document.Blobs): (Boolean, Document.Node.Perspective_Text) = + def node_perspective(hidden: Boolean, doc_blobs: Document.Blobs) + : (Boolean, Document.Node.Perspective_Text) = { GUI_Thread.require {} @@ -132,17 +133,8 @@ range <- doc_view.perspective(snapshot).ranges } yield range - val load_ranges = - for { - cmd <- snapshot.node.load_commands - blob_name <- cmd.blobs_names - blob_buffer <- JEdit_Lib.jedit_buffer(blob_name) - if JEdit_Lib.jedit_text_areas(blob_buffer).nonEmpty - start <- snapshot.node.command_start(cmd) - range = snapshot.convert(cmd.proper_range + start) - } yield range - - val reparse = snapshot.node.load_commands.exists(_.blobs_changed(doc_blobs)) + val load_ranges = snapshot.commands_loading_ranges(PIDE.editor.visible_node(_)) + val reparse = snapshot.node.load_commands_changed(doc_blobs) (reparse, Document.Node.Perspective(node_required,