tuned signatures;
authorwenzelm
Fri Aug 20 20:11:25 2010 +0200 (2010-08-20)
changeset 385699d480f6a2589
parent 38568 f117ba49a59c
child 38570 3fa11fb01f86
tuned signatures;
src/Pure/PIDE/document.scala
src/Pure/System/session.scala
src/Pure/Thy/thy_syntax.scala
src/Tools/jEdit/src/jedit/document_model.scala
src/Tools/jEdit/src/jedit/isabelle_sidekick.scala
     1.1 --- a/src/Pure/PIDE/document.scala	Fri Aug 20 12:12:28 2010 +0200
     1.2 +++ b/src/Pure/PIDE/document.scala	Fri Aug 20 20:11:25 2010 +0200
     1.3 @@ -65,11 +65,11 @@
     1.4      def command_start(cmd: Command): Option[Text.Offset] =
     1.5        command_starts.find(_._1 == cmd).map(_._2)
     1.6  
     1.7 -    def command_range(i: Text.Offset): Iterator[(Command, Text.Offset)] =
     1.8 +    def command_range(i: Text.Offset = 0): Iterator[(Command, Text.Offset)] =
     1.9        command_starts dropWhile { case (cmd, start) => start + cmd.length <= i }
    1.10  
    1.11 -    def command_range(i: Text.Offset, j: Text.Offset): Iterator[(Command, Text.Offset)] =
    1.12 -      command_range(i) takeWhile { case (_, start) => start < j }
    1.13 +    def command_range(range: Text.Range): Iterator[(Command, Text.Offset)] =
    1.14 +      command_range(range.start) takeWhile { case (_, start) => start < range.stop }
    1.15  
    1.16      def command_at(i: Text.Offset): Option[(Command, Text.Offset)] =
    1.17      {
     2.1 --- a/src/Pure/System/session.scala	Fri Aug 20 12:12:28 2010 +0200
     2.2 +++ b/src/Pure/System/session.scala	Fri Aug 20 20:11:25 2010 +0200
     2.3 @@ -60,7 +60,7 @@
     2.4    /** main actor **/
     2.5  
     2.6    @volatile private var syntax = new Outer_Syntax(system.symbols)
     2.7 -  def current_syntax: Outer_Syntax = syntax
     2.8 +  def current_syntax(): Outer_Syntax = syntax
     2.9  
    2.10    @volatile private var global_state = Document.State.init
    2.11    private def change_state(f: Document.State => Document.State) { global_state = f(global_state) }
     3.1 --- a/src/Pure/Thy/thy_syntax.scala	Fri Aug 20 12:12:28 2010 +0200
     3.2 +++ b/src/Pure/Thy/thy_syntax.scala	Fri Aug 20 20:11:25 2010 +0200
     3.3 @@ -84,7 +84,7 @@
     3.4              commands.iterator(first).takeWhile(_ != last).toList ::: List(last)
     3.5  
     3.6            val sources = range.flatMap(_.span.map(_.source))
     3.7 -          val spans0 = parse_spans(session.current_syntax.scan(sources.mkString))
     3.8 +          val spans0 = parse_spans(session.current_syntax().scan(sources.mkString))
     3.9  
    3.10            val (before_edit, spans1) =
    3.11              if (!spans0.isEmpty && first.is_command && first.span == spans0.head)
     4.1 --- a/src/Tools/jEdit/src/jedit/document_model.scala	Fri Aug 20 12:12:28 2010 +0200
     4.2 +++ b/src/Tools/jEdit/src/jedit/document_model.scala	Fri Aug 20 20:11:25 2010 +0200
     4.3 @@ -278,7 +278,7 @@
     4.4        var next_x = start
     4.5        for {
     4.6          (command, command_start) <-
     4.7 -          snapshot.node.command_range(snapshot.revert(start), snapshot.revert(stop))
     4.8 +          snapshot.node.command_range(snapshot.revert(Text.Range(start, stop)))
     4.9          markup <- snapshot.state(command).highlight
    4.10          val Text.Range(abs_start, abs_stop) = snapshot.convert(markup.range + command_start)
    4.11          if (abs_stop > start)
     5.1 --- a/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala	Fri Aug 20 12:12:28 2010 +0200
     5.2 +++ b/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala	Fri Aug 20 20:11:25 2010 +0200
     5.3 @@ -72,7 +72,7 @@
     5.4      val start = buffer.getLineStartOffset(line)
     5.5      val text = buffer.getSegment(start, caret - start)
     5.6  
     5.7 -    val completion = Isabelle.session.current_syntax.completion
     5.8 +    val completion = Isabelle.session.current_syntax().completion
     5.9  
    5.10      completion.complete(text) match {
    5.11        case None => null
    5.12 @@ -97,7 +97,7 @@
    5.13      val root = data.root
    5.14      val snapshot = Swing_Thread.now { model.snapshot() }  // FIXME cover all nodes (!??)
    5.15      for {
    5.16 -      (command, command_start) <- snapshot.node.command_range(0)
    5.17 +      (command, command_start) <- snapshot.node.command_range()
    5.18        if command.is_command && !stopped
    5.19      }
    5.20      {
    5.21 @@ -128,7 +128,7 @@
    5.22  
    5.23      val root = data.root
    5.24      val snapshot = Swing_Thread.now { model.snapshot() }  // FIXME cover all nodes (!??)
    5.25 -    for ((command, command_start) <- snapshot.node.command_range(0) if !stopped) {
    5.26 +    for ((command, command_start) <- snapshot.node.command_range() if !stopped) {
    5.27        snapshot.state(command).markup_root.swing_tree(root)((node: Markup_Tree.Node[Any]) =>
    5.28            {
    5.29              val content = command.source(node.range).replace('\n', ' ')