# HG changeset patch
# User huffman
# Date 1289571089 28800
# Node ID 094e5d1f5bafb3d16cddcceb8c8fda44805c197e
# Parent  638943ad5bdce12640db4c42266fda8a79d813ba# Parent  f9057eca82f197a06cfd6ec73e093cd6bdcaf35f
merged

diff -r 638943ad5bdc -r 094e5d1f5baf doc-src/IsarRef/Thy/Framework.thy
--- a/doc-src/IsarRef/Thy/Framework.thy	Fri Nov 12 06:05:26 2010 -0800
+++ b/doc-src/IsarRef/Thy/Framework.thy	Fri Nov 12 06:11:29 2010 -0800
@@ -649,25 +649,25 @@
 theorem True
 proof
 (*>*)
-  txt_raw {* \begin{minipage}[t]{0.4\textwidth} *}
+  txt_raw {* \begin{minipage}[t]{0.45\textwidth} *}
   {
     fix x
     have "B x" sorry %noproof
   }
   note `\<And>x. B x`
-  txt_raw {* \end{minipage}\quad\begin{minipage}[t]{0.4\textwidth} *}(*<*)next(*>*)
+  txt_raw {* \end{minipage}\quad\begin{minipage}[t]{0.45\textwidth} *}(*<*)next(*>*)
   {
     assume A
     have B sorry %noproof
   }
   note `A \<Longrightarrow> B`
-  txt_raw {* \end{minipage}\\[3ex]\begin{minipage}[t]{0.4\textwidth} *}(*<*)next(*>*)
+  txt_raw {* \end{minipage}\\[3ex]\begin{minipage}[t]{0.45\textwidth} *}(*<*)next(*>*)
   {
     def x \<equiv> a
     have "B x" sorry %noproof
   }
   note `B a`
