--- a/doc-src/TutorialI/ToyList/ToyList.thy Mon Aug 16 10:32:35 2010 +0200
+++ b/doc-src/TutorialI/ToyList/ToyList.thy Mon Aug 16 10:32:45 2010 +0200
@@ -105,6 +105,8 @@
When Isabelle prints a syntax error message, it refers to the HOL syntax as
the \textbf{inner syntax} and the enclosing theory language as the \textbf{outer syntax}.
+Comments\index{comment} must be in enclosed in \texttt{(* }and\texttt{ *)}.
+
\section{Evaluation}
\index{evaluation}
@@ -120,19 +122,10 @@
But we can go beyond mere functional programming and evaluate terms with
variables in them, executing functions symbolically: *}
-normal_form "rev (a # b # c # [])"
+value "rev (a # b # c # [])"
text{*\noindent yields @{term"c # b # a # []"}.
-Command \commdx{normal\protect\_form} works for arbitrary terms
-but can be slower than command \commdx{value},
-which is restricted to variable-free terms and executable functions.
-To appreciate the subtleties of evaluating terms with variables,
-try this one:
-*}
-normal_form "rev (a # b # c # xs)"
-
-text{*
\section{An Introductory Proof}
\label{sec:intro-proof}
--- a/doc-src/TutorialI/ToyList/document/ToyList.tex Mon Aug 16 10:32:35 2010 +0200
+++ b/doc-src/TutorialI/ToyList/document/ToyList.tex Mon Aug 16 10:32:45 2010 +0200
@@ -125,6 +125,8 @@
When Isabelle prints a syntax error message, it refers to the HOL syntax as
the \textbf{inner syntax} and the enclosing theory language as the \textbf{outer syntax}.
+Comments\index{comment} must be in enclosed in \texttt{(* }and\texttt{ *)}.
+
\section{Evaluation}
\index{evaluation}
@@ -142,20 +144,11 @@
variables in them, executing functions symbolically:%
\end{isamarkuptext}%
\isamarkuptrue%
-\isacommand{normal{\isacharunderscore}form}\isamarkupfalse%
+\isacommand{value}\isamarkupfalse%
\ {\isachardoublequoteopen}rev\ {\isacharparenleft}a\ {\isacharhash}\ b\ {\isacharhash}\ c\ {\isacharhash}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}{\isachardoublequoteclose}%
\begin{isamarkuptext}%
\noindent yields \isa{c\ {\isacharhash}\ b\ {\isacharhash}\ a\ {\isacharhash}\ {\isacharbrackleft}{\isacharbrackright}}.
-Command \commdx{normal\protect\_form} works for arbitrary terms
-but can be slower than command \commdx{value},
-which is restricted to variable-free terms and executable functions.
-To appreciate the subtleties of evaluating terms with variables,
-try this one:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{normal{\isacharunderscore}form}\isamarkupfalse%
-\ {\isachardoublequoteopen}rev\ {\isacharparenleft}a\ {\isacharhash}\ b\ {\isacharhash}\ c\ {\isacharhash}\ xs{\isacharparenright}{\isachardoublequoteclose}%
-\begin{isamarkuptext}%
+
\section{An Introductory Proof}
\label{sec:intro-proof}
--- a/doc-src/TutorialI/ToyList2/ToyList1 Mon Aug 16 10:32:35 2010 +0200
+++ b/doc-src/TutorialI/ToyList2/ToyList1 Mon Aug 16 10:32:45 2010 +0200
@@ -5,6 +5,7 @@
datatype 'a list = Nil ("[]")
| Cons 'a "'a list" (infixr "#" 65)
+(* This is the append function: *)
primrec app :: "'a list => 'a list => 'a list" (infixr "@" 65)
where
"[] @ ys = ys" |
--- a/doc-src/TutorialI/basics.tex Mon Aug 16 10:32:35 2010 +0200
+++ b/doc-src/TutorialI/basics.tex Mon Aug 16 10:32:45 2010 +0200
@@ -346,6 +346,5 @@
\begin{pgnote}
You can choose a different logic via the \pgmenu{Isabelle} $>$
-\pgmenu{Logics} menu. For example, you may want to work in the real
-numbers, an extension of HOL (see \S\ref{sec:real}).
+\pgmenu{Logics} menu.
\end{pgnote}
--- a/src/Pure/General/linear_set.scala Mon Aug 16 10:32:35 2010 +0200
+++ b/src/Pure/General/linear_set.scala Mon Aug 16 10:32:45 2010 +0200
@@ -48,6 +48,12 @@
def next(elem: A): Option[A] = rep.nexts.get(elem)
def prev(elem: A): Option[A] = rep.prevs.get(elem)
+ def get_after(hook: Option[A]): Option[A] =
+ hook match {
+ case None => rep.start
+ case Some(elem) => next(elem)
+ }
+
def insert_after(hook: Option[A], elem: A): Linear_Set[A] =
if (contains(elem)) throw new Linear_Set.Duplicate(elem.toString)
else
--- a/src/Pure/General/markup.ML Mon Aug 16 10:32:35 2010 +0200
+++ b/src/Pure/General/markup.ML Mon Aug 16 10:32:45 2010 +0200
@@ -6,6 +6,8 @@
signature MARKUP =
sig
+ val parse_int: string -> int
+ val print_int: int -> string
type T = string * Properties.T
val none: T
val is_none: T -> bool
@@ -109,8 +111,10 @@
val failedN: string val failed: T
val finishedN: string val finished: T
val disposedN: string val disposed: T
- val assignN: string val assign: T
- val editN: string val edit: string -> string -> T
+ val versionN: string
+ val execN: string
+ val assignN: string val assign: int -> T
+ val editN: string val edit: int -> int -> T
val pidN: string
val promptN: string val prompt: T
val readyN: string val ready: T
@@ -127,6 +131,16 @@
(** markup elements **)
+(* integers *)
+
+fun parse_int s =
+ (case Int.fromString s of
+ SOME i => i
+ | NONE => raise Fail ("Bad integer: " ^ quote s));
+
+val print_int = signed_string_of_int;
+
+
(* basic markup *)
type T = string * Properties.T;
@@ -142,7 +156,7 @@
fun markup_elem elem = (elem, (elem, []): T);
fun markup_string elem prop = (elem, fn s => (elem, [(prop, s)]): T);
-fun markup_int elem prop = (elem, fn i => (elem, [(prop, Int.toString i)]): T);
+fun markup_int elem prop = (elem, fn i => (elem, [(prop, print_int i)]): T);
(* name *)
@@ -315,10 +329,12 @@
(* interactive documents *)
-val (assignN, assign) = markup_elem "assign";
+val versionN = "version";
+val execN = "exec";
+val (assignN, assign) = markup_int "assign" versionN;
val editN = "edit";
-fun edit id state_id : T = (editN, [(idN, id), (stateN, state_id)]);
+fun edit cmd_id exec_id : T = (editN, [(idN, print_int cmd_id), (execN, print_int exec_id)]);
(* messages *)
--- a/src/Pure/General/markup.scala Mon Aug 16 10:32:35 2010 +0200
+++ b/src/Pure/General/markup.scala Mon Aug 16 10:32:45 2010 +0200
@@ -9,20 +9,41 @@
object Markup
{
+ /* integers */
+
+ object Int {
+ def apply(i: scala.Int): String = i.toString
+ def unapply(s: String): Option[scala.Int] =
+ try { Some(Integer.parseInt(s)) }
+ catch { case _: NumberFormatException => None }
+ }
+
+ object Long {
+ def apply(i: scala.Long): String = i.toString
+ def unapply(s: String): Option[scala.Long] =
+ try { Some(java.lang.Long.parseLong(s)) }
+ catch { case _: NumberFormatException => None }
+ }
+
+
/* property values */
def get_string(name: String, props: List[(String, String)]): Option[String] =
props.find(p => p._1 == name).map(_._2)
- def parse_int(s: String): Option[Int] =
- try { Some(Integer.parseInt(s)) }
- catch { case _: NumberFormatException => None }
-
- def get_int(name: String, props: List[(String, String)]): Option[Int] =
+ def get_long(name: String, props: List[(String, String)]): Option[scala.Long] =
{
get_string(name, props) match {
case None => None
- case Some(value) => parse_int(value)
+ case Some(Long(i)) => Some(i)
+ }
+ }
+
+ def get_int(name: String, props: List[(String, String)]): Option[scala.Int] =
+ {
+ get_string(name, props) match {
+ case None => None
+ case Some(Int(i)) => Some(i)
}
}
@@ -183,7 +204,9 @@
/* interactive documents */
- val Assign = Markup("assign", Nil)
+ val VERSION = "version"
+ val EXEC = "exec"
+ val ASSIGN = "assign"
val EDIT = "edit"
--- a/src/Pure/General/position.scala Mon Aug 16 10:32:35 2010 +0200
+++ b/src/Pure/General/position.scala Mon Aug 16 10:32:45 2010 +0200
@@ -18,7 +18,7 @@
def get_end_column(pos: T): Option[Int] = Markup.get_int(Markup.END_COLUMN, pos)
def get_end_offset(pos: T): Option[Int] = Markup.get_int(Markup.END_OFFSET, pos)
def get_file(pos: T): Option[String] = Markup.get_string(Markup.FILE, pos)
- def get_id(pos: T): Option[String] = Markup.get_string(Markup.ID, pos)
+ def get_id(pos: T): Option[Long] = Markup.get_long(Markup.ID, pos)
def get_range(pos: T): Option[(Int, Int)] =
(get_offset(pos), get_end_offset(pos)) match {
@@ -27,6 +27,6 @@
case (None, _) => None
}
- object Id { def unapply(pos: T): Option[String] = get_id(pos) }
+ object Id { def unapply(pos: T): Option[Long] = get_id(pos) }
object Range { def unapply(pos: T): Option[(Int, Int)] = get_range(pos) }
}
--- a/src/Pure/General/pretty.scala Mon Aug 16 10:32:35 2010 +0200
+++ b/src/Pure/General/pretty.scala Mon Aug 16 10:32:45 2010 +0200
@@ -16,29 +16,26 @@
object Block
{
- def apply(indent: Int, body: List[XML.Tree]): XML.Tree =
- XML.Elem(Markup(Markup.BLOCK, List((Markup.INDENT, indent.toString))), body)
+ def apply(i: Int, body: List[XML.Tree]): XML.Tree =
+ XML.Elem(Markup(Markup.BLOCK, List((Markup.INDENT, Markup.Int(i)))), body)
def unapply(tree: XML.Tree): Option[(Int, List[XML.Tree])] =
tree match {
- case XML.Elem(Markup(Markup.BLOCK, List((Markup.INDENT, indent))), body) =>
- Markup.parse_int(indent) match {
- case Some(i) => Some((i, body))
- case None => None
- }
+ case XML.Elem(
+ Markup(Markup.BLOCK, List((Markup.INDENT, Markup.Int(i)))), body) => Some((i, body))
case _ => None
}
}
object Break
{
- def apply(width: Int): XML.Tree =
- XML.Elem(Markup(Markup.BREAK, List((Markup.WIDTH, width.toString))),
- List(XML.Text(Symbol.spaces(width))))
+ def apply(w: Int): XML.Tree =
+ XML.Elem(
+ Markup(Markup.BREAK, List((Markup.WIDTH, Markup.Int(w)))), List(XML.Text(Symbol.spaces(w))))
def unapply(tree: XML.Tree): Option[Int] =
tree match {
- case XML.Elem(Markup(Markup.BREAK, List((Markup.WIDTH, width))), _) => Markup.parse_int(width)
+ case XML.Elem(Markup(Markup.BREAK, List((Markup.WIDTH, Markup.Int(w)))), _) => Some(w)
case _ => None
}
}
--- a/src/Pure/General/scan.scala Mon Aug 16 10:32:35 2010 +0200
+++ b/src/Pure/General/scan.scala Mon Aug 16 10:32:45 2010 +0200
@@ -285,8 +285,8 @@
val junk = many1(sym => !(symbols.is_blank(sym)))
val bad_delimiter =
- ("\"" | "`" | "{*" | "(*") ~ junk ^^ { case x ~ y => Token(Token.Kind.BAD_INPUT, x + y) }
- val bad = junk ^^ (x => Token(Token.Kind.BAD_INPUT, x))
+ ("\"" | "`" | "{*" | "(*") ~ junk ^^ { case x ~ y => Token(Token.Kind.UNPARSED, x + y) }
+ val bad = junk ^^ (x => Token(Token.Kind.UNPARSED, x))
/* tokens */
--- a/src/Pure/General/xml_data.scala Mon Aug 16 10:32:35 2010 +0200
+++ b/src/Pure/General/xml_data.scala Mon Aug 16 10:32:45 2010 +0200
@@ -15,6 +15,13 @@
class XML_Atom(s: String) extends Exception(s)
+ private def make_long_atom(i: Long): String = i.toString
+
+ private def dest_long_atom(s: String): Long =
+ try { java.lang.Long.parseLong(s) }
+ catch { case e: NumberFormatException => throw new XML_Atom(s) }
+
+
private def make_int_atom(i: Int): String = i.toString
private def dest_int_atom(s: String): Int =
@@ -71,6 +78,9 @@
}
+ def make_long(i: Long): XML.Body = make_string(make_long_atom(i))
+ def dest_long(ts: XML.Body): Long = dest_long_atom(dest_string(ts))
+
def make_int(i: Int): XML.Body = make_string(make_int_atom(i))
def dest_int(ts: XML.Body): Int = dest_int_atom(dest_string(ts))
--- a/src/Pure/IsaMakefile Mon Aug 16 10:32:35 2010 +0200
+++ b/src/Pure/IsaMakefile Mon Aug 16 10:32:45 2010 +0200
@@ -119,7 +119,6 @@
Isar/expression.ML \
Isar/generic_target.ML \
Isar/isar_cmd.ML \
- Isar/isar_document.ML \
Isar/isar_syn.ML \
Isar/keyword.ML \
Isar/local_defs.ML \
@@ -191,6 +190,7 @@
Syntax/type_ext.ML \
System/isabelle_process.ML \
System/isar.ML \
+ System/isar_document.ML \
System/session.ML \
Thy/html.ML \
Thy/latex.ML \
--- a/src/Pure/Isar/isar_document.ML Mon Aug 16 10:32:35 2010 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,296 +0,0 @@
-(* Title: Pure/Isar/isar_document.ML
- Author: Makarius
-
-Interactive Isar documents, which are structured as follows:
-
- - history: tree of documents (i.e. changes without merge)
- - document: graph of nodes (cf. theory files)
- - node: linear set of commands, potentially with proof structure
-*)
-
-structure Isar_Document: sig end =
-struct
-
-(* unique identifiers *)
-
-local
- val id_count = Synchronized.var "id" 0;
-in
- fun create_id () =
- Synchronized.change_result id_count
- (fn i =>
- let val i' = i + 1
- in ("i" ^ string_of_int i', i') end);
-end;
-
-fun err_dup kind id = error ("Duplicate " ^ kind ^ ": " ^ quote id);
-fun err_undef kind id = error ("Undefined " ^ kind ^ ": " ^ quote id);
-
-
-
-(** documents **)
-
-datatype entry = Entry of {next: Document.command_id option, state: Document.state_id option};
-type node = entry Symtab.table; (*unique command entries indexed by command_id, start with no_id*)
-type document = node Graph.T; (*development graph via static imports*)
-
-
-(* command entries *)
-
-fun make_entry next state = Entry {next = next, state = state};
-
-fun the_entry (node: node) (id: Document.command_id) =
- (case Symtab.lookup node id of
- NONE => err_undef "command entry" id
- | SOME (Entry entry) => entry);
-
-fun put_entry (id: Document.command_id, entry: entry) = Symtab.update (id, entry);
-
-fun put_entry_state (id: Document.command_id) state (node: node) =
- let val {next, ...} = the_entry node id
- in put_entry (id, make_entry next state) node end;
-
-fun reset_entry_state id = put_entry_state id NONE;
-fun set_entry_state (id, state_id) = put_entry_state id (SOME state_id);
-
-
-(* iterate entries *)
-
-fun fold_entries id0 f (node: node) =
- let
- fun apply NONE x = x
- | apply (SOME id) x =
- let val entry = the_entry node id
- in apply (#next entry) (f (id, entry) x) end;
- in if Symtab.defined node id0 then apply (SOME id0) else I end;
-
-fun first_entry P (node: node) =
- let
- fun first _ NONE = NONE
- | first prev (SOME id) =
- let val entry = the_entry node id
- in if P (id, entry) then SOME (prev, id, entry) else first (SOME id) (#next entry) end;
- in first NONE (SOME Document.no_id) end;
-
-
-(* modify entries *)
-
-fun insert_after (id: Document.command_id) (id2: Document.command_id) (node: node) =
- let val {next, state} = the_entry node id in
- node
- |> put_entry (id, make_entry (SOME id2) state)
- |> put_entry (id2, make_entry next NONE)
- end;
-
-fun delete_after (id: Document.command_id) (node: node) =
- let val {next, state} = the_entry node id in
- (case next of
- NONE => error ("No next entry to delete: " ^ quote id)
- | SOME id2 =>
- node |>
- (case #next (the_entry node id2) of
- NONE => put_entry (id, make_entry NONE state)
- | SOME id3 => put_entry (id, make_entry (SOME id3) state) #> reset_entry_state id3))
- end;
-
-
-(* node operations *)
-
-val empty_node: node = Symtab.make [(Document.no_id, make_entry NONE (SOME Document.no_id))];
-
-fun the_node (document: document) name =
- Graph.get_node document name handle Graph.UNDEF _ => empty_node;
-
-fun edit_node (id, SOME id2) = insert_after id id2
- | edit_node (id, NONE) = delete_after id;
-
-fun edit_nodes (name, SOME edits) =
- Graph.default_node (name, empty_node) #>
- Graph.map_node name (fold edit_node edits)
- | edit_nodes (name, NONE) = Graph.del_node name;
-
-
-
-(** global configuration **)
-
-(* states *)
-
-local
-
-val global_states =
- Unsynchronized.ref (Symtab.make [(Document.no_id, Lazy.value (SOME Toplevel.toplevel))]);
-
-in
-
-fun define_state (id: Document.state_id) state =
- NAMED_CRITICAL "Isar" (fn () =>
- Unsynchronized.change global_states (Symtab.update_new (id, state))
- handle Symtab.DUP dup => err_dup "state" dup);
-
-fun the_state (id: Document.state_id) =
- (case Symtab.lookup (! global_states) id of
- NONE => err_undef "state" id
- | SOME state => state);
-
-end;
-
-
-(* commands *)
-
-local
-
-val global_commands = Unsynchronized.ref (Symtab.make [(Document.no_id, Toplevel.empty)]);
-
-in
-
-fun define_command (id: Document.command_id) text =
- let
- val tr =
- Position.setmp_thread_data (Position.id_only id) (fn () =>
- Outer_Syntax.prepare_command (Position.id id) text) ();
- in
- NAMED_CRITICAL "Isar" (fn () =>
- Unsynchronized.change global_commands (Symtab.update_new (id, Toplevel.put_id id tr))
- handle Symtab.DUP dup => err_dup "command" dup)
- end;
-
-fun the_command (id: Document.command_id) =
- (case Symtab.lookup (! global_commands) id of
- NONE => err_undef "command" id
- | SOME tr => tr);
-
-end;
-
-
-(* document versions *)
-
-local
-
-val global_documents = Unsynchronized.ref (Symtab.make [(Document.no_id, Graph.empty: document)]);
-
-in
-
-fun define_document (id: Document.version_id) document =
- NAMED_CRITICAL "Isar" (fn () =>
- Unsynchronized.change global_documents (Symtab.update_new (id, document))
- handle Symtab.DUP dup => err_dup "document" dup);
-
-fun the_document (id: Document.version_id) =
- (case Symtab.lookup (! global_documents) id of
- NONE => err_undef "document" id
- | SOME document => document);
-
-end;
-
-
-
-(** document editing **)
-
-(* execution *)
-
-local
-
-val execution: unit future list Unsynchronized.ref = Unsynchronized.ref [];
-
-fun force_state NONE = ()
- | force_state (SOME state_id) = ignore (Lazy.force (the_state state_id));
-
-in
-
-fun execute document =
- NAMED_CRITICAL "Isar" (fn () =>
- let
- val old_execution = ! execution;
- val _ = List.app Future.cancel old_execution;
- fun await_cancellation () = uninterruptible (K Future.join_results) old_execution;
- (* FIXME proper node deps *)
- val new_execution = Graph.keys document |> map (fn name =>
- Future.fork_pri 1 (fn () =>
- let
- val _ = await_cancellation ();
- val exec =
- fold_entries Document.no_id (fn (_, {state, ...}) => fn () => force_state state)
- (the_node document name);
- in exec () end));
- in execution := new_execution end);
-
-end;
-
-
-(* editing *)
-
-local
-
-fun is_changed node' (id, {next = _, state}) =
- (case try (the_entry node') id of
- NONE => true
- | SOME {next = _, state = state'} => state' <> state);
-
-fun new_state name (id: Document.command_id) (state_id, updates) =
- let
- val state = the_state state_id;
- val state_id' = create_id ();
- val tr = Toplevel.put_id state_id' (the_command id);
- val state' =
- Lazy.lazy (fn () =>
- (case Lazy.force state of
- NONE => NONE
- | SOME st => Toplevel.run_command name tr st));
- val _ = define_state state_id' state';
- in (state_id', (id, state_id') :: updates) end;
-
-fun updates_status updates =
- implode (map (fn (id, state_id) => Markup.markup (Markup.edit id state_id) "") updates)
- |> Markup.markup Markup.assign
- |> Output.status;
-
-in
-
-fun edit_document (old_id: Document.version_id) (new_id: Document.version_id) edits =
- Position.setmp_thread_data (Position.id_only new_id) (fn () =>
- NAMED_CRITICAL "Isar" (fn () =>
- let
- val old_document = the_document old_id;
- val new_document = fold edit_nodes edits old_document;
-
- fun update_node name node =
- (case first_entry (is_changed (the_node old_document name)) node of
- NONE => ([], node)
- | SOME (prev, id, _) =>
- let
- val prev_state_id = the (#state (the_entry node (the prev)));
- val (_, updates) = fold_entries id (new_state name o #1) node (prev_state_id, []);
- val node' = fold set_entry_state updates node;
- in (rev updates, node') end);
-
- (* FIXME proper node deps *)
- val (updatess, new_document') =
- (Graph.keys new_document, new_document)
- |-> fold_map (fn name => Graph.map_node_yield name (update_node name));
-
- val _ = define_document new_id new_document';
- val _ = updates_status (flat updatess);
- val _ = execute new_document';
- in () end)) ();
-
-end;
-
-
-
-(** Isabelle process commands **)
-
-val _ =
- Isabelle_Process.add_command "Isar_Document.define_command"
- (fn [id, text] => define_command id text);
-
-val _ =
- Isabelle_Process.add_command "Isar_Document.edit_document"
- (fn [old_id, new_id, edits] =>
- edit_document old_id new_id
- (XML_Data.dest_list (XML_Data.dest_pair XML_Data.dest_string
- (XML_Data.dest_option (XML_Data.dest_list
- (XML_Data.dest_pair XML_Data.dest_string
- (XML_Data.dest_option XML_Data.dest_string))))) (YXML.parse_body edits)));
-
-end;
-
--- a/src/Pure/Isar/isar_document.scala Mon Aug 16 10:32:35 2010 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,59 +0,0 @@
-/* Title: Pure/Isar/isar_document.scala
- Author: Makarius
-
-Interactive Isar documents.
-*/
-
-package isabelle
-
-
-object Isar_Document
-{
- /* protocol messages */
-
- object Assign {
- def unapply(msg: XML.Tree): Option[List[XML.Tree]] =
- msg match {
- case XML.Elem(Markup.Assign, edits) => Some(edits)
- case _ => None
- }
- }
-
- object Edit {
- def unapply(msg: XML.Tree): Option[(Document.Command_ID, Document.State_ID)] =
- msg match {
- case XML.Elem(Markup(Markup.EDIT, List((Markup.ID, cmd_id), (Markup.STATE, state_id))), Nil) =>
- Some(cmd_id, state_id)
- case _ => None
- }
- }
-}
-
-
-trait Isar_Document extends Isabelle_Process
-{
- import Isar_Document._
-
-
- /* commands */
-
- def define_command(id: Document.Command_ID, text: String): Unit =
- input("Isar_Document.define_command", id, text)
-
-
- /* documents */
-
- def edit_document(old_id: Document.Version_ID, new_id: Document.Version_ID,
- edits: List[Document.Edit[Document.Command_ID]])
- {
- def make_id1(id1: Option[Document.Command_ID]): XML.Body =
- XML_Data.make_string(id1 getOrElse Document.NO_ID)
- val arg =
- XML_Data.make_list(
- XML_Data.make_pair(XML_Data.make_string)(
- XML_Data.make_option(XML_Data.make_list(
- XML_Data.make_pair(make_id1)(XML_Data.make_option(XML_Data.make_string))))))(edits)
-
- input("Isar_Document.edit_document", old_id, new_id, YXML.string_of_body(arg))
- }
-}
--- a/src/Pure/Isar/keyword.ML Mon Aug 16 10:32:35 2010 +0200
+++ b/src/Pure/Isar/keyword.ML Mon Aug 16 10:32:45 2010 +0200
@@ -151,7 +151,8 @@
val keyword_statusN = "keyword_status";
fun status_message s =
- (if print_mode_active keyword_statusN then Output.status else writeln) s;
+ Position.setmp_thread_data Position.none
+ (if print_mode_active keyword_statusN then Output.status else writeln) s;
fun keyword_status name =
status_message (Markup.markup (Markup.keyword_decl name)
--- a/src/Pure/Isar/token.scala Mon Aug 16 10:32:35 2010 +0200
+++ b/src/Pure/Isar/token.scala Mon Aug 16 10:32:45 2010 +0200
@@ -27,7 +27,6 @@
val VERBATIM = Value("verbatim text")
val SPACE = Value("white space")
val COMMENT = Value("comment text")
- val BAD_INPUT = Value("bad input")
val UNPARSED = Value("unparsed input")
}
@@ -79,7 +78,6 @@
def is_space: Boolean = kind == Token.Kind.SPACE
def is_comment: Boolean = kind == Token.Kind.COMMENT
def is_ignored: Boolean = is_space || is_comment
- def is_unparsed: Boolean = kind == Token.Kind.UNPARSED
def content: String =
if (kind == Token.Kind.STRING) Scan.Lexicon.empty.quoted_content("\"", source)
--- a/src/Pure/PIDE/command.scala Mon Aug 16 10:32:35 2010 +0200
+++ b/src/Pure/PIDE/command.scala Mon Aug 16 10:32:45 2010 +0200
@@ -1,5 +1,4 @@
/* Title: Pure/PIDE/command.scala
- Author: Johannes Hölzl, TU Munich
Author: Fabian Immler, TU Munich
Author: Makarius
@@ -13,9 +12,6 @@
import scala.collection.mutable
-case class Command_Set(set: Set[Command])
-
-
object Command
{
object Status extends Enumeration
@@ -31,14 +27,128 @@
}
case class TypeInfo(ty: String)
case class RefInfo(file: Option[String], line: Option[Int],
- command_id: Option[String], offset: Option[Int])
+ command_id: Option[Document.Command_ID], offset: Option[Int]) // FIXME Command_ID vs. Exec_ID !?
+
+
+
+ /** accumulated results from prover **/
+
+ case class State(
+ val command: Command,
+ val status: Command.Status.Value,
+ val forks: Int,
+ val reverse_results: List[XML.Tree],
+ val markup: Markup_Text)
+ {
+ /* content */
+
+ lazy val results = reverse_results.reverse
+
+ def add_result(result: XML.Tree): State = copy(reverse_results = result :: reverse_results)
+
+ def add_markup(node: Markup_Tree): State = copy(markup = markup + node)
+
+
+ /* markup */
+
+ lazy val highlight: Markup_Text =
+ {
+ markup.filter(_.info match {
+ case Command.HighlightInfo(_, _) => true
+ case _ => false
+ })
+ }
+
+ private lazy val types: List[Markup_Node] =
+ markup.filter(_.info match {
+ case Command.TypeInfo(_) => true
+ case _ => false }).flatten
+
+ def type_at(pos: Int): Option[String] =
+ {
+ types.find(t => t.start <= pos && pos < t.stop) match {
+ case Some(t) =>
+ t.info match {
+ case Command.TypeInfo(ty) => Some(command.source(t.start, t.stop) + " : " + ty)
+ case _ => None
+ }
+ case None => None
+ }
+ }
+
+ private lazy val refs: List[Markup_Node] =
+ markup.filter(_.info match {
+ case Command.RefInfo(_, _, _, _) => true
+ case _ => false }).flatten
+
+ def ref_at(pos: Int): Option[Markup_Node] =
+ refs.find(t => t.start <= pos && pos < t.stop)
+
+
+ /* message dispatch */
+
+ def accumulate(message: XML.Tree): Command.State =
+ message match {
+ case XML.Elem(Markup(Markup.STATUS, _), elems) =>
+ (this /: elems)((state, elem) =>
+ elem match {
+ case XML.Elem(Markup(Markup.UNPROCESSED, _), _) => state.copy(status = Command.Status.UNPROCESSED)
+ case XML.Elem(Markup(Markup.FINISHED, _), _) => state.copy(status = Command.Status.FINISHED)
+ case XML.Elem(Markup(Markup.FAILED, _), _) => state.copy(status = Command.Status.FAILED)
+ case XML.Elem(Markup(Markup.FORKED, _), _) => state.copy(forks = state.forks + 1)
+ case XML.Elem(Markup(Markup.JOINED, _), _) => state.copy(forks = state.forks - 1)
+ case _ => System.err.println("Ignored status message: " + elem); state
+ })
+
+ case XML.Elem(Markup(Markup.REPORT, _), elems) =>
+ (this /: elems)((state, elem) =>
+ elem match {
+ case XML.Elem(Markup(kind, atts), body) if Position.get_id(atts) == Some(command.id) =>
+ atts match {
+ case Position.Range(begin, end) =>
+ if (kind == Markup.ML_TYPING) {
+ val info = Pretty.string_of(body, margin = 40)
+ state.add_markup(
+ command.markup_node(begin - 1, end - 1, Command.TypeInfo(info)))
+ }
+ else if (kind == Markup.ML_REF) {
+ body match {
+ case List(XML.Elem(Markup(Markup.ML_DEF, props), _)) =>
+ state.add_markup(
+ command.markup_node(
+ begin - 1, end - 1,
+ Command.RefInfo(
+ Position.get_file(props),
+ Position.get_line(props),
+ Position.get_id(props),
+ Position.get_offset(props))))
+ case _ => state
+ }
+ }
+ else {
+ state.add_markup(
+ command.markup_node(begin - 1, end - 1,
+ Command.HighlightInfo(kind, Markup.get_string(Markup.KIND, atts))))
+ }
+ case _ => state
+ }
+ case _ => System.err.println("Ignored report message: " + elem); state
+ })
+ case _ => add_result(message)
+ }
+ }
+
+
+ /* unparsed dummy commands */
+
+ def unparsed(source: String) =
+ new Command(Document.NO_ID, List(Token(Token.Kind.UNPARSED, source)))
}
+
class Command(
val id: Document.Command_ID,
- val span: Thy_Syntax.Span,
- val static_parent: Option[Command] = None) // FIXME !?
- extends Session.Entity
+ val span: List[Token])
{
/* classification */
@@ -46,6 +156,8 @@
def is_ignored: Boolean = span.forall(_.is_ignored)
def is_malformed: Boolean = !is_command && !is_ignored
+ def is_unparsed = id == Document.NO_ID
+
def name: String = if (is_command) span.head.content else ""
override def toString =
id + "/" + (if (is_command) name else if (is_ignored) "IGNORED" else "MALFORMED")
@@ -60,54 +172,18 @@
lazy val symbol_index = new Symbol.Index(source)
- /* accumulated messages */
-
- @volatile protected var state = new State(this)
- def current_state: State = state
-
- private case class Consume(message: XML.Tree, forward: Command => Unit)
- private case object Assign
-
- private val accumulator = actor {
- var assigned = false
- loop {
- react {
- case Consume(message, forward) if !assigned =>
- val old_state = state
- state = old_state.accumulate(message)
- if (!(state eq old_state)) forward(static_parent getOrElse this)
-
- case Assign =>
- assigned = true // single assignment
- reply(())
-
- case bad => System.err.println("Command accumulator: ignoring bad message " + bad)
- }
- }
- }
-
- def consume(message: XML.Tree, forward: Command => Unit)
- {
- accumulator ! Consume(message, forward)
- }
-
- def assign_state(state_id: Document.State_ID): Command =
- {
- val cmd = new Command(state_id, span, Some(this))
- accumulator !? Assign
- cmd.state = current_state
- cmd
- }
-
-
/* markup */
- lazy val empty_markup = new Markup_Text(Nil, source)
-
def markup_node(begin: Int, end: Int, info: Any): Markup_Tree =
{
val start = symbol_index.decode(begin)
val stop = symbol_index.decode(end)
new Markup_Tree(new Markup_Node(start, stop, info), Nil)
}
+
+
+ /* accumulated results */
+
+ val empty_state: Command.State =
+ Command.State(this, Command.Status.UNPROCESSED, 0, Nil, new Markup_Text(Nil, source))
}
--- a/src/Pure/PIDE/document.ML Mon Aug 16 10:32:35 2010 +0200
+++ b/src/Pure/PIDE/document.ML Mon Aug 16 10:32:45 2010 +0200
@@ -7,10 +7,13 @@
signature DOCUMENT =
sig
- type state_id = string
- type command_id = string
- type version_id = string
- val no_id: string
+ type id = int
+ type version_id = id
+ type command_id = id
+ type exec_id = id
+ val no_id: id
+ val parse_id: string -> id
+ val print_id: id -> string
type edit = string * ((command_id * command_id option) list) option
end;
@@ -19,11 +22,15 @@
(* unique identifiers *)
-type state_id = string;
-type command_id = string;
-type version_id = string;
+type id = int;
+type version_id = id;
+type command_id = id;
+type exec_id = id;
-val no_id = "";
+val no_id = 0;
+
+val parse_id = Markup.parse_int;
+val print_id = Markup.print_int;
(* edits *)
--- a/src/Pure/PIDE/document.scala Mon Aug 16 10:32:35 2010 +0200
+++ b/src/Pure/PIDE/document.scala Mon Aug 16 10:32:45 2010 +0200
@@ -9,18 +9,24 @@
import scala.collection.mutable
-import scala.annotation.tailrec
object Document
{
/* formal identifiers */
- type Version_ID = String
- type Command_ID = String
- type State_ID = String
+ type ID = Long
- val NO_ID = ""
+ object ID {
+ def apply(id: ID): String = Markup.Long.apply(id)
+ def unapply(s: String): Option[ID] = Markup.Long.unapply(s)
+ }
+
+ type Version_ID = ID
+ type Command_ID = ID
+ type Exec_ID = ID
+
+ val NO_ID: ID = 0
@@ -74,12 +80,7 @@
/* initial document */
- val init: Document =
- {
- val doc = new Document(NO_ID, Map().withDefaultValue(Node.empty), Map())
- doc.assign_states(Nil)
- doc
- }
+ val init: Document = new Document(NO_ID, Map().withDefaultValue(Node.empty))
@@ -98,161 +99,121 @@
val is_outdated: Boolean
def convert(offset: Int): Int
def revert(offset: Int): Int
+ def lookup_command(id: Command_ID): Option[Command]
+ def state(command: Command): Command.State
}
object Change
{
- val init = new Change(NO_ID, None, Nil, Future.value(Nil, Document.init))
+ val init = new Change(Future.value(Document.init), Nil, Future.value(Nil, Document.init))
}
class Change(
- val id: Version_ID,
- val parent: Option[Change],
+ val prev: Future[Document],
val edits: List[Node_Text_Edit],
val result: Future[(List[Edit[Command]], Document)])
{
- def ancestors: Iterator[Change] = new Iterator[Change]
- {
- private var state: Option[Change] = Some(Change.this)
- def hasNext = state.isDefined
- def next =
- state match {
- case Some(change) => state = change.parent; change
- case None => throw new NoSuchElementException("next on empty iterator")
- }
- }
-
- def join_document: Document = result.join._2
- def is_assigned: Boolean = result.is_finished && join_document.assignment.is_finished
-
- def snapshot(name: String, pending_edits: List[Text_Edit]): Snapshot =
- {
- val latest = Change.this
- val stable = latest.ancestors.find(_.is_assigned)
- require(stable.isDefined)
-
- val edits =
- (pending_edits /: latest.ancestors.takeWhile(_ != stable.get))((edits, change) =>
- (for ((a, eds) <- change.edits if a == name) yield eds).flatten ::: edits)
- lazy val reverse_edits = edits.reverse
-
- new Snapshot {
- val document = stable.get.join_document
- val node = document.nodes(name)
- val is_outdated = !(pending_edits.isEmpty && latest == stable.get)
- def convert(offset: Int): Int = (offset /: edits)((i, edit) => edit.convert(i))
- def revert(offset: Int): Int = (offset /: reverse_edits)((i, edit) => edit.revert(i))
- }
- }
+ val document: Future[Document] = result.map(_._2)
+ def is_finished: Boolean = prev.is_finished && document.is_finished
}
- /** editing **/
-
- def text_edits(session: Session, old_doc: Document, new_id: Version_ID,
- edits: List[Node_Text_Edit]): (List[Edit[Command]], Document) =
- {
- require(old_doc.assignment.is_finished)
-
-
- /* unparsed dummy commands */
+ /** global state -- accumulated prover results **/
- def unparsed(source: String) =
- new Command(NO_ID, List(Token(Token.Kind.UNPARSED, source)))
-
- def is_unparsed(command: Command) = command.id == NO_ID
+ object State
+ {
+ class Fail(state: State) extends Exception
-
- /* phase 1: edit individual command source */
+ val init = State().define_document(Document.init, Map()).assign(Document.init.id, Nil)
- @tailrec def edit_text(eds: List[Text_Edit],
- commands: Linear_Set[Command]): Linear_Set[Command] =
+ class Assignment(former_assignment: Map[Command, Exec_ID])
{
- eds match {
- case e :: es =>
- Node.command_starts(commands.iterator).find {
- case (cmd, cmd_start) =>
- e.can_edit(cmd.source, cmd_start) ||
- e.is_insert && e.start == cmd_start + cmd.length
- } match {
- case Some((cmd, cmd_start)) if e.can_edit(cmd.source, cmd_start) =>
- val (rest, text) = e.edit(cmd.source, cmd_start)
- val new_commands = commands.insert_after(Some(cmd), unparsed(text)) - cmd
- edit_text(rest.toList ::: es, new_commands)
+ @volatile private var tmp_assignment = former_assignment
+ private val promise = Future.promise[Map[Command, Exec_ID]]
+ def is_finished: Boolean = promise.is_finished
+ def join: Map[Command, Exec_ID] = promise.join
+ def assign(command_execs: List[(Command, Exec_ID)])
+ {
+ promise.fulfill(tmp_assignment ++ command_execs)
+ tmp_assignment = Map()
+ }
+ }
+ }
- case Some((cmd, cmd_start)) =>
- edit_text(es, commands.insert_after(Some(cmd), unparsed(e.text)))
+ case class State(
+ val documents: Map[Version_ID, Document] = Map(),
+ val commands: Map[Command_ID, Command.State] = Map(),
+ val execs: Map[Exec_ID, (Command.State, Set[Document])] = Map(),
+ val assignments: Map[Document, State.Assignment] = Map(),
+ val disposed: Set[ID] = Set()) // FIXME unused!?
+ {
+ private def fail[A]: A = throw new State.Fail(this)
- case None =>
- require(e.is_insert && e.start == 0)
- edit_text(es, commands.insert_after(None, unparsed(e.text)))
- }
- case Nil => commands
- }
+ def define_document(document: Document, former_assignment: Map[Command, Exec_ID]): State =
+ {
+ val id = document.id
+ if (documents.isDefinedAt(id) || disposed(id)) fail
+ copy(documents = documents + (id -> document),
+ assignments = assignments + (document -> new State.Assignment(former_assignment)))
+ }
+
+ def define_command(command: Command): State =
+ {
+ val id = command.id
+ if (commands.isDefinedAt(id) || disposed(id)) fail
+ copy(commands = commands + (id -> command.empty_state))
}
-
- /* phase 2: recover command spans */
+ def lookup_command(id: Command_ID): Option[Command] = commands.get(id).map(_.command)
- @tailrec def parse_spans(commands: Linear_Set[Command]): Linear_Set[Command] =
- {
- commands.iterator.find(is_unparsed) match {
- case Some(first_unparsed) =>
- val first =
- commands.reverse_iterator(first_unparsed).find(_.is_command) getOrElse commands.head
- val last =
- commands.iterator(first_unparsed).find(_.is_command) getOrElse commands.last
- val range =
- commands.iterator(first).takeWhile(_ != last).toList ::: List(last)
-
- val sources = range.flatMap(_.span.map(_.source))
- val spans0 = Thy_Syntax.parse_spans(session.current_syntax.scan(sources.mkString))
+ def the_document(id: Version_ID): Document = documents.getOrElse(id, fail)
+ def the_command(id: Command_ID): Command.State = commands.getOrElse(id, fail)
+ def the_exec_state(id: Exec_ID): Command.State = execs.getOrElse(id, fail)._1
+ def the_assignment(document: Document): State.Assignment = assignments.getOrElse(document, fail)
- val (before_edit, spans1) =
- if (!spans0.isEmpty && first.is_command && first.span == spans0.head)
- (Some(first), spans0.tail)
- else (commands.prev(first), spans0)
+ def accumulate(id: ID, message: XML.Tree): (Command.State, State) =
+ execs.get(id) match {
+ case Some((st, docs)) =>
+ val new_st = st.accumulate(message)
+ (new_st, copy(execs = execs + (id -> (new_st, docs))))
+ case None =>
+ commands.get(id) match {
+ case Some(st) =>
+ val new_st = st.accumulate(message)
+ (new_st, copy(commands = commands + (id -> new_st)))
+ case None => fail
+ }
+ }
- val (after_edit, spans2) =
- if (!spans1.isEmpty && last.is_command && last.span == spans1.last)
- (Some(last), spans1.take(spans1.length - 1))
- else (commands.next(last), spans1)
+ def assign(id: Version_ID, edits: List[(Command_ID, Exec_ID)]): State =
+ {
+ val doc = the_document(id)
+ val docs = Set(doc) // FIXME unused (!?)
- val inserted = spans2.map(span => new Command(session.create_id(), span))
- val new_commands =
- commands.delete_between(before_edit, after_edit).append_after(before_edit, inserted)
- parse_spans(new_commands)
-
- case None => commands
- }
+ var new_execs = execs
+ val assigned_execs =
+ for ((cmd_id, exec_id) <- edits) yield {
+ val st = the_command(cmd_id)
+ if (new_execs.isDefinedAt(exec_id) || disposed(exec_id)) fail
+ new_execs += (exec_id -> (st, docs))
+ (st.command, exec_id)
+ }
+ the_assignment(doc).assign(assigned_execs) // FIXME explicit value instead of promise (!?)
+ copy(execs = new_execs)
}
-
- /* phase 3: resulting document edits */
-
- {
- val doc_edits = new mutable.ListBuffer[Edit[Command]]
- var nodes = old_doc.nodes
- var former_states = old_doc.assignment.join
-
- for ((name, text_edits) <- edits) {
- val commands0 = nodes(name).commands
- val commands1 = edit_text(text_edits, commands0)
- val commands2 = parse_spans(commands1) // FIXME somewhat slow
+ def is_assigned(document: Document): Boolean =
+ assignments.get(document) match {
+ case Some(assgn) => assgn.is_finished
+ case None => false
+ }
- 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)))
-
- doc_edits += (name -> Some(cmd_edits))
- nodes += (name -> new Node(commands2))
- former_states --= removed_commands
- }
- (doc_edits.toList, new Document(new_id, nodes, former_states))
+ def command_state(document: Document, command: Command): Command.State =
+ {
+ val assgn = the_assignment(document)
+ require(assgn.is_finished)
+ the_exec_state(assgn.join.getOrElse(command, fail))
}
}
}
@@ -260,28 +221,5 @@
class Document(
val id: Document.Version_ID,
- val nodes: Map[String, Document.Node],
- former_states: Map[Command, Command]) // FIXME !?
-{
- /* command state assignment */
-
- val assignment = Future.promise[Map[Command, Command]]
- def await_assignment { assignment.join }
-
- @volatile private var tmp_states = former_states
+ val nodes: Map[String, Document.Node])
- def assign_states(new_states: List[(Command, Command)])
- {
- assignment.fulfill(tmp_states ++ new_states)
- tmp_states = Map()
- }
-
- def current_state(cmd: Command): State =
- {
- require(assignment.is_finished)
- (assignment.join).get(cmd) match {
- case Some(cmd_state) => cmd_state.current_state
- case None => new State(cmd, Command.Status.UNDEFINED, 0, Nil, cmd.empty_markup)
- }
- }
-}
--- a/src/Pure/PIDE/markup_node.scala Mon Aug 16 10:32:35 2010 +0200
+++ b/src/Pure/PIDE/markup_node.scala Mon Aug 16 10:32:45 2010 +0200
@@ -2,7 +2,7 @@
Author: Fabian Immler, TU Munich
Author: Makarius
-Document markup nodes, with connection to Swing tree model.
+Text markup nodes.
*/
package isabelle
@@ -78,8 +78,7 @@
case class Markup_Text(val markup: List[Markup_Tree], val content: String)
{
- private lazy val root =
- new Markup_Tree(new Markup_Node(0, content.length, None), markup)
+ private val root = new Markup_Tree(new Markup_Node(0, content.length, None), markup) // FIXME !?
def + (new_tree: Markup_Tree): Markup_Text =
new Markup_Text((root + new_tree).branches, content)
--- a/src/Pure/PIDE/state.scala Mon Aug 16 10:32:35 2010 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,125 +0,0 @@
-/* Title: Pure/PIDE/state.scala
- Author: Fabian Immler, TU Munich
- Author: Makarius
-
-Accumulated results from prover.
-*/
-
-package isabelle
-
-
-class State(
- val command: Command,
- val status: Command.Status.Value,
- val forks: Int,
- val reverse_results: List[XML.Tree],
- val markup_root: Markup_Text)
-{
- def this(command: Command) =
- this(command, Command.Status.UNPROCESSED, 0, Nil, command.empty_markup)
-
-
- /* content */
-
- private def set_status(st: Command.Status.Value): State =
- new State(command, st, forks, reverse_results, markup_root)
-
- private def add_forks(i: Int): State =
- new State(command, status, forks + i, reverse_results, markup_root)
-
- private def add_result(res: XML.Tree): State =
- new State(command, status, forks, res :: reverse_results, markup_root)
-
- private def add_markup(node: Markup_Tree): State =
- new State(command, status, forks, reverse_results, markup_root + node)
-
- lazy val results = reverse_results.reverse
-
-
- /* markup */
-
- lazy val highlight: Markup_Text =
- {
- markup_root.filter(_.info match {
- case Command.HighlightInfo(_, _) => true
- case _ => false
- })
- }
-
- private lazy val types: List[Markup_Node] =
- markup_root.filter(_.info match {
- case Command.TypeInfo(_) => true
- case _ => false }).flatten
-
- def type_at(pos: Int): Option[String] =
- {
- types.find(t => t.start <= pos && pos < t.stop) match {
- case Some(t) =>
- t.info match {
- case Command.TypeInfo(ty) => Some(command.source(t.start, t.stop) + " : " + ty)
- case _ => None
- }
- case None => None
- }
- }
-
- private lazy val refs: List[Markup_Node] =
- markup_root.filter(_.info match {
- case Command.RefInfo(_, _, _, _) => true
- case _ => false }).flatten
-
- def ref_at(pos: Int): Option[Markup_Node] =
- refs.find(t => t.start <= pos && pos < t.stop)
-
-
- /* message dispatch */
-
- def accumulate(message: XML.Tree): State =
- message match {
- case XML.Elem(Markup(Markup.STATUS, _), elems) =>
- (this /: elems)((state, elem) =>
- elem match {
- case XML.Elem(Markup(Markup.UNPROCESSED, _), _) => state.set_status(Command.Status.UNPROCESSED)
- case XML.Elem(Markup(Markup.FINISHED, _), _) => state.set_status(Command.Status.FINISHED)
- case XML.Elem(Markup(Markup.FAILED, _), _) => state.set_status(Command.Status.FAILED)
- case XML.Elem(Markup(Markup.FORKED, _), _) => state.add_forks(1)
- case XML.Elem(Markup(Markup.JOINED, _), _) => state.add_forks(-1)
- case _ => System.err.println("Ignored status message: " + elem); state
- })
-
- case XML.Elem(Markup(Markup.REPORT, _), elems) =>
- (this /: elems)((state, elem) =>
- elem match {
- case XML.Elem(Markup(kind, atts), body) if Position.get_id(atts) == Some(command.id) =>
- atts match {
- case Position.Range(begin, end) =>
- if (kind == Markup.ML_TYPING) {
- val info = Pretty.string_of(body, margin = 40)
- state.add_markup(
- command.markup_node(begin - 1, end - 1, Command.TypeInfo(info)))
- }
- else if (kind == Markup.ML_REF) {
- body match {
- case List(XML.Elem(Markup(Markup.ML_DEF, atts), _)) =>
- state.add_markup(command.markup_node(
- begin - 1, end - 1,
- Command.RefInfo(
- Position.get_file(atts),
- Position.get_line(atts),
- Position.get_id(atts),
- Position.get_offset(atts))))
- case _ => state
- }
- }
- else {
- state.add_markup(
- command.markup_node(begin - 1, end - 1,
- Command.HighlightInfo(kind, Markup.get_string(Markup.KIND, atts))))
- }
- case _ => state
- }
- case _ => System.err.println("Ignored report message: " + elem); state
- })
- case _ => add_result(message)
- }
-}
--- a/src/Pure/ROOT.ML Mon Aug 16 10:32:35 2010 +0200
+++ b/src/Pure/ROOT.ML Mon Aug 16 10:32:45 2010 +0200
@@ -255,9 +255,9 @@
(* Isabelle/Isar system *)
use "System/session.ML";
+use "System/isabelle_process.ML";
+use "System/isar_document.ML";
use "System/isar.ML";
-use "System/isabelle_process.ML";
-use "Isar/isar_document.ML";
(* miscellaneous tools and packages for Pure Isabelle *)
--- a/src/Pure/System/isabelle_process.scala Mon Aug 16 10:32:35 2010 +0200
+++ b/src/Pure/System/isabelle_process.scala Mon Aug 16 10:32:45 2010 +0200
@@ -373,8 +373,11 @@
def input_raw(text: String): Unit = standard_input ! Input_Text(text)
+ def input_bytes(name: String, args: Array[Byte]*): Unit =
+ command_input ! Input_Chunks(Standard_System.string_bytes(name) :: args.toList)
+
def input(name: String, args: String*): Unit =
- command_input ! Input_Chunks((name :: args.toList).map(Standard_System.string_bytes))
+ input_bytes(name, args.map(Standard_System.string_bytes): _*)
def close(): Unit = command_input ! Close
}
--- a/src/Pure/System/isabelle_system.scala Mon Aug 16 10:32:35 2010 +0200
+++ b/src/Pure/System/isabelle_system.scala Mon Aug 16 10:32:45 2010 +0200
@@ -8,8 +8,7 @@
import java.util.regex.Pattern
import java.util.Locale
-import java.io.{BufferedInputStream, FileInputStream, BufferedOutputStream, FileOutputStream,
- OutputStream, File, IOException}
+import java.io.{InputStream, FileInputStream, OutputStream, FileOutputStream, File, IOException}
import java.awt.{GraphicsEnvironment, Font}
import java.awt.font.TextAttribute
@@ -287,39 +286,33 @@
if (rc != 0) error(result)
}
- def fifo_input_stream(fifo: String): BufferedInputStream =
+ def fifo_input_stream(fifo: String): InputStream =
{
- // block until peer is ready
- val stream =
- if (Platform.is_windows) { // Cygwin fifo as Windows/Java input stream
- val proc = execute(false, expand_path("$ISABELLE_HOME/lib/scripts/raw_dump"), fifo, "-")
- proc.getOutputStream.close
- proc.getErrorStream.close
- proc.getInputStream
- }
- else new FileInputStream(fifo)
- new BufferedInputStream(stream)
+ if (Platform.is_windows) { // Cygwin fifo as Windows/Java input stream
+ val proc = execute(false, expand_path("$ISABELLE_HOME/lib/scripts/raw_dump"), fifo, "-")
+ proc.getOutputStream.close
+ proc.getErrorStream.close
+ proc.getInputStream
+ }
+ else new FileInputStream(fifo)
}
- def fifo_output_stream(fifo: String): BufferedOutputStream =
+ def fifo_output_stream(fifo: String): OutputStream =
{
- // block until peer is ready
- val stream =
- if (Platform.is_windows) { // Cygwin fifo as Windows/Java output stream
- val proc = execute(false, expand_path("$ISABELLE_HOME/lib/scripts/raw_dump"), "-", fifo)
- proc.getInputStream.close
- proc.getErrorStream.close
- val out = proc.getOutputStream
- new OutputStream {
- override def close() { out.close(); proc.waitFor() }
- override def flush() { out.flush() }
- override def write(b: Array[Byte]) { out.write(b) }
- override def write(b: Array[Byte], off: Int, len: Int) { out.write(b, off, len) }
- override def write(b: Int) { out.write(b) }
- }
+ if (Platform.is_windows) { // Cygwin fifo as Windows/Java output stream
+ val proc = execute(false, expand_path("$ISABELLE_HOME/lib/scripts/raw_dump"), "-", fifo)
+ proc.getInputStream.close
+ proc.getErrorStream.close
+ val out = proc.getOutputStream
+ new OutputStream {
+ override def close() { out.close(); proc.waitFor() }
+ override def flush() { out.flush() }
+ override def write(b: Array[Byte]) { out.write(b) }
+ override def write(b: Array[Byte], off: Int, len: Int) { out.write(b, off, len) }
+ override def write(b: Int) { out.write(b) }
}
- else new FileOutputStream(fifo)
- new BufferedOutputStream(stream)
+ }
+ else new FileOutputStream(fifo)
}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/System/isar_document.ML Mon Aug 16 10:32:45 2010 +0200
@@ -0,0 +1,295 @@
+(* Title: Pure/System/isar_document.ML
+ Author: Makarius
+
+Interactive Isar documents, which are structured as follows:
+
+ - history: tree of documents (i.e. changes without merge)
+ - document: graph of nodes (cf. theory files)
+ - node: linear set of commands, potentially with proof structure
+*)
+
+structure Isar_Document: sig end =
+struct
+
+(* unique identifiers *)
+
+local
+ val id_count = Synchronized.var "id" 0;
+in
+ fun create_id () =
+ Synchronized.change_result id_count
+ (fn i =>
+ let val i' = i + 1
+ in (i', i') end);
+end;
+
+fun err_dup kind id = error ("Duplicate " ^ kind ^ ": " ^ Document.print_id id);
+fun err_undef kind id = error ("Undefined " ^ kind ^ ": " ^ Document.print_id id);
+
+
+(** documents **)
+
+datatype entry = Entry of {next: Document.command_id option, exec: Document.exec_id option};
+type node = entry Inttab.table; (*unique command entries indexed by command_id, start with no_id*)
+type document = node Graph.T; (*development graph via static imports*)
+
+
+(* command entries *)
+
+fun make_entry next exec = Entry {next = next, exec = exec};
+
+fun the_entry (node: node) (id: Document.command_id) =
+ (case Inttab.lookup node id of
+ NONE => err_undef "command entry" id
+ | SOME (Entry entry) => entry);
+
+fun put_entry (id: Document.command_id, entry: entry) = Inttab.update (id, entry);
+
+fun put_entry_exec (id: Document.command_id) exec (node: node) =
+ let val {next, ...} = the_entry node id
+ in put_entry (id, make_entry next exec) node end;
+
+fun reset_entry_exec id = put_entry_exec id NONE;
+fun set_entry_exec (id, exec_id) = put_entry_exec id (SOME exec_id);
+
+
+(* iterate entries *)
+
+fun fold_entries id0 f (node: node) =
+ let
+ fun apply NONE x = x
+ | apply (SOME id) x =
+ let val entry = the_entry node id
+ in apply (#next entry) (f (id, entry) x) end;
+ in if Inttab.defined node id0 then apply (SOME id0) else I end;
+
+fun first_entry P (node: node) =
+ let
+ fun first _ NONE = NONE
+ | first prev (SOME id) =
+ let val entry = the_entry node id
+ in if P (id, entry) then SOME (prev, id, entry) else first (SOME id) (#next entry) end;
+ in first NONE (SOME Document.no_id) end;
+
+
+(* modify entries *)
+
+fun insert_after (id: Document.command_id) (id2: Document.command_id) (node: node) =
+ let val {next, exec} = the_entry node id in
+ node
+ |> put_entry (id, make_entry (SOME id2) exec)
+ |> put_entry (id2, make_entry next NONE)
+ end;
+
+fun delete_after (id: Document.command_id) (node: node) =
+ let val {next, exec} = the_entry node id in
+ (case next of
+ NONE => error ("No next entry to delete: " ^ Document.print_id id)
+ | SOME id2 =>
+ node |>
+ (case #next (the_entry node id2) of
+ NONE => put_entry (id, make_entry NONE exec)
+ | SOME id3 => put_entry (id, make_entry (SOME id3) exec) #> reset_entry_exec id3))
+ end;
+
+
+(* node operations *)
+
+val empty_node: node = Inttab.make [(Document.no_id, make_entry NONE (SOME Document.no_id))];
+
+fun the_node (document: document) name =
+ Graph.get_node document name handle Graph.UNDEF _ => empty_node;
+
+fun edit_node (id, SOME id2) = insert_after id id2
+ | edit_node (id, NONE) = delete_after id;
+
+fun edit_nodes (name, SOME edits) =
+ Graph.default_node (name, empty_node) #>
+ Graph.map_node name (fold edit_node edits)
+ | edit_nodes (name, NONE) = Graph.del_node name;
+
+
+
+(** global configuration **)
+
+(* command executions *)
+
+local
+
+val global_execs =
+ Unsynchronized.ref (Inttab.make [(Document.no_id, Lazy.value (SOME Toplevel.toplevel))]);
+
+in
+
+fun define_exec (id: Document.exec_id) exec =
+ NAMED_CRITICAL "Isar" (fn () =>
+ Unsynchronized.change global_execs (Inttab.update_new (id, exec))
+ handle Inttab.DUP dup => err_dup "exec" dup);
+
+fun the_exec (id: Document.exec_id) =
+ (case Inttab.lookup (! global_execs) id of
+ NONE => err_undef "exec" id
+ | SOME exec => exec);
+
+end;
+
+
+(* commands *)
+
+local
+
+val global_commands = Unsynchronized.ref (Inttab.make [(Document.no_id, Toplevel.empty)]);
+
+in
+
+fun define_command (id: Document.command_id) text =
+ let
+ val id_string = Document.print_id id;
+ val tr =
+ Position.setmp_thread_data (Position.id_only id_string) (fn () =>
+ Outer_Syntax.prepare_command (Position.id id_string) text) ();
+ in
+ NAMED_CRITICAL "Isar" (fn () =>
+ Unsynchronized.change global_commands (Inttab.update_new (id, Toplevel.put_id id_string tr))
+ handle Inttab.DUP dup => err_dup "command" dup)
+ end;
+
+fun the_command (id: Document.command_id) =
+ (case Inttab.lookup (! global_commands) id of
+ NONE => err_undef "command" id
+ | SOME tr => tr);
+
+end;
+
+
+(* document versions *)
+
+local
+
+val global_documents = Unsynchronized.ref (Inttab.make [(Document.no_id, Graph.empty: document)]);
+
+in
+
+fun define_document (id: Document.version_id) document =
+ NAMED_CRITICAL "Isar" (fn () =>
+ Unsynchronized.change global_documents (Inttab.update_new (id, document))
+ handle Inttab.DUP dup => err_dup "document" dup);
+
+fun the_document (id: Document.version_id) =
+ (case Inttab.lookup (! global_documents) id of
+ NONE => err_undef "document" id
+ | SOME document => document);
+
+end;
+
+
+
+(** document editing **)
+
+(* execution *)
+
+local
+
+val execution: unit future list Unsynchronized.ref = Unsynchronized.ref [];
+
+fun force_exec NONE = ()
+ | force_exec (SOME exec_id) = ignore (Lazy.force (the_exec exec_id));
+
+in
+
+fun execute document =
+ NAMED_CRITICAL "Isar" (fn () =>
+ let
+ val old_execution = ! execution;
+ val _ = List.app Future.cancel old_execution;
+ fun await_cancellation () = uninterruptible (K Future.join_results) old_execution;
+ (* FIXME proper node deps *)
+ val new_execution = Graph.keys document |> map (fn name =>
+ Future.fork_pri 1 (fn () =>
+ let
+ val _ = await_cancellation ();
+ val exec =
+ fold_entries Document.no_id (fn (_, {exec, ...}) => fn () => force_exec exec)
+ (the_node document name);
+ in exec () end));
+ in execution := new_execution end);
+
+end;
+
+
+(* editing *)
+
+local
+
+fun is_changed node' (id, {next = _, exec}) =
+ (case try (the_entry node') id of
+ NONE => true
+ | SOME {next = _, exec = exec'} => exec' <> exec);
+
+fun new_exec name (id: Document.command_id) (exec_id, updates) =
+ let
+ val exec = the_exec exec_id;
+ val exec_id' = create_id ();
+ val tr = Toplevel.put_id (Document.print_id exec_id') (the_command id);
+ val exec' =
+ Lazy.lazy (fn () =>
+ (case Lazy.force exec of
+ NONE => NONE
+ | SOME st => Toplevel.run_command name tr st));
+ val _ = define_exec exec_id' exec';
+ in (exec_id', (id, exec_id') :: updates) end;
+
+fun updates_status new_id updates =
+ implode (map (fn (id, exec_id) => Markup.markup (Markup.edit id exec_id) "") updates)
+ |> Markup.markup (Markup.assign new_id)
+ |> Output.status;
+
+in
+
+fun edit_document (old_id: Document.version_id) (new_id: Document.version_id) edits =
+ NAMED_CRITICAL "Isar" (fn () =>
+ let
+ val old_document = the_document old_id;
+ val new_document = fold edit_nodes edits old_document;
+
+ fun update_node name node =
+ (case first_entry (is_changed (the_node old_document name)) node of
+ NONE => ([], node)
+ | SOME (prev, id, _) =>
+ let
+ val prev_exec_id = the (#exec (the_entry node (the prev)));
+ val (_, updates) = fold_entries id (new_exec name o #1) node (prev_exec_id, []);
+ val node' = fold set_entry_exec updates node;
+ in (rev updates, node') end);
+
+ (* FIXME proper node deps *)
+ val (updatess, new_document') =
+ (Graph.keys new_document, new_document)
+ |-> fold_map (fn name => Graph.map_node_yield name (update_node name));
+
+ val _ = define_document new_id new_document';
+ val _ = updates_status new_id (flat updatess);
+ val _ = execute new_document';
+ in () end);
+
+end;
+
+
+
+(** Isabelle process commands **)
+
+val _ =
+ Isabelle_Process.add_command "Isar_Document.define_command"
+ (fn [id, text] => define_command (Document.parse_id id) text);
+
+val _ =
+ Isabelle_Process.add_command "Isar_Document.edit_document"
+ (fn [old_id, new_id, edits] =>
+ edit_document (Document.parse_id old_id) (Document.parse_id new_id)
+ (XML_Data.dest_list (XML_Data.dest_pair XML_Data.dest_string
+ (XML_Data.dest_option (XML_Data.dest_list
+ (XML_Data.dest_pair XML_Data.dest_int
+ (XML_Data.dest_option XML_Data.dest_int))))) (YXML.parse_body edits)));
+
+end;
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/System/isar_document.scala Mon Aug 16 10:32:45 2010 +0200
@@ -0,0 +1,66 @@
+/* Title: Pure/System/isar_document.scala
+ Author: Makarius
+
+Interactive Isar documents.
+*/
+
+package isabelle
+
+
+object Isar_Document
+{
+ /* protocol messages */
+
+ object Assign {
+ def unapply(msg: XML.Tree)
+ : Option[(Document.Version_ID, List[(Document.Command_ID, Document.Exec_ID)])] =
+ msg match {
+ case XML.Elem(Markup(Markup.ASSIGN, List((Markup.VERSION, Document.ID(id)))), edits) =>
+ val id_edits = edits.map(Edit.unapply)
+ if (id_edits.forall(_.isDefined)) Some((id, id_edits.map(_.get)))
+ else None
+ case _ => None
+ }
+ }
+
+ object Edit {
+ def unapply(msg: XML.Tree): Option[(Document.Command_ID, Document.Exec_ID)] =
+ msg match {
+ case XML.Elem(
+ Markup(Markup.EDIT,
+ List((Markup.ID, Document.ID(i)), (Markup.EXEC, Document.ID(j)))), Nil) => Some((i, j))
+ case _ => None
+ }
+ }
+}
+
+
+trait Isar_Document extends Isabelle_Process
+{
+ import Isar_Document._
+
+
+ /* commands */
+
+ def define_command(id: Document.Command_ID, text: String): Unit =
+ input("Isar_Document.define_command", Document.ID(id), text)
+
+
+ /* documents */
+
+ def edit_document(old_id: Document.Version_ID, new_id: Document.Version_ID,
+ edits: List[Document.Edit[Document.Command_ID]])
+ {
+ def make_id1(id1: Option[Document.Command_ID]): XML.Body =
+ XML_Data.make_long(id1 getOrElse Document.NO_ID)
+
+ val arg =
+ XML_Data.make_list(
+ XML_Data.make_pair(XML_Data.make_string)(
+ XML_Data.make_option(XML_Data.make_list(
+ XML_Data.make_pair(make_id1)(XML_Data.make_option(XML_Data.make_long))))))(edits)
+
+ input("Isar_Document.edit_document",
+ Document.ID(old_id), Document.ID(new_id), YXML.string_of_body(arg))
+ }
+}
--- a/src/Pure/System/session.scala Mon Aug 16 10:32:35 2010 +0200
+++ b/src/Pure/System/session.scala Mon Aug 16 10:32:45 2010 +0200
@@ -19,17 +19,7 @@
case object Global_Settings
case object Perspective
-
-
- /* managed entities */
-
- type Entity_ID = String
-
- trait Entity
- {
- val id: Entity_ID
- def consume(message: XML.Tree, forward: Command => Unit): Unit
- }
+ case class Commands_Changed(set: Set[Command])
}
@@ -52,14 +42,18 @@
val global_settings = new Event_Bus[Session.Global_Settings.type]
val raw_results = new Event_Bus[Isabelle_Process.Result]
val raw_output = new Event_Bus[Isabelle_Process.Result]
- val commands_changed = new Event_Bus[Command_Set]
+ val commands_changed = new Event_Bus[Session.Commands_Changed]
val perspective = new Event_Bus[Session.Perspective.type]
/* unique ids */
- private var id_count: BigInt = 0
- def create_id(): Session.Entity_ID = synchronized { id_count += 1; "j" + id_count }
+ private var id_count: Document.ID = 0
+ def create_id(): Document.ID = synchronized {
+ require(id_count > java.lang.Long.MIN_VALUE)
+ id_count -= 1
+ id_count
+ }
@@ -68,13 +62,9 @@
@volatile private var syntax = new Outer_Syntax(system.symbols)
def current_syntax: Outer_Syntax = syntax
- @volatile private var entities = Map[Session.Entity_ID, Session.Entity]()
- def lookup_entity(id: Session.Entity_ID): Option[Session.Entity] = entities.get(id)
- def lookup_command(id: Session.Entity_ID): Option[Command] =
- lookup_entity(id) match {
- case Some(cmd: Command) => Some(cmd)
- case _ => None
- }
+ @volatile private var global_state = Document.State.init
+ private def change_state(f: Document.State => Document.State) { global_state = f(global_state) }
+ def current_state(): Document.State = global_state
private case class Started(timeout: Int, args: List[String])
private case object Stop
@@ -83,26 +73,29 @@
var prover: Isabelle_Process with Isar_Document = null
- def register(entity: Session.Entity) { entities += (entity.id -> entity) }
-
- var documents = Map[Document.Version_ID, Document]()
- def register_document(doc: Document) { documents += (doc.id -> doc) }
- register_document(Document.init)
-
/* document changes */
def handle_change(change: Document.Change)
//{{{
{
- require(change.parent.isDefined)
+ require(change.is_finished)
+
+ val old_doc = change.prev.join
+ val (node_edits, doc) = change.result.join
- val (node_edits, doc) = change.result.join
+ var former_assignment = current_state().the_assignment(old_doc).join
+ for {
+ (name, Some(cmd_edits)) <- node_edits
+ (prev, None) <- cmd_edits
+ removed <- old_doc.nodes(name).commands.get_after(prev)
+ } former_assignment -= removed
+
val id_edits =
node_edits map {
case (name, None) => (name, None)
case (name, Some(cmd_edits)) =>
- val chs =
+ val ids =
cmd_edits map {
case (c1, c2) =>
val id1 = c1.map(_.id)
@@ -110,18 +103,18 @@
c2 match {
case None => None
case Some(command) =>
- if (!lookup_command(command.id).isDefined) {
- register(command)
+ if (current_state().lookup_command(command.id).isEmpty) {
+ change_state(_.define_command(command))
prover.define_command(command.id, system.symbols.encode(command.source))
}
Some(command.id)
}
(id1, id2)
}
- (name -> Some(chs))
+ (name -> Some(ids))
}
- register_document(doc)
- prover.edit_document(change.parent.get.id, doc.id, id_edits)
+ change_state(_.define_document(doc, former_assignment))
+ prover.edit_document(old_doc.id, doc.id, id_edits)
}
//}}}
@@ -138,47 +131,29 @@
{
raw_results.event(result)
- val target_id: Option[Session.Entity_ID] = Position.get_id(result.properties)
- val target: Option[Session.Entity] =
- target_id match {
- case None => None
- case Some(id) => lookup_entity(id)
+ Position.get_id(result.properties) match {
+ case Some(state_id) =>
+ try {
+ val (st, state) = global_state.accumulate(state_id, result.message)
+ global_state = state
+ indicate_command_change(st.command)
+ }
+ catch { case _: Document.State.Fail => bad_result(result) }
+ case None =>
+ if (result.is_status) {
+ result.body match {
+ case List(Isar_Document.Assign(doc_id, edits)) =>
+ try { change_state(_.assign(doc_id, edits)) }
+ catch { case _: Document.State.Fail => bad_result(result) }
+ case List(Keyword.Command_Decl(name, kind)) => syntax += (name, kind)
+ case List(Keyword.Keyword_Decl(name)) => syntax += name
+ case _ => if (!result.is_ready) bad_result(result)
+ }
+ }
+ else if (result.kind == Markup.EXIT) prover = null
+ else if (result.is_raw) raw_output.event(result)
+ else if (!result.is_system) bad_result(result) // FIXME syslog for system messages (!?)
}
- if (target.isDefined) target.get.consume(result.message, indicate_command_change)
- else if (result.is_status) {
- // global status message
- result.body match {
-
- // document state assignment
- case List(Isar_Document.Assign(edits)) if target_id.isDefined =>
- documents.get(target_id.get) match {
- case Some(doc) =>
- val states =
- for {
- Isar_Document.Edit(cmd_id, state_id) <- edits
- cmd <- lookup_command(cmd_id)
- } yield {
- val st = cmd.assign_state(state_id)
- register(st)
- (cmd, st)
- }
- doc.assign_states(states)
- case None => bad_result(result)
- }
-
- // keyword declarations
- case List(Keyword.Command_Decl(name, kind)) => syntax += (name, kind)
- case List(Keyword.Keyword_Decl(name)) => syntax += name
-
- case _ => if (!result.is_ready) bad_result(result)
- }
- }
- else if (result.kind == Markup.EXIT)
- prover = null
- else if (result.is_raw)
- raw_output.event(result)
- else if (!result.is_system) // FIXME syslog (!?)
- bad_result(result)
}
//}}}
@@ -278,7 +253,7 @@
def flush()
{
- if (!changed.isEmpty) commands_changed.event(Command_Set(changed))
+ if (!changed.isEmpty) commands_changed.event(Session.Commands_Changed(changed))
changed = Set()
flush_time = None
}
@@ -315,25 +290,56 @@
private val editor_history = new Actor
{
- @volatile private var history = Document.Change.init
- def current_change(): Document.Change = history
+ @volatile private var history = List(Document.Change.init)
+
+ def snapshot(name: String, pending_edits: List[Text_Edit]): Document.Snapshot =
+ {
+ val state_snapshot = current_state()
+ val history_snapshot = history
+
+ val found_stable = history_snapshot.find(change =>
+ change.is_finished && state_snapshot.is_assigned(change.document.join))
+ require(found_stable.isDefined)
+ val stable = found_stable.get
+ val latest = history_snapshot.head
+
+ val edits =
+ (pending_edits /: history_snapshot.takeWhile(_ != stable))((edits, change) =>
+ (for ((a, eds) <- change.edits if a == name) yield eds).flatten ::: edits)
+ lazy val reverse_edits = edits.reverse
+
+ new Document.Snapshot {
+ val document = stable.document.join
+ val node = document.nodes(name)
+ val is_outdated = !(pending_edits.isEmpty && latest == stable)
+ def convert(offset: Int): Int = (offset /: edits)((i, edit) => edit.convert(i))
+ def revert(offset: Int): Int = (offset /: reverse_edits)((i, edit) => edit.revert(i))
+ def lookup_command(id: Document.Command_ID): Option[Command] =
+ state_snapshot.lookup_command(id)
+ def state(command: Command): Command.State =
+ try { state_snapshot.command_state(document, command) }
+ catch { case _: Document.State.Fail => command.empty_state }
+ }
+ }
def act
{
loop {
react {
case Edit_Document(edits) =>
- val old_change = history
- val new_id = create_id()
+ val history_snapshot = history
+ require(!history_snapshot.isEmpty)
+
+ val prev = history_snapshot.head.document
val result: isabelle.Future[(List[Document.Edit[Command]], Document)] =
isabelle.Future.fork {
- val old_doc = old_change.join_document
- old_doc.await_assignment
- Document.text_edits(Session.this, old_doc, new_id, edits)
+ val old_doc = prev.join
+ val former_assignment = current_state().the_assignment(old_doc).join // FIXME async!?
+ Thy_Syntax.text_edits(Session.this, old_doc, edits)
}
- val new_change = new Document.Change(new_id, Some(old_change), edits, result)
- history = new_change
- new_change.result.map(_ => session_actor ! new_change)
+ val new_change = new Document.Change(prev, edits, result)
+ history ::= new_change
+ new_change.document.map(_ => session_actor ! new_change)
reply(())
case bad => System.err.println("editor_model: ignoring bad message " + bad)
@@ -352,7 +358,8 @@
def stop() { session_actor ! Stop }
- def current_change(): Document.Change = editor_history.current_change()
+ def snapshot(name: String, pending_edits: List[Text_Edit]): Document.Snapshot =
+ editor_history.snapshot(name, pending_edits)
def edit_document(edits: List[Document.Node_Text_Edit]) { editor_history !? Edit_Document(edits) }
}
--- a/src/Pure/Thy/thy_syntax.scala Mon Aug 16 10:32:35 2010 +0200
+++ b/src/Pure/Thy/thy_syntax.scala Mon Aug 16 10:32:45 2010 +0200
@@ -1,22 +1,23 @@
/* Title: Pure/Thy/thy_syntax.scala
Author: Makarius
-Superficial theory syntax: command spans.
+Superficial theory syntax: tokens and spans.
*/
package isabelle
import scala.collection.mutable
+import scala.annotation.tailrec
object Thy_Syntax
{
- type Span = List[Token]
+ /** parse spans **/
- def parse_spans(toks: List[Token]): List[Span] =
+ def parse_spans(toks: List[Token]): List[List[Token]] =
{
- val result = new mutable.ListBuffer[Span]
+ val result = new mutable.ListBuffer[List[Token]]
val span = new mutable.ListBuffer[Token]
val whitespace = new mutable.ListBuffer[Token]
@@ -32,4 +33,101 @@
flush(span); flush(whitespace)
result.toList
}
+
+
+
+ /** text edits **/
+
+ def text_edits(session: Session, old_doc: Document, edits: List[Document.Node_Text_Edit])
+ : (List[Document.Edit[Command]], Document) =
+ {
+ /* phase 1: edit individual command source */
+
+ @tailrec def edit_text(eds: List[Text_Edit], commands: Linear_Set[Command])
+ : Linear_Set[Command] =
+ {
+ eds match {
+ case e :: es =>
+ Document.Node.command_starts(commands.iterator).find {
+ case (cmd, cmd_start) =>
+ e.can_edit(cmd.source, cmd_start) ||
+ e.is_insert && e.start == cmd_start + cmd.length
+ } match {
+ case Some((cmd, cmd_start)) if e.can_edit(cmd.source, cmd_start) =>
+ val (rest, text) = e.edit(cmd.source, cmd_start)
+ val new_commands = commands.insert_after(Some(cmd), Command.unparsed(text)) - cmd
+ edit_text(rest.toList ::: es, new_commands)
+
+ case Some((cmd, cmd_start)) =>
+ edit_text(es, commands.insert_after(Some(cmd), Command.unparsed(e.text)))
+
+ case None =>
+ require(e.is_insert && e.start == 0)
+ edit_text(es, commands.insert_after(None, Command.unparsed(e.text)))
+ }
+ case Nil => commands
+ }
+ }
+
+
+ /* phase 2: recover command spans */
+
+ @tailrec def recover_spans(commands: Linear_Set[Command]): Linear_Set[Command] =
+ {
+ commands.iterator.find(_.is_unparsed) match {
+ case Some(first_unparsed) =>
+ val first =
+ commands.reverse_iterator(first_unparsed).find(_.is_command) getOrElse commands.head
+ val last =
+ commands.iterator(first_unparsed).find(_.is_command) getOrElse commands.last
+ val range =
+ commands.iterator(first).takeWhile(_ != last).toList ::: List(last)
+
+ val sources = range.flatMap(_.span.map(_.source))
+ val spans0 = parse_spans(session.current_syntax.scan(sources.mkString))
+
+ val (before_edit, spans1) =
+ if (!spans0.isEmpty && first.is_command && first.span == spans0.head)
+ (Some(first), spans0.tail)
+ else (commands.prev(first), spans0)
+
+ val (after_edit, spans2) =
+ if (!spans1.isEmpty && last.is_command && last.span == spans1.last)
+ (Some(last), spans1.take(spans1.length - 1))
+ else (commands.next(last), spans1)
+
+ val inserted = spans2.map(span => new Command(session.create_id(), span))
+ val new_commands =
+ commands.delete_between(before_edit, after_edit).append_after(before_edit, inserted)
+ recover_spans(new_commands)
+
+ case None => commands
+ }
+ }
+
+
+ /* resulting document edits */
+
+ {
+ val doc_edits = new mutable.ListBuffer[Document.Edit[Command]]
+ var nodes = old_doc.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
+
+ 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)))
+
+ doc_edits += (name -> Some(cmd_edits))
+ nodes += (name -> new Document.Node(commands2))
+ }
+ (doc_edits.toList, new Document(session.create_id(), nodes))
+ }
+ }
}
--- a/src/Pure/build-jars Mon Aug 16 10:32:35 2010 +0200
+++ b/src/Pure/build-jars Mon Aug 16 10:32:45 2010 +0200
@@ -33,7 +33,6 @@
General/xml.scala
General/xml_data.scala
General/yxml.scala
- Isar/isar_document.scala
Isar/keyword.scala
Isar/outer_syntax.scala
Isar/parse.scala
@@ -42,7 +41,6 @@
PIDE/document.scala
PIDE/event_bus.scala
PIDE/markup_node.scala
- PIDE/state.scala
PIDE/text_edit.scala
System/cygwin.scala
System/download.scala
@@ -50,6 +48,7 @@
System/isabelle_process.scala
System/isabelle_syntax.scala
System/isabelle_system.scala
+ System/isar_document.scala
System/platform.scala
System/session.scala
System/session_manager.scala
--- a/src/Tools/jEdit/src/jedit/document_model.scala Mon Aug 16 10:32:35 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/document_model.scala Mon Aug 16 10:32:45 2010 +0200
@@ -227,7 +227,7 @@
def snapshot(): Document.Snapshot = {
Swing_Thread.require()
- session.current_change().snapshot(thy_name, pending_edits.snapshot())
+ session.snapshot(thy_name, pending_edits.snapshot())
}
@@ -278,7 +278,7 @@
for {
(command, command_start) <-
snapshot.node.command_range(snapshot.revert(start), snapshot.revert(stop))
- markup <- snapshot.document.current_state(command).highlight.flatten
+ markup <- snapshot.state(command).highlight.flatten
val abs_start = snapshot.convert(command_start + markup.start)
val abs_stop = snapshot.convert(command_start + markup.stop)
if (abs_stop > start)
--- a/src/Tools/jEdit/src/jedit/document_view.scala Mon Aug 16 10:32:35 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/document_view.scala Mon Aug 16 10:32:45 2010 +0200
@@ -26,7 +26,7 @@
{
def choose_color(snapshot: Document.Snapshot, command: Command): Color =
{
- val state = snapshot.document.current_state(command)
+ val state = snapshot.state(command)
if (snapshot.is_outdated) new Color(240, 240, 240)
else if (state.forks > 0) new Color(255, 228, 225)
else if (state.forks < 0) Color.red
@@ -103,7 +103,7 @@
private val commands_changed_actor = actor {
loop {
react {
- case Command_Set(changed) =>
+ case Session.Commands_Changed(changed) =>
Swing_Thread.now {
// FIXME cover doc states as well!!?
val snapshot = model.snapshot()
@@ -203,7 +203,7 @@
val offset = snapshot.revert(text_area.xyToOffset(x, y))
snapshot.node.command_at(offset) match {
case Some((command, command_start)) =>
- snapshot.document.current_state(command).type_at(offset - command_start) match {
+ snapshot.state(command).type_at(offset - command_start) match {
case Some(text) => Isabelle.tooltip(text)
case None => null
}
--- a/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala Mon Aug 16 10:32:35 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala Mon Aug 16 10:32:45 2010 +0200
@@ -47,7 +47,7 @@
val offset = snapshot.revert(original_offset)
snapshot.node.command_at(offset) match {
case Some((command, command_start)) =>
- snapshot.document.current_state(command).ref_at(offset - command_start) match {
+ snapshot.state(command).ref_at(offset - command_start) match {
case Some(ref) =>
val begin = snapshot.convert(command_start + ref.start)
val line = buffer.getLineOfOffset(begin)
@@ -56,8 +56,8 @@
case Command.RefInfo(Some(ref_file), Some(ref_line), _, _) =>
new External_Hyperlink(begin, end, line, ref_file, ref_line)
case Command.RefInfo(_, _, Some(id), Some(offset)) =>
- Isabelle.session.lookup_entity(id) match {
- case Some(ref_cmd: Command) =>
+ snapshot.lookup_command(id) match { // FIXME Command_ID vs. Exec_ID (!??)
+ case Some(ref_cmd) =>
snapshot.node.command_start(ref_cmd) match {
case Some(ref_cmd_start) =>
new Internal_Hyperlink(begin, end, line,
--- a/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala Mon Aug 16 10:32:35 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala Mon Aug 16 10:32:45 2010 +0200
@@ -130,7 +130,7 @@
val root = data.root
val snapshot = Swing_Thread.now { model.snapshot() } // FIXME cover all nodes (!??)
for ((command, command_start) <- snapshot.node.command_range(0) if !stopped) {
- root.add(snapshot.document.current_state(command).markup_root.swing_tree((node: Markup_Node) =>
+ root.add(snapshot.state(command).markup.swing_tree((node: Markup_Node) =>
{
val content = command.source(node.start, node.stop).replace('\n', ' ')
val id = command.id
@@ -139,7 +139,7 @@
override def getIcon: Icon = null
override def getShortString: String = content
override def getLongString: String = node.info.toString
- override def getName: String = id
+ override def getName: String = Markup.Long(id)
override def setName(name: String) = ()
override def setStart(start: Position) = ()
override def getStart: Position = command_start + node.start
--- a/src/Tools/jEdit/src/jedit/output_dockable.scala Mon Aug 16 10:32:35 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/output_dockable.scala Mon Aug 16 10:32:45 2010 +0200
@@ -67,7 +67,7 @@
case Some(cmd) if !restriction.isDefined || restriction.get.contains(cmd) =>
val snapshot = doc_view.model.snapshot()
val filtered_results =
- snapshot.document.current_state(cmd).results filter {
+ snapshot.state(cmd).results filter {
case XML.Elem(Markup(Markup.TRACING, _), _) => show_tracing
case XML.Elem(Markup(Markup.DEBUG, _), _) => show_debug
case _ => true
@@ -87,7 +87,7 @@
loop {
react {
case Session.Global_Settings => handle_resize()
- case Command_Set(changed) => handle_update(Some(changed))
+ case Session.Commands_Changed(changed) => handle_update(Some(changed))
case Session.Perspective => if (follow_caret && handle_perspective()) handle_update()
case bad => System.err.println("Output_Dockable: ignoring bad message " + bad)
}