tuned signature;
authorwenzelm
Mon Aug 12 11:56:12 2013 +0200 (2013-08-12)
changeset 52973d5f7fa1498b7
parent 52972 8fd8e1c14988
child 52974 908e8a36e975
tuned signature;
src/Tools/jEdit/src/document_model.scala
src/Tools/jEdit/src/document_view.scala
src/Tools/jEdit/src/jedit_editor.scala
src/Tools/jEdit/src/plugin.scala
src/Tools/jEdit/src/theories_dockable.scala
src/Tools/jEdit/src/timing_dockable.scala
     1.1 --- a/src/Tools/jEdit/src/document_model.scala	Mon Aug 12 11:49:58 2013 +0200
     1.2 +++ b/src/Tools/jEdit/src/document_model.scala	Mon Aug 12 11:56:12 2013 +0200
     1.3 @@ -46,11 +46,11 @@
     1.4      }
     1.5    }
     1.6  
     1.7 -  def init(session: Session, buffer: Buffer, name: Document.Node.Name): Document_Model =
     1.8 +  def init(session: Session, buffer: Buffer, node_name: Document.Node.Name): Document_Model =
     1.9    {
    1.10      Swing_Thread.require()
    1.11      apply(buffer).map(_.deactivate)
    1.12 -    val model = new Document_Model(session, buffer, name)
    1.13 +    val model = new Document_Model(session, buffer, node_name)
    1.14      buffer.setProperty(key, model)
    1.15      model.activate()
    1.16      buffer.propertiesChanged
    1.17 @@ -59,7 +59,7 @@
    1.18  }
    1.19  
    1.20  
    1.21 -class Document_Model(val session: Session, val buffer: Buffer, val name: Document.Node.Name)
    1.22 +class Document_Model(val session: Session, val buffer: Buffer, val node_name: Document.Node.Name)
    1.23  {
    1.24    /* header */
    1.25  
    1.26 @@ -68,7 +68,7 @@
    1.27      Swing_Thread.require()
    1.28      JEdit_Lib.buffer_lock(buffer) {
    1.29        Exn.capture {
    1.30 -        PIDE.thy_load.check_thy_text(name, buffer.getSegment(0, buffer.getLength))
    1.31 +        PIDE.thy_load.check_thy_text(node_name, buffer.getSegment(0, buffer.getLength))
    1.32        } match {
    1.33          case Exn.Res(header) => header
    1.34          case Exn.Exn(exn) => Document.Node.bad_header(Exn.message(exn))
    1.35 @@ -131,10 +131,10 @@
    1.36      val text = JEdit_Lib.buffer_text(buffer)
    1.37      val perspective = node_perspective()
    1.38  
    1.39 -    List(session.header_edit(name, header),
    1.40 -      name -> Document.Node.Clear(),
    1.41 -      name -> Document.Node.Edits(List(Text.Edit.insert(0, text))),
    1.42 -      name -> perspective)
    1.43 +    List(session.header_edit(node_name, header),
    1.44 +      node_name -> Document.Node.Clear(),
    1.45 +      node_name -> Document.Node.Edits(List(Text.Edit.insert(0, text))),
    1.46 +      node_name -> perspective)
    1.47    }
    1.48  
    1.49    def node_edits(perspective: Document.Node.Perspective_Text, text_edits: List[Text.Edit])
    1.50 @@ -144,9 +144,9 @@
    1.51  
    1.52      val header = node_header()
    1.53  
    1.54 -    List(session.header_edit(name, header),
    1.55 -      name -> Document.Node.Edits(text_edits),
    1.56 -      name -> perspective)
    1.57 +    List(session.header_edit(node_name, header),
    1.58 +      node_name -> Document.Node.Edits(text_edits),
    1.59 +      node_name -> perspective)
    1.60    }
    1.61  
    1.62  
    1.63 @@ -208,7 +208,7 @@
    1.64    def snapshot(): Document.Snapshot =
    1.65    {
    1.66      Swing_Thread.require()
    1.67 -    session.snapshot(name, pending_edits.snapshot())
    1.68 +    session.snapshot(node_name, pending_edits.snapshot())
    1.69    }
    1.70  
    1.71  
     2.1 --- a/src/Tools/jEdit/src/document_view.scala	Mon Aug 12 11:49:58 2013 +0200
     2.2 +++ b/src/Tools/jEdit/src/document_view.scala	Mon Aug 12 11:56:12 2013 +0200
     2.3 @@ -197,7 +197,7 @@
     2.4                  val snapshot = model.snapshot()
     2.5  
     2.6                  if (changed.assignment ||
     2.7 -                    (changed.nodes.contains(model.name) &&
     2.8 +                    (changed.nodes.contains(model.node_name) &&
     2.9                       changed.commands.exists(snapshot.node.commands.contains)))
    2.10                    Swing_Thread.later { overview.delay_repaint.invoke() }
    2.11  
     3.1 --- a/src/Tools/jEdit/src/jedit_editor.scala	Mon Aug 12 11:49:58 2013 +0200
     3.2 +++ b/src/Tools/jEdit/src/jedit_editor.scala	Mon Aug 12 11:56:12 2013 +0200
     3.3 @@ -21,7 +21,7 @@
     3.4      Swing_Thread.require { jEdit.getActiveView() }
     3.5  
     3.6    def current_node(view: View): Option[Document.Node.Name] =
     3.7 -    Swing_Thread.require { PIDE.document_model(view.getBuffer).map(_.name) }
     3.8 +    Swing_Thread.require { PIDE.document_model(view.getBuffer).map(_.node_name) }
     3.9  
    3.10    def current_snapshot(view: View): Option[Document.Snapshot] =
    3.11      Swing_Thread.require { PIDE.document_model(view.getBuffer).map(_.snapshot()) }
    3.12 @@ -35,7 +35,7 @@
    3.13        val text_area = view.getTextArea
    3.14        PIDE.document_view(text_area) match {
    3.15          case Some(doc_view) =>
    3.16 -          val node = snapshot.version.nodes(doc_view.model.name)
    3.17 +          val node = snapshot.version.nodes(doc_view.model.node_name)
    3.18            node.command_at(text_area.getCaretPosition)
    3.19          case None => None
    3.20        }
     4.1 --- a/src/Tools/jEdit/src/plugin.scala	Mon Aug 12 11:49:58 2013 +0200
     4.2 +++ b/src/Tools/jEdit/src/plugin.scala	Mon Aug 12 11:56:12 2013 +0200
     4.3 @@ -97,7 +97,7 @@
     4.4                thy_load.buffer_node_name(buffer) match {
     4.5                  case Some(node_name) =>
     4.6                    document_model(buffer) match {
     4.7 -                    case Some(model) if model.name == node_name => (Nil, Some(model))
     4.8 +                    case Some(model) if model.node_name == node_name => (Nil, Some(model))
     4.9                      case _ =>
    4.10                        val model = Document_Model.init(session, buffer, node_name)
    4.11                        (model.init_edits(), Some(model))
    4.12 @@ -175,7 +175,7 @@
    4.13  
    4.14          val thys =
    4.15            for (buffer <- buffers; model <- PIDE.document_model(buffer))
    4.16 -            yield model.name
    4.17 +            yield model.node_name
    4.18  
    4.19          val thy_info = new Thy_Info(PIDE.thy_load)
    4.20          // FIXME avoid I/O in Swing thread!?!
     5.1 --- a/src/Tools/jEdit/src/theories_dockable.scala	Mon Aug 12 11:49:58 2013 +0200
     5.2 +++ b/src/Tools/jEdit/src/theories_dockable.scala	Mon Aug 12 11:56:12 2013 +0200
     5.3 @@ -98,7 +98,7 @@
     5.4        buffer <- JEdit_Lib.jedit_buffers
     5.5        model <- PIDE.document_model(buffer)
     5.6        if model.node_required
     5.7 -    } nodes_required += model.name
     5.8 +    } nodes_required += model.node_name
     5.9    }
    5.10    update_nodes_required()
    5.11  
     6.1 --- a/src/Tools/jEdit/src/timing_dockable.scala	Mon Aug 12 11:49:58 2013 +0200
     6.2 +++ b/src/Tools/jEdit/src/timing_dockable.scala	Mon Aug 12 11:56:12 2013 +0200
     6.3 @@ -165,7 +165,7 @@
     6.4      val name =
     6.5        Document_View(view.getTextArea) match {
     6.6          case None => Document.Node.Name.empty
     6.7 -        case Some(doc_view) => doc_view.model.name
     6.8 +        case Some(doc_view) => doc_view.model.node_name
     6.9        }
    6.10      val timing = nodes_timing.getOrElse(name, Protocol.empty_node_timing)
    6.11