# HG changeset patch # User wenzelm # Date 1354634424 -3600 # Node ID 8cf33d605e81cf878f1c6316786a189d5219bb59 # Parent 40d5ec9149d50de118fae102b7f5978964e55af3# Parent 608265769ce02c594668dd4ced34b1f2bb8bb94d merged diff -r 40d5ec9149d5 -r 8cf33d605e81 src/Pure/System/session.scala --- a/src/Pure/System/session.scala Tue Dec 04 15:02:45 2012 +0100 +++ b/src/Pure/System/session.scala Tue Dec 04 16:20:24 2012 +0100 @@ -468,15 +468,6 @@ def edit(edits: List[Document.Edit_Text]) { session_actor !? Session.Raw_Edits(edits) } - def init_node(name: Document.Node.Name, - header: Document.Node.Header, perspective: Text.Perspective, text: String) - { - edit(List(header_edit(name, header), - name -> Document.Node.Clear(), - name -> Document.Node.Edits(List(Text.Edit.insert(0, text))), - name -> Document.Node.Perspective(perspective))) - } - def edit_node(name: Document.Node.Name, header: Document.Node.Header, perspective: Text.Perspective, text_edits: List[Text.Edit]) { diff -r 40d5ec9149d5 -r 8cf33d605e81 src/Tools/jEdit/src/document_model.scala --- a/src/Tools/jEdit/src/document_model.scala Tue Dec 04 15:02:45 2012 +0100 +++ b/src/Tools/jEdit/src/document_model.scala Tue Dec 04 16:20:24 2012 +0100 @@ -81,7 +81,7 @@ def buffer_range(): Text.Range = Text.Range(0, (buffer.getLength - 1) max 0) - def perspective(): Text.Perspective = + def node_perspective(): Text.Perspective = { Swing_Thread.require() Text.Perspective( @@ -92,7 +92,23 @@ } - /* pending text edits */ + /* initial edits */ + + def init_edits(): List[Document.Edit_Text] = + { + Swing_Thread.require() + val header = node_header() + val text = JEdit_Lib.buffer_text(buffer) + val perspective = node_perspective() + + List(session.header_edit(name, header), + name -> Document.Node.Clear(), + name -> Document.Node.Edits(List(Text.Edit.insert(0, text))), + name -> Document.Node.Perspective(perspective)) + } + + + /* pending edits */ private object pending_edits // owned by Swing thread { @@ -106,7 +122,7 @@ Swing_Thread.require() val edits = snapshot() - val new_perspective = perspective() + val new_perspective = node_perspective() if (!edits.isEmpty || last_perspective != new_perspective) { pending.clear last_perspective = new_perspective @@ -132,7 +148,7 @@ def init() { flush() - session.init_node(name, node_header(), perspective(), JEdit_Lib.buffer_text(buffer)) + session.edit(init_edits()) } def exit() @@ -194,7 +210,7 @@ private def activate() { buffer.addBufferListener(buffer_listener) - pending_edits.init() + pending_edits.flush() Token_Markup.refresh_buffer(buffer) } diff -r 40d5ec9149d5 -r 8cf33d605e81 src/Tools/jEdit/src/isabelle.scala --- a/src/Tools/jEdit/src/isabelle.scala Tue Dec 04 15:02:45 2012 +0100 +++ b/src/Tools/jEdit/src/isabelle.scala Tue Dec 04 16:20:24 2012 +0100 @@ -60,6 +60,27 @@ def decrease_font_size(view: View): Unit = change_font_size(view, i => i - ((i / 10) max 1)) + /* structured insert */ + + def insert_line_padding(text_area: JEditTextArea, text: String) + { + val buffer = text_area.getBuffer + JEdit_Lib.buffer_edit(buffer) { + val text1 = + if (text_area.getSelectionCount == 0) { + def pad(range: Text.Range): String = + if (JEdit_Lib.try_get_text(buffer, range) == Some("\n")) "" else "\n" + + val caret = JEdit_Lib.point_range(buffer, text_area.getCaretPosition) + val before_caret = JEdit_Lib.point_range(buffer, caret.start - 1) + pad(before_caret) + text + pad(caret) + } + else text + text_area.setSelectedText(text1) + } + } + + /* control styles */ def control_sub(text_area: JEditTextArea) diff -r 40d5ec9149d5 -r 8cf33d605e81 src/Tools/jEdit/src/plugin.scala --- a/src/Tools/jEdit/src/plugin.scala Tue Dec 04 15:02:45 2012 +0100 +++ b/src/Tools/jEdit/src/plugin.scala Tue Dec 04 16:20:24 2012 +0100 @@ -58,32 +58,44 @@ if doc_view.isDefined } yield doc_view.get - def exit_model(buffer: Buffer) + def exit_models(buffers: List[Buffer]) { - JEdit_Lib.swing_buffer_lock(buffer) { - JEdit_Lib.jedit_text_areas(buffer).foreach(Document_View.exit) - Document_Model.exit(buffer) - } + Swing_Thread.now { + buffers.foreach(buffer => + JEdit_Lib.buffer_lock(buffer) { + JEdit_Lib.jedit_text_areas(buffer).foreach(Document_View.exit) + Document_Model.exit(buffer) + }) + } } - def init_model(buffer: Buffer) + def init_models(buffers: List[Buffer]) { - JEdit_Lib.swing_buffer_lock(buffer) { - val opt_model = - JEdit_Lib.buffer_node_name(buffer) match { - case Some(node_name) => - document_model(buffer) match { - case Some(model) if model.name == node_name => Some(model) - case _ => Some(Document_Model.init(session, buffer, node_name)) + Swing_Thread.now { + val init_edits = + (List.empty[Document.Edit_Text] /: buffers) { case (edits, buffer) => + JEdit_Lib.buffer_lock(buffer) { + val (model_edits, opt_model) = + JEdit_Lib.buffer_node_name(buffer) match { + case Some(node_name) => + document_model(buffer) match { + case Some(model) if model.name == node_name => (Nil, Some(model)) + case _ => + val model = Document_Model.init(session, buffer, node_name) + (model.init_edits(), Some(model)) + } + case None => (Nil, None) + } + if (opt_model.isDefined) { + for (text_area <- JEdit_Lib.jedit_text_areas(buffer)) { + if (document_view(text_area).map(_.model) != opt_model) + Document_View.init(opt_model.get, text_area) + } } - case None => None + model_edits ::: edits + } } - if (opt_model.isDefined) { - for (text_area <- JEdit_Lib.jedit_text_areas(buffer)) { - if (document_view(text_area).map(_.model) != opt_model) - Document_View.init(opt_model.get, text_area) - } - } + PIDE.session.edit(init_edits) } } @@ -123,6 +135,12 @@ { /* theory files */ + private lazy val delay_init = + Swing_Thread.delay_last(PIDE.options.seconds("editor_load_delay")) + { + PIDE.init_models(JEdit_Lib.jedit_buffers().toList) + } + private lazy val delay_load = Swing_Thread.delay_last(PIDE.options.seconds("editor_load_delay")) { @@ -179,11 +197,11 @@ case Session.Ready => PIDE.session.global_options.event(Session.Global_Options(PIDE.options.value)) - JEdit_Lib.jedit_buffers.foreach(PIDE.init_model) + PIDE.init_models(JEdit_Lib.jedit_buffers().toList) Swing_Thread.later { delay_load.invoke() } case Session.Shutdown => - JEdit_Lib.jedit_buffers.foreach(PIDE.exit_model) + PIDE.exit_models(JEdit_Lib.jedit_buffers().toList) Swing_Thread.later { delay_load.revoke() } case _ => @@ -221,7 +239,7 @@ if msg.getWhat == BufferUpdate.LOADED || msg.getWhat == BufferUpdate.PROPERTIES_CHANGED => if (PIDE.session.is_ready) { val buffer = msg.getBuffer - if (buffer != null && !buffer.isLoading) PIDE.init_model(buffer) + if (buffer != null && !buffer.isLoading) delay_init.invoke() Swing_Thread.later { delay_load.invoke() } } @@ -289,7 +307,7 @@ PIDE.options.value.save_prefs() PIDE.session.phase_changed -= session_manager - JEdit_Lib.jedit_buffers.foreach(PIDE.exit_model) + PIDE.exit_models(JEdit_Lib.jedit_buffers().toList) PIDE.session.stop() } } diff -r 40d5ec9149d5 -r 8cf33d605e81 src/Tools/jEdit/src/sendback.scala --- a/src/Tools/jEdit/src/sendback.scala Tue Dec 04 15:02:45 2012 +0100 +++ b/src/Tools/jEdit/src/sendback.scala Tue Dec 04 16:20:24 2012 +0100 @@ -42,21 +42,9 @@ case None => } case _ => - JEdit_Lib.buffer_edit(buffer) { - val text1 = - if (props.exists(_ == Markup.PADDING_LINE) && - text_area.getSelectionCount == 0) - { - def pad(range: Text.Range): String = - if (JEdit_Lib.try_get_text(buffer, range) == Some("\n")) "" else "\n" - - val caret = JEdit_Lib.point_range(buffer, text_area.getCaretPosition) - val before_caret = JEdit_Lib.point_range(buffer, caret.start - 1) - pad(before_caret) + text + pad(caret) - } - else text - text_area.setSelectedText(text1) - } + if (props.exists(_ == Markup.PADDING_LINE)) + Isabelle.insert_line_padding(text_area, text) + else text_area.setSelectedText(text) } } }