--- a/doc-src/IsarRef/Thy/Framework.thy Wed Nov 10 18:45:48 2010 -0800
+++ b/doc-src/IsarRef/Thy/Framework.thy Fri Nov 12 12:57:02 2010 +0100
@@ -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
--- a/doc-src/IsarRef/Thy/document/Framework.tex Wed Nov 10 18:45:48 2010 -0800
+++ b/doc-src/IsarRef/Thy/document/Framework.tex Fri Nov 12 12:57:02 2010 +0100
@@ -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%
--- a/lib/scripts/run-polyml Wed Nov 10 18:45:48 2010 -0800
+++ b/lib/scripts/run-polyml Fri Nov 12 12:57:02 2010 +0100
@@ -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:
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Wed Nov 10 18:45:48 2010 -0800
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Nov 12 12:57:02 2010 +0100
@@ -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
--- a/src/Pure/Concurrent/lazy.ML Wed Nov 10 18:45:48 2010 -0800
+++ b/src/Pure/Concurrent/lazy.ML Fri Nov 12 12:57:02 2010 +0100
@@ -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 _ =
--- a/src/Pure/General/exn.ML Wed Nov 10 18:45:48 2010 -0800
+++ b/src/Pure/General/exn.ML Fri Nov 12 12:57:02 2010 +0100
@@ -85,3 +85,6 @@
handle EXCEPTIONS (exn :: _) => reraise exn;
end;
+
+datatype illegal = Interrupt;
+
--- a/src/Pure/PIDE/document.ML Wed Nov 10 18:45:48 2010 -0800
+++ b/src/Pure/PIDE/document.ML Fri Nov 12 12:57:02 2010 +0100
@@ -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;
--- a/src/Pure/PIDE/document.scala Wed Nov 10 18:45:48 2010 -0800
+++ b/src/Pure/PIDE/document.scala Fri Nov 12 12:57:02 2010 +0100
@@ -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
--- a/src/Pure/PIDE/isar_document.scala Wed Nov 10 18:45:48 2010 -0800
+++ b/src/Pure/PIDE/isar_document.scala Fri Nov 12 12:57:02 2010 +0100
@@ -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(
--- a/src/Pure/System/session.scala Wed Nov 10 18:45:48 2010 -0800
+++ b/src/Pure/System/session.scala Fri Nov 12 12:57:02 2010 +0100
@@ -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)
--- a/src/Pure/Thy/thy_syntax.scala Wed Nov 10 18:45:48 2010 -0800
+++ b/src/Pure/Thy/thy_syntax.scala Fri Nov 12 12:57:02 2010 +0100
@@ -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))
}
--- a/src/Pure/library.scala Wed Nov 10 18:45:48 2010 -0800
+++ b/src/Pure/library.scala Fri Nov 12 12:57:02 2010 +0100
@@ -82,6 +82,13 @@
}
}
+ def first_line(source: CharSequence): String =
+ {
+ val lines = chunks(source)
+ if (lines.hasNext) lines.next.toString
+ else ""
+ }
+
/* simple dialogs */
--- a/src/Tools/jEdit/src/jedit/document_model.scala Wed Nov 10 18:45:48 2010 -0800
+++ b/src/Tools/jEdit/src/jedit/document_model.scala Fri Nov 12 12:57:02 2010 +0100
@@ -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)
}
--- a/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala Wed Nov 10 18:45:48 2010 -0800
+++ b/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala Fri Nov 12 12:57:02 2010 +0100
@@ -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))
--- a/src/Tools/jEdit/src/jedit/plugin.scala Wed Nov 10 18:45:48 2010 -0800
+++ b/src/Tools/jEdit/src/jedit/plugin.scala Fri Nov 12 12:57:02 2010 +0100
@@ -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 */