-  txt_raw {* \end{minipage}\quad\begin{minipage}[t]{0.4\textwidth} *}(*<*)next(*>*)
+  txt_raw {* \end{minipage}\quad\begin{minipage}[t]{0.45\textwidth} *}(*<*)next(*>*)
   {
     obtain x where "A x" sorry %noproof
     have B sorry %noproof
diff -r 638943ad5bdc -r 094e5d1f5baf doc-src/IsarRef/Thy/document/Framework.tex
--- a/doc-src/IsarRef/Thy/document/Framework.tex	Fri Nov 12 06:05:26 2010 -0800
+++ b/doc-src/IsarRef/Thy/document/Framework.tex	Fri Nov 12 06:11:29 2010 -0800
@@ -758,7 +758,7 @@
 %
 \isatagproof
 %
-\begin{minipage}[t]{0.4\textwidth}
+\begin{minipage}[t]{0.45\textwidth}
 \ \ \isacommand{{\isaliteral{7B}{\isacharbraceleft}}}\isamarkupfalse%
 \isanewline
 \ \ \ \ \isacommand{fix}\isamarkupfalse%
@@ -796,7 +796,7 @@
 \isanewline
 \ \ \isacommand{note}\isamarkupfalse%
 \ {\isaliteral{60}{\isacharbackquoteopen}}{\isaliteral{5C3C416E643E}{\isasymAnd}}x{\isaliteral{2E}{\isachardot}}\ B\ x{\isaliteral{60}{\isacharbackquoteclose}}%
-\end{minipage}\quad\begin{minipage}[t]{0.4\textwidth}
+\end{minipage}\quad\begin{minipage}[t]{0.45\textwidth}
 \ \ \isacommand{{\isaliteral{7B}{\isacharbraceleft}}}\isamarkupfalse%
 \isanewline
 \ \ \ \ \isacommand{assume}\isamarkupfalse%
@@ -834,7 +834,7 @@
 \isanewline
 \ \ \isacommand{note}\isamarkupfalse%
 \ {\isaliteral{60}{\isacharbackquoteopen}}A\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ B{\isaliteral{60}{\isacharbackquoteclose}}%
-\end{minipage}\\[3ex]\begin{minipage}[t]{0.4\textwidth}
+\end{minipage}\\[3ex]\begin{minipage}[t]{0.45\textwidth}
 \ \ \isacommand{{\isaliteral{7B}{\isacharbraceleft}}}\isamarkupfalse%
 \isanewline
 \ \ \ \ \isacommand{def}\isamarkupfalse%
@@ -872,7 +872,7 @@
 \isanewline
 \ \ \isacommand{note}\isamarkupfalse%
 \ {\isaliteral{60}{\isacharbackquoteopen}}B\ a{\isaliteral{60}{\isacharbackquoteclose}}%
-\end{minipage}\quad\begin{minipage}[t]{0.4\textwidth}
+\end{minipage}\quad\begin{minipage}[t]{0.45\textwidth}
 \ \ \isacommand{{\isaliteral{7B}{\isacharbraceleft}}}\isamarkupfalse%
 \isanewline
 \ \ \ \ \isacommand{obtain}\isamarkupfalse%
diff -r 638943ad5bdc -r 094e5d1f5baf lib/scripts/run-polyml
--- a/lib/scripts/run-polyml	Fri Nov 12 06:05:26 2010 -0800
+++ b/lib/scripts/run-polyml	Fri Nov 12 06:11:29 2010 -0800
@@ -47,7 +47,7 @@
   EXIT="fun exit 0 = (OS.Process.exit OS.Process.success): unit | exit _ = OS.Process.exit OS.Process.failure;"
 else
   check_file "$INFILE"
-  INIT="(Signal.signal (2, Signal.SIG_HANDLE (fn _ => Process.interruptConsoleProcesses ())); PolyML.SaveState.loadState \"$INFILE\" handle Fail msg => (TextIO.output (TextIO.stdErr, msg ^ \"\\n\"); OS.Process.exit OS.Process.failure));"
+  INIT="(Signal.signal (2, Signal.SIG_HANDLE (fn _ => Process.interruptConsoleProcesses ())); PolyML.SaveState.loadState \"$INFILE\" handle Fail msg => (TextIO.output (TextIO.stdErr, msg ^ \": $INFILE\\n\"); OS.Process.exit OS.Process.failure));"
   EXIT=""
 fi
 
@@ -78,3 +78,5 @@
 [ -n "$OUTFILE" -a -f "$OUTFILE" -a -n "$NOWRITE" ] && chmod -w "$OUTFILE"
 
 exit "$RC"
+
+#:wrap=soft:maxLineLen=100:
diff -r 638943ad5bdc -r 094e5d1f5baf src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Nov 12 06:05:26 2010 -0800
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Nov 12 06:11:29 2010 -0800
@@ -154,15 +154,13 @@
       prover :: avoid_too_many_local_threads thy n provers
     end
 
-fun num_processors () = try Thread.numProcessors () |> the_default 1
-
 (* The first ATP of the list is used by Auto Sledgehammer. Because of the low
    timeout, it makes sense to put SPASS first. *)
 fun default_provers_param_value ctxt =
   let val thy = ProofContext.theory_of ctxt in
     [spassN, eN, vampireN, sine_eN (* FIXME: , smtN *)]
     |> map_filter (remotify_prover_if_not_installed ctxt)
-    |> avoid_too_many_local_threads thy (num_processors ())
+    |> avoid_too_many_local_threads thy (Multithreading.max_threads_value ())
     |> space_implode " "
   end
 
diff -r 638943ad5bdc -r 094e5d1f5baf src/Pure/Concurrent/lazy.ML
--- a/src/Pure/Concurrent/lazy.ML	Fri Nov 12 06:05:26 2010 -0800
+++ b/src/Pure/Concurrent/lazy.ML	Fri Nov 12 06:11:29 2010 -0800
@@ -55,8 +55,9 @@
           (case expr of
             SOME e =>
               let
-                val res = restore_interrupts (fn () => Exn.capture e ()) ();
-                val _ = Future.fulfill_result x res;
+                val res0 = restore_interrupts (fn () => Exn.capture e ()) ();
+                val _ = Future.fulfill_result x res0;
+                val res = Future.join_result x;
                 (*semantic race: some other threads might see the same
                   interrupt, until there is a fresh start*)
                 val _ =
diff -r 638943ad5bdc -r 094e5d1f5baf src/Pure/General/exn.ML
--- a/src/Pure/General/exn.ML	Fri Nov 12 06:05:26 2010 -0800
+++ b/src/Pure/General/exn.ML	Fri Nov 12 06:11:29 2010 -0800
@@ -85,3 +85,6 @@
   handle EXCEPTIONS (exn :: _) => reraise exn;
 
 end;
+
+datatype illegal = Interrupt;
+
diff -r 638943ad5bdc -r 094e5d1f5baf src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Fri Nov 12 06:05:26 2010 -0800
+++ b/src/Pure/PIDE/document.ML	Fri Nov 12 06:11:29 2010 -0800
@@ -98,10 +98,12 @@
         |> Graph.default_node (name, empty_node)
         |> Graph.map_node name (fold edit_node edits))
   | edit_nodes (name, NONE) (Version nodes) =
-      Version (Graph.del_node name nodes);
+      Version (perhaps (try (Graph.del_node name)) nodes);
 
 fun put_node name node (Version nodes) =
-  Version (Graph.map_node name (K node) nodes);
+  Version (nodes
+    |> Graph.default_node (name, empty_node)
+    |> Graph.map_node name (K node));
 
 end;
 
diff -r 638943ad5bdc -r 094e5d1f5baf src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Fri Nov 12 06:05:26 2010 -0800
+++ b/src/Pure/PIDE/document.scala	Fri Nov 12 06:11:29 2010 -0800
@@ -17,7 +17,8 @@
 
   type ID = Long
 
-  object ID {
+  object ID
+  {
     def apply(id: ID): String = Markup.Long.apply(id)
     def unapply(s: String): Option[ID] = Markup.Long.unapply(s)
   }
@@ -34,11 +35,13 @@
 
   /* named nodes -- development graph */
 
-  type Node_Text_Edit = (String, List[Text.Edit])  // FIXME None: remove
+  type Edit[A] =
+   (String,  // node name
+    Option[List[A]])  // None: remove node, Some: edit content
 
-  type Edit[C] =
-   (String,  // node name
-    Option[List[(Option[C], Option[C])]])  // None: remove, Some: insert/remove commands
+  type Edit_Text = Edit[Text.Edit]
+  type Edit_Command = Edit[(Option[Command], Option[Command])]
+  type Edit_Command_ID = Edit[(Option[Command_ID], Option[Command_ID])]
 
   object Node
   {
@@ -133,8 +136,8 @@
 
   class Change(
     val previous: Future[Version],
-    val edits: List[Node_Text_Edit],
-    val result: Future[(List[Edit[Command]], Version)])
+    val edits: List[Edit_Text],
+    val result: Future[(List[Edit_Command], Version)])
   {
     val version: Future[Version] = result.map(_._2)
     def is_finished: Boolean = previous.is_finished && version.is_finished
@@ -267,8 +270,8 @@
       }
 
     def extend_history(previous: Future[Version],
-        edits: List[Node_Text_Edit],
-        result: Future[(List[Edit[Command]], Version)]): (Change, State) =
+        edits: List[Edit_Text],
+        result: Future[(List[Edit_Command], Version)]): (Change, State) =
     {
       val change = new Change(previous, edits, result)
       (change, copy(history = history + change))
@@ -284,9 +287,10 @@
       val stable = found_stable.get
       val latest = history.undo_list.head
 
+      // FIXME proper treatment of deleted nodes
       val edits =
         (pending_edits /: history.undo_list.takeWhile(_ != stable))((edits, change) =>
-            (for ((a, eds) <- change.edits if a == name) yield eds).flatten ::: edits)
+            (for ((a, Some(eds)) <- change.edits if a == name) yield eds).flatten ::: edits)
       lazy val reverse_edits = edits.reverse
 
       new Snapshot
diff -r 638943ad5bdc -r 094e5d1f5baf src/Pure/PIDE/isar_document.scala
--- a/src/Pure/PIDE/isar_document.scala	Fri Nov 12 06:05:26 2010 -0800
+++ b/src/Pure/PIDE/isar_document.scala	Fri Nov 12 06:11:29 2010 -0800
@@ -140,7 +140,7 @@
   /* document versions */
 
   def edit_version(old_id: Document.Version_ID, new_id: Document.Version_ID,
-      edits: List[Document.Edit[Document.Command_ID]])
+      edits: List[Document.Edit_Command_ID])
   {
     val arg =
       XML_Data.make_list(
diff -r 638943ad5bdc -r 094e5d1f5baf src/Pure/System/session.scala
--- a/src/Pure/System/session.scala	Fri Nov 12 06:05:26 2010 -0800
+++ b/src/Pure/System/session.scala	Fri Nov 12 06:11:29 2010 -0800
@@ -135,7 +135,7 @@
   def current_state(): Document.State = global_state.peek()
 
   private case object Interrupt_Prover
-  private case class Edit_Version(edits: List[Document.Node_Text_Edit])
+  private case class Edit_Version(edits: List[Document.Edit_Text])
   private case class Start(timeout: Int, args: List[String])
 
   private val (_, session_actor) = Simple_Thread.actor("session_actor", daemon = true)
@@ -289,7 +289,7 @@
 
   def interrupt() { session_actor ! Interrupt_Prover }
 
-  def edit_version(edits: List[Document.Node_Text_Edit]) { session_actor !? Edit_Version(edits) }
+  def edit_version(edits: List[Document.Edit_Text]) { session_actor !? Edit_Version(edits) }
 
   def snapshot(name: String, pending_edits: List[Text.Edit]): Document.Snapshot =
     global_state.peek().snapshot(name, pending_edits)
diff -r 638943ad5bdc -r 094e5d1f5baf src/Pure/Thy/thy_syntax.scala
--- a/src/Pure/Thy/thy_syntax.scala	Fri Nov 12 06:05:26 2010 -0800
+++ b/src/Pure/Thy/thy_syntax.scala	Fri Nov 12 06:11:29 2010 -0800
@@ -17,10 +17,7 @@
 
   object Structure
   {
-    sealed abstract class Entry
-    {
-      def length: Int
-    }
+    sealed abstract class Entry { def length: Int }
     case class Block(val name: String, val body: List[Entry]) extends Entry
     {
       val length: Int = (0 /: body)(_ + _.length)
@@ -103,7 +100,7 @@
   /** text edits **/
 
   def text_edits(session: Session, previous: Document.Version,
-      edits: List[Document.Node_Text_Edit]): (List[Document.Edit[Command]], Document.Version) =
+      edits: List[Document.Edit_Text]): (List[Document.Edit_Command], Document.Version) =
   {
     /* phase 1: edit individual command source */
 
@@ -175,23 +172,28 @@
     /* resulting document edits */
 
     {
-      val doc_edits = new mutable.ListBuffer[Document.Edit[Command]]
+      val doc_edits = new mutable.ListBuffer[Document.Edit_Command]
       var nodes = previous.nodes
 
-      for ((name, text_edits) <- edits) {
-        val commands0 = nodes(name).commands
-        val commands1 = edit_text(text_edits, commands0)
-        val commands2 = recover_spans(commands1)   // FIXME somewhat slow
+      edits foreach {
+        case (name, None) =>
+          doc_edits += (name -> None)
+          nodes -= name
+
+        case (name, Some(text_edits)) =>
+          val commands0 = nodes(name).commands
+          val commands1 = edit_text(text_edits, commands0)
+          val commands2 = recover_spans(commands1)   // FIXME somewhat slow
 
-        val removed_commands = commands0.iterator.filter(!commands2.contains(_)).toList
-        val inserted_commands = commands2.iterator.filter(!commands0.contains(_)).toList
+          val removed_commands = commands0.iterator.filter(!commands2.contains(_)).toList
+          val inserted_commands = commands2.iterator.filter(!commands0.contains(_)).toList
 
-        val cmd_edits =
-          removed_commands.reverse.map(cmd => (commands0.prev(cmd), None)) :::
-          inserted_commands.map(cmd => (commands2.prev(cmd), Some(cmd)))
+          val cmd_edits =
+            removed_commands.reverse.map(cmd => (commands0.prev(cmd), None)) :::
+            inserted_commands.map(cmd => (commands2.prev(cmd), Some(cmd)))
 
-        doc_edits += (name -> Some(cmd_edits))
-        nodes += (name -> new Document.Node(commands2))
+          doc_edits += (name -> Some(cmd_edits))
+          nodes += (name -> new Document.Node(commands2))
       }
       (doc_edits.toList, new Document.Version(session.new_id(), nodes))
     }
diff -r 638943ad5bdc -r 094e5d1f5baf src/Pure/library.scala
--- a/src/Pure/library.scala	Fri Nov 12 06:05:26 2010 -0800
+++ b/src/Pure/library.scala	Fri Nov 12 06:11:29 2010 -0800
@@ -82,6 +82,13 @@
       }
   }
 
+  def first_line(source: CharSequence): String =
+  {
+    val lines = chunks(source)
+    if (lines.hasNext) lines.next.toString
+    else ""
+  }
+
 
   /* simple dialogs */
 
diff -r 638943ad5bdc -r 094e5d1f5baf src/Tools/jEdit/src/jedit/document_model.scala
--- a/src/Tools/jEdit/src/jedit/document_model.scala	Fri Nov 12 06:05:26 2010 -0800
+++ b/src/Tools/jEdit/src/jedit/document_model.scala	Fri Nov 12 06:11:29 2010 -0800
@@ -116,18 +116,27 @@
     private val pending = new mutable.ListBuffer[Text.Edit]
     def snapshot(): List[Text.Edit] = pending.toList
 
-    private val delay_flush = Swing_Thread.delay_last(session.input_delay) {
-      if (!pending.isEmpty) session.edit_version(List((thy_name, flush())))
-    }
-
-    def flush(): List[Text.Edit] =
+    def flush(more_edits: Option[List[Text.Edit]]*)
     {
       Swing_Thread.require()
       val edits = snapshot()
       pending.clear
-      edits
+
+      val all_edits =
+        if (edits.isEmpty) more_edits.toList
+        else Some(edits) :: more_edits.toList
+      if (!all_edits.isEmpty) session.edit_version(all_edits.map((thy_name, _)))
     }
 
+    def init()
+    {
+      Swing_Thread.require()
+      flush(None, Some(List(Text.Edit.insert(0, Isabelle.buffer_text(buffer)))))
+    }
+
+    private val delay_flush =
+      Swing_Thread.delay_last(session.input_delay) { flush() }
+
     def +=(edit: Text.Edit)
     {
       Swing_Thread.require()
@@ -150,16 +159,23 @@
 
   private val buffer_listener: BufferListener = new BufferAdapter
   {
+    override def bufferLoaded(buffer: JEditBuffer)
+    {
+      pending_edits.init()
+    }
+
     override def contentInserted(buffer: JEditBuffer,
       start_line: Int, offset: Int, num_lines: Int, length: Int)
     {
-      pending_edits += Text.Edit.insert(offset, buffer.getText(offset, length))
+      if (!buffer.isLoading)
+        pending_edits += Text.Edit.insert(offset, buffer.getText(offset, length))
     }
 
     override def preContentRemoved(buffer: JEditBuffer,
       start_line: Int, offset: Int, num_lines: Int, removed_length: Int)
     {
-      pending_edits += Text.Edit.remove(offset, buffer.getText(offset, removed_length))
+      if (!buffer.isLoading)
+        pending_edits += Text.Edit.remove(offset, buffer.getText(offset, removed_length))
     }
   }
 
@@ -219,7 +235,7 @@
     buffer.setTokenMarker(token_marker)
     buffer.addBufferListener(buffer_listener)
     buffer.propertiesChanged()
-    pending_edits += Text.Edit.insert(0, buffer.getText(0, buffer.getLength))
+    pending_edits.init()
   }
 
   def refresh()
@@ -229,6 +245,7 @@
 
   def deactivate()
   {
+    pending_edits.flush()
     buffer.setTokenMarker(buffer.getMode.getTokenMarker)
     buffer.removeBufferListener(buffer_listener)
   }
diff -r 638943ad5bdc -r 094e5d1f5baf src/Tools/jEdit/src/jedit/isabelle_sidekick.scala
--- a/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala	Fri Nov 12 06:05:26 2010 -0800
+++ b/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala	Fri Nov 12 06:11:29 2010 -0800
@@ -24,10 +24,10 @@
 
 object Isabelle_Sidekick
 {
-  def int_to_pos(offset: Int): Position =
+  def int_to_pos(offset: Text.Offset): Position =
     new Position { def getOffset = offset; override def toString = offset.toString }
 
-  class Asset(name: String, start: Int, end: Int) extends IAsset
+  class Asset(name: String, start: Text.Offset, end: Text.Offset) extends IAsset
   {
     protected var _name = name
     protected var _start = int_to_pos(start)
@@ -79,7 +79,7 @@
   override def supportsCompletion = true
   override def canCompleteAnywhere = true
 
-  override def complete(pane: EditPane, caret: Int): SideKickCompletion =
+  override def complete(pane: EditPane, caret: Text.Offset): SideKickCompletion =
   {
     val buffer = pane.getBuffer
     Isabelle.swing_buffer_lock(buffer) {
@@ -116,12 +116,12 @@
   {
     val syntax = model.session.current_syntax()
 
-    def make_tree(offset: Int, entry: Structure.Entry): List[DefaultMutableTreeNode] =
+    def make_tree(offset: Text.Offset, entry: Structure.Entry): List[DefaultMutableTreeNode] =
       entry match {
         case Structure.Block(name, body) =>
           val node =
             new DefaultMutableTreeNode(
-              new Isabelle_Sidekick.Asset(name, offset, offset + entry.length))
+              new Isabelle_Sidekick.Asset(Library.first_line(name), offset, offset + entry.length))
           (offset /: body)((i, e) =>
             {
               make_tree(i, e) foreach (nd => node.add(nd))
@@ -137,8 +137,7 @@
         case _ => Nil
       }
 
-    val buffer = model.buffer
-    val text = Isabelle.buffer_lock(buffer) { buffer.getText(0, buffer.getLength) }
+    val text = Isabelle.buffer_text(model.buffer)
     val structure = Structure.parse_sections(syntax, "theory " + model.thy_name, text)
 
     make_tree(0, structure) foreach (node => data.root.add(node))
diff -r 638943ad5bdc -r 094e5d1f5baf src/Tools/jEdit/src/jedit/plugin.scala
--- a/src/Tools/jEdit/src/jedit/plugin.scala	Fri Nov 12 06:05:26 2010 -0800
+++ b/src/Tools/jEdit/src/jedit/plugin.scala	Fri Nov 12 06:11:29 2010 -0800
@@ -147,6 +147,9 @@
   def swing_buffer_lock[A](buffer: JEditBuffer)(body: => A): A =
     Swing_Thread.now { buffer_lock(buffer) { body } }
 
+  def buffer_text(buffer: JEditBuffer): String =
+    buffer_lock(buffer) { buffer.getText(0, buffer.getLength) }
+
 
   /* dockable windows */