# HG changeset patch
# User wenzelm
# Date 1274956540 -7200
# Node ID 10ef4da1c314673919d05286a240615b505f394f
# Parent  d4697a30bd02ee011775e943eecd457b93bfe65b
indicate prospective properties;

diff -r d4697a30bd02 -r 10ef4da1c314 src/Pure/System/isabelle_process.scala
--- a/src/Pure/System/isabelle_process.scala	Thu May 27 12:34:30 2010 +0200
+++ b/src/Pure/System/isabelle_process.scala	Thu May 27 12:35:40 2010 +0200
@@ -161,7 +161,7 @@
     if (proc == 0) error("Cannot kill Isabelle: no process")
     else {
       try_close()
-      Thread.sleep(500)
+      Thread.sleep(500)  // FIXME property!?
       put_result(Kind.SIGNAL, "KILL")
       proc.destroy
       proc = null
@@ -391,7 +391,7 @@
     new Thread("isabelle: exit") {
       override def run() = {
         val rc = proc.waitFor()
-        Thread.sleep(300)
+        Thread.sleep(300)  // FIXME property!?
         put_result(Kind.SYSTEM, "Exit thread terminated")
         put_result(Kind.EXIT, rc.toString)
         rm_fifo()
diff -r d4697a30bd02 -r 10ef4da1c314 src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala	Thu May 27 12:34:30 2010 +0200
+++ b/src/Pure/System/isabelle_system.scala	Thu May 27 12:35:40 2010 +0200
@@ -215,12 +215,12 @@
               catch { case _: IOException => None }
             if (pid.isDefined) {
               var running = true
-              var count = 10
+              var count = 10   // FIXME property!?
               while (running && count > 0) {
                 if (execute(true, "kill", "-INT", "-" + pid.get).waitFor != 0)
                   running = false
                 else {
-                  Thread.sleep(100)
+                  Thread.sleep(100)   // FIXME property!?
                   if (!strict) count -= 1
                 }
               }
diff -r d4697a30bd02 -r 10ef4da1c314 src/Pure/System/session.scala
--- a/src/Pure/System/session.scala	Thu May 27 12:34:30 2010 +0200
+++ b/src/Pure/System/session.scala	Thu May 27 12:35:40 2010 +0200
@@ -263,7 +263,7 @@
     {
       val now = currentTime
       flush_time match {
-        case None => flush_time = Some(now + 100)
+        case None => flush_time = Some(now + 100)   // FIXME output_delay property
         case Some(time) => if (now >= time) flush()
       }
     }
diff -r d4697a30bd02 -r 10ef4da1c314 src/Tools/jEdit/src/jedit/document_model.scala
--- a/src/Tools/jEdit/src/jedit/document_model.scala	Thu May 27 12:34:30 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/document_model.scala	Thu May 27 12:35:40 2010 +0200
@@ -95,7 +95,7 @@
 
   private val edits_buffer = new mutable.ListBuffer[Text_Edit]   // owned by Swing thread
 
-  private val edits_delay = Swing_Thread.delay_last(300) {
+  private val edits_delay = Swing_Thread.delay_last(300) {  // FIXME input_delay property
     if (!edits_buffer.isEmpty) {
       val new_change = current_change().edit(session, edits_buffer.toList)
       edits_buffer.clear
diff -r d4697a30bd02 -r 10ef4da1c314 src/Tools/jEdit/src/jedit/document_view.scala
--- a/src/Tools/jEdit/src/jedit/document_view.scala	Thu May 27 12:34:30 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/document_view.scala	Thu May 27 12:35:40 2010 +0200
@@ -162,6 +162,7 @@
   /* (re)painting */
 
   private val update_delay = Swing_Thread.delay_first(500) { model.buffer.propertiesChanged() }
+  // FIXME update_delay property
 
   private def update_syntax(cmd: Command)
   {
diff -r d4697a30bd02 -r 10ef4da1c314 src/Tools/jEdit/src/jedit/output_dockable.scala
--- a/src/Tools/jEdit/src/jedit/output_dockable.scala	Thu May 27 12:34:30 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/output_dockable.scala	Thu May 27 12:35:40 2010 +0200
@@ -106,7 +106,7 @@
   /* resize */
 
   addComponentListener(new ComponentAdapter {
-    val delay = Swing_Thread.delay_last(500) { handle_resize() }
+    val delay = Swing_Thread.delay_last(500) { handle_resize() }  // FIXME update_delay property
     override def componentResized(e: ComponentEvent) { delay() }
   })