# HG changeset patch
# User wenzelm
# Date 1282327885 -7200
# Node ID 9d480f6a258934530b7f8f42ac600293b8b6d055
# Parent  f117ba49a59ca4f9fe7bf9b2db41267d95618ef4
tuned signatures;

diff -r f117ba49a59c -r 9d480f6a2589 src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Fri Aug 20 12:12:28 2010 +0200
+++ b/src/Pure/PIDE/document.scala	Fri Aug 20 20:11:25 2010 +0200
@@ -65,11 +65,11 @@
     def command_start(cmd: Command): Option[Text.Offset] =
       command_starts.find(_._1 == cmd).map(_._2)
 
-    def command_range(i: Text.Offset): Iterator[(Command, Text.Offset)] =
+    def command_range(i: Text.Offset = 0): Iterator[(Command, Text.Offset)] =
       command_starts dropWhile { case (cmd, start) => start + cmd.length <= i }
 
-    def command_range(i: Text.Offset, j: Text.Offset): Iterator[(Command, Text.Offset)] =
-      command_range(i) takeWhile { case (_, start) => start < j }
+    def command_range(range: Text.Range): Iterator[(Command, Text.Offset)] =
+      command_range(range.start) takeWhile { case (_, start) => start < range.stop }
 
     def command_at(i: Text.Offset): Option[(Command, Text.Offset)] =
     {
diff -r f117ba49a59c -r 9d480f6a2589 src/Pure/System/session.scala
--- a/src/Pure/System/session.scala	Fri Aug 20 12:12:28 2010 +0200
+++ b/src/Pure/System/session.scala	Fri Aug 20 20:11:25 2010 +0200
@@ -60,7 +60,7 @@
   /** main actor **/
 
   @volatile private var syntax = new Outer_Syntax(system.symbols)
-  def current_syntax: Outer_Syntax = syntax
+  def current_syntax(): Outer_Syntax = syntax
 
   @volatile private var global_state = Document.State.init
   private def change_state(f: Document.State => Document.State) { global_state = f(global_state) }
diff -r f117ba49a59c -r 9d480f6a2589 src/Pure/Thy/thy_syntax.scala
--- a/src/Pure/Thy/thy_syntax.scala	Fri Aug 20 12:12:28 2010 +0200
+++ b/src/Pure/Thy/thy_syntax.scala	Fri Aug 20 20:11:25 2010 +0200
@@ -84,7 +84,7 @@
             commands.iterator(first).takeWhile(_ != last).toList ::: List(last)
 
           val sources = range.flatMap(_.span.map(_.source))
-          val spans0 = parse_spans(session.current_syntax.scan(sources.mkString))
+          val spans0 = parse_spans(session.current_syntax().scan(sources.mkString))
 
           val (before_edit, spans1) =
             if (!spans0.isEmpty && first.is_command && first.span == spans0.head)
diff -r f117ba49a59c -r 9d480f6a2589 src/Tools/jEdit/src/jedit/document_model.scala
--- a/src/Tools/jEdit/src/jedit/document_model.scala	Fri Aug 20 12:12:28 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/document_model.scala	Fri Aug 20 20:11:25 2010 +0200
@@ -278,7 +278,7 @@
       var next_x = start
       for {
         (command, command_start) <-
-          snapshot.node.command_range(snapshot.revert(start), snapshot.revert(stop))
+          snapshot.node.command_range(snapshot.revert(Text.Range(start, stop)))
         markup <- snapshot.state(command).highlight
         val Text.Range(abs_start, abs_stop) = snapshot.convert(markup.range + command_start)
         if (abs_stop > start)
diff -r f117ba49a59c -r 9d480f6a2589 src/Tools/jEdit/src/jedit/isabelle_sidekick.scala
--- a/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala	Fri Aug 20 12:12:28 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala	Fri Aug 20 20:11:25 2010 +0200
@@ -72,7 +72,7 @@
     val start = buffer.getLineStartOffset(line)
     val text = buffer.getSegment(start, caret - start)
 
-    val completion = Isabelle.session.current_syntax.completion
+    val completion = Isabelle.session.current_syntax().completion
 
     completion.complete(text) match {
       case None => null
@@ -97,7 +97,7 @@
     val root = data.root
     val snapshot = Swing_Thread.now { model.snapshot() }  // FIXME cover all nodes (!??)
     for {
-      (command, command_start) <- snapshot.node.command_range(0)
+      (command, command_start) <- snapshot.node.command_range()
       if command.is_command && !stopped
     }
     {
@@ -128,7 +128,7 @@
 
     val root = data.root
     val snapshot = Swing_Thread.now { model.snapshot() }  // FIXME cover all nodes (!??)
-    for ((command, command_start) <- snapshot.node.command_range(0) if !stopped) {
+    for ((command, command_start) <- snapshot.node.command_range() if !stopped) {
       snapshot.state(command).markup_root.swing_tree(root)((node: Markup_Tree.Node[Any]) =>
           {
             val content = command.source(node.range).replace('\n', ' ')