# HG changeset patch
# User wenzelm
# Date 1273346725 -7200
# Node ID 40837a7b32a7c7aa5dc6793e6de3f9b6b56b5fb9
# Parent  c8ae87ce6e4d4d6015d7a2bbf0c71e32bafa3cd0
proper use of var stopped;

diff -r c8ae87ce6e4d -r 40837a7b32a7 src/Tools/jEdit/src/jedit/isabelle_sidekick.scala
--- a/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala	Sat May 08 21:17:42 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala	Sat May 08 21:25:25 2010 +0200
@@ -98,7 +98,7 @@
     val document = model.recent_document()
     for {
       (command, command_start) <- document.command_range(0)
-      if command.is_command && !is_stopped()
+      if command.is_command && !stopped
     }
     {
       val name = command.name
@@ -129,7 +129,7 @@
 
     val root = data.root
     val document = model.recent_document()
-    for ((command, command_start) <- document.command_range(0) if !is_stopped()) {
+    for ((command, command_start) <- document.command_range(0) if !stopped) {
       root.add(document.current_state(command).get.markup_root.swing_tree((node: Markup_Node) =>
           {
             val content = Pretty.str_of(List(XML.Text(command.source(node.start, node.stop))))