# HG changeset patch
# User wenzelm
# Date 1232489634 -3600
# Node ID 1b2995592bb94278c11f9b6db74d8fdaf92e0d3f
# Parent  722533c532dae33dcaa288d9344bb7bd4ce2af25
renamed getNextCommandContaining to find_command_at;
more de-camelization;

diff -r 722533c532da -r 1b2995592bb9 src/Tools/jEdit/src/jedit/TheoryView.scala
--- a/src/Tools/jEdit/src/jedit/TheoryView.scala	Tue Jan 20 22:55:45 2009 +0100
+++ b/src/Tools/jEdit/src/jedit/TheoryView.scala	Tue Jan 20 23:13:54 2009 +0100
@@ -107,7 +107,7 @@
 
   private val selected_state_controller = new CaretListener {
     override def caretUpdate(e: CaretEvent) = {
-      val cmd = prover.document.getNextCommandContaining(e.getDot)
+      val cmd = prover.document.find_command_at(e.getDot)
       if (cmd != null && cmd.start <= e.getDot &&
           Isabelle.prover_setup(buffer).get.selected_state != cmd)
         Isabelle.prover_setup(buffer).get.selected_state = cmd
@@ -193,7 +193,7 @@
     val saved_color = gfx.getColor
 
     val metrics = text_area.getPainter.getFontMetrics
-    var e = prover.document.getNextCommandContaining(from_current(start))
+    var e = prover.document.find_command_at(from_current(start))
 
     // encolor phase
     while (e != null && to_current(e.start) < end) {
diff -r 722533c532da -r 1b2995592bb9 src/Tools/jEdit/src/proofdocument/ProofDocument.scala
--- a/src/Tools/jEdit/src/proofdocument/ProofDocument.scala	Tue Jan 20 22:55:45 2009 +0100
+++ b/src/Tools/jEdit/src/proofdocument/ProofDocument.scala	Tue Jan 20 23:13:54 2009 +0100
@@ -235,7 +235,7 @@
     def next() = { val s = current.command ; current = s.last.next ; s }
   }
 
-  def getNextCommandContaining(pos: Int): Command = {
+  def find_command_at(pos: Int): Command = {
     for (cmd <- commands) { if (pos < cmd.stop) return cmd }
     return null
   }
@@ -246,7 +246,7 @@
     var first: Command = null
     var last: Command = null
 
-    for(t <- tokens(removed)) {
+    for (t <- tokens(removed)) {
       if (first == null)
         first = t.command
       if (t.command != last)
@@ -297,43 +297,43 @@
     else
       scan = first_token
 
-    var stopScan: Token = null
+    var stop_scan: Token = null
     if (stop != null) {
       if (stop == stop.command.first)
-        stopScan = stop
+        stop_scan = stop
       else
-        stopScan = stop.command.last.next
+        stop_scan = stop.command.last.next
     }
     else if (last != null)
-      stopScan = last.last.next
+      stop_scan = last.last.next
     else
-      stopScan = null
+      stop_scan = null
 
-    var cmdStart: Token = null
-    var cmdStop: Token = null
+    var cmd_start: Token = null
+    var cmd_stop: Token = null
     var overrun = false
     var finished = false
     while (scan != null && !finished) {
-      if (scan == stopScan) {
+      if (scan == stop_scan) {
         if (scan.kind == Token.Kind.COMMAND_START)
           finished = true
         else
           overrun = true
       }
 
-      if (scan.kind == Token.Kind.COMMAND_START && cmdStart != null && !finished) {
+      if (scan.kind == Token.Kind.COMMAND_START && cmd_start != null && !finished) {
         if (!overrun) {
-          added_commands = new Command(text, cmdStart, cmdStop) :: added_commands
-          cmdStart = scan
-          cmdStop = scan
+          added_commands = new Command(text, cmd_start, cmd_stop) :: added_commands
+          cmd_start = scan
+          cmd_stop = scan
         }
         else
           finished = true
       }
       else if (!finished) {
-        if (cmdStart == null)
-          cmdStart = scan
-        cmdStop = scan
+        if (cmd_start == null)
+          cmd_start = scan
+        cmd_stop = scan
       }
       if (overrun && !finished) {
         if (scan.command != last)
@@ -345,8 +345,8 @@
         scan = scan.next
     }
 
-    if (cmdStart != null)
-      added_commands = new Command(text, cmdStart, cmdStop) :: added_commands
+    if (cmd_start != null)
+      added_commands = new Command(text, cmd_start, cmd_stop) :: added_commands
 
     // relink commands
     added_commands = added_commands.reverse