# HG changeset patch # User wenzelm # Date 1376301372 -7200 # Node ID d5f7fa1498b787b0506d0318f2e476a0a609ded9 # Parent 8fd8e1c149886b399187bd91377f251a38d2b7c4 tuned signature; diff -r 8fd8e1c14988 -r d5f7fa1498b7 src/Tools/jEdit/src/document_model.scala --- a/src/Tools/jEdit/src/document_model.scala Mon Aug 12 11:49:58 2013 +0200 +++ b/src/Tools/jEdit/src/document_model.scala Mon Aug 12 11:56:12 2013 +0200 @@ -46,11 +46,11 @@ } } - def init(session: Session, buffer: Buffer, name: Document.Node.Name): Document_Model = + def init(session: Session, buffer: Buffer, node_name: Document.Node.Name): Document_Model = { Swing_Thread.require() apply(buffer).map(_.deactivate) - val model = new Document_Model(session, buffer, name) + val model = new Document_Model(session, buffer, node_name) buffer.setProperty(key, model) model.activate() buffer.propertiesChanged @@ -59,7 +59,7 @@ } -class Document_Model(val session: Session, val buffer: Buffer, val name: Document.Node.Name) +class Document_Model(val session: Session, val buffer: Buffer, val node_name: Document.Node.Name) { /* header */ @@ -68,7 +68,7 @@ Swing_Thread.require() JEdit_Lib.buffer_lock(buffer) { Exn.capture { - PIDE.thy_load.check_thy_text(name, buffer.getSegment(0, buffer.getLength)) + PIDE.thy_load.check_thy_text(node_name, buffer.getSegment(0, buffer.getLength)) } match { case Exn.Res(header) => header case Exn.Exn(exn) => Document.Node.bad_header(Exn.message(exn)) @@ -131,10 +131,10 @@ 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 -> perspective) + List(session.header_edit(node_name, header), + node_name -> Document.Node.Clear(), + node_name -> Document.Node.Edits(List(Text.Edit.insert(0, text))), + node_name -> perspective) } def node_edits(perspective: Document.Node.Perspective_Text, text_edits: List[Text.Edit]) @@ -144,9 +144,9 @@ val header = node_header() - List(session.header_edit(name, header), - name -> Document.Node.Edits(text_edits), - name -> perspective) + List(session.header_edit(node_name, header), + node_name -> Document.Node.Edits(text_edits), + node_name -> perspective) } @@ -208,7 +208,7 @@ def snapshot(): Document.Snapshot = { Swing_Thread.require() - session.snapshot(name, pending_edits.snapshot()) + session.snapshot(node_name, pending_edits.snapshot()) } diff -r 8fd8e1c14988 -r d5f7fa1498b7 src/Tools/jEdit/src/document_view.scala --- a/src/Tools/jEdit/src/document_view.scala Mon Aug 12 11:49:58 2013 +0200 +++ b/src/Tools/jEdit/src/document_view.scala Mon Aug 12 11:56:12 2013 +0200 @@ -197,7 +197,7 @@ val snapshot = model.snapshot() if (changed.assignment || - (changed.nodes.contains(model.name) && + (changed.nodes.contains(model.node_name) && changed.commands.exists(snapshot.node.commands.contains))) Swing_Thread.later { overview.delay_repaint.invoke() } diff -r 8fd8e1c14988 -r d5f7fa1498b7 src/Tools/jEdit/src/jedit_editor.scala --- a/src/Tools/jEdit/src/jedit_editor.scala Mon Aug 12 11:49:58 2013 +0200 +++ b/src/Tools/jEdit/src/jedit_editor.scala Mon Aug 12 11:56:12 2013 +0200 @@ -21,7 +21,7 @@ Swing_Thread.require { jEdit.getActiveView() } def current_node(view: View): Option[Document.Node.Name] = - Swing_Thread.require { PIDE.document_model(view.getBuffer).map(_.name) } + Swing_Thread.require { PIDE.document_model(view.getBuffer).map(_.node_name) } def current_snapshot(view: View): Option[Document.Snapshot] = Swing_Thread.require { PIDE.document_model(view.getBuffer).map(_.snapshot()) } @@ -35,7 +35,7 @@ val text_area = view.getTextArea PIDE.document_view(text_area) match { case Some(doc_view) => - val node = snapshot.version.nodes(doc_view.model.name) + val node = snapshot.version.nodes(doc_view.model.node_name) node.command_at(text_area.getCaretPosition) case None => None } diff -r 8fd8e1c14988 -r d5f7fa1498b7 src/Tools/jEdit/src/plugin.scala --- a/src/Tools/jEdit/src/plugin.scala Mon Aug 12 11:49:58 2013 +0200 +++ b/src/Tools/jEdit/src/plugin.scala Mon Aug 12 11:56:12 2013 +0200 @@ -97,7 +97,7 @@ thy_load.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 Some(model) if model.node_name == node_name => (Nil, Some(model)) case _ => val model = Document_Model.init(session, buffer, node_name) (model.init_edits(), Some(model)) @@ -175,7 +175,7 @@ val thys = for (buffer <- buffers; model <- PIDE.document_model(buffer)) - yield model.name + yield model.node_name val thy_info = new Thy_Info(PIDE.thy_load) // FIXME avoid I/O in Swing thread!?! diff -r 8fd8e1c14988 -r d5f7fa1498b7 src/Tools/jEdit/src/theories_dockable.scala --- a/src/Tools/jEdit/src/theories_dockable.scala Mon Aug 12 11:49:58 2013 +0200 +++ b/src/Tools/jEdit/src/theories_dockable.scala Mon Aug 12 11:56:12 2013 +0200 @@ -98,7 +98,7 @@ buffer <- JEdit_Lib.jedit_buffers model <- PIDE.document_model(buffer) if model.node_required - } nodes_required += model.name + } nodes_required += model.node_name } update_nodes_required() diff -r 8fd8e1c14988 -r d5f7fa1498b7 src/Tools/jEdit/src/timing_dockable.scala --- a/src/Tools/jEdit/src/timing_dockable.scala Mon Aug 12 11:49:58 2013 +0200 +++ b/src/Tools/jEdit/src/timing_dockable.scala Mon Aug 12 11:56:12 2013 +0200 @@ -165,7 +165,7 @@ val name = Document_View(view.getTextArea) match { case None => Document.Node.Name.empty - case Some(doc_view) => doc_view.model.name + case Some(doc_view) => doc_view.model.node_name } val timing = nodes_timing.getOrElse(name, Protocol.empty_node_timing)