# HG changeset patch # User haftmann # Date 1281947565 -7200 # Node ID 386fd5c0ccbfde6f36462d8d3ccc72788e2233f0 # Parent 9513c79ac4cc8f250d74ed9bd05dc49faeafad49# Parent 439f50a241c17fbb6066facf08eb3961c6a4035b merged diff -r 9513c79ac4cc -r 386fd5c0ccbf doc-src/TutorialI/ToyList/ToyList.thy --- 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} diff -r 9513c79ac4cc -r 386fd5c0ccbf doc-src/TutorialI/ToyList/document/ToyList.tex --- 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} diff -r 9513c79ac4cc -r 386fd5c0ccbf doc-src/TutorialI/ToyList2/ToyList1 --- 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" | diff -r 9513c79ac4cc -r 386fd5c0ccbf doc-src/TutorialI/basics.tex --- 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} diff -r 9513c79ac4cc -r 386fd5c0ccbf src/Pure/General/linear_set.scala --- 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 diff -r 9513c79ac4cc -r 386fd5c0ccbf src/Pure/General/markup.ML --- 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 *) diff -r 9513c79ac4cc -r 386fd5c0ccbf src/Pure/General/markup.scala --- 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" diff -r 9513c79ac4cc -r 386fd5c0ccbf src/Pure/General/position.scala --- 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) } } diff -r 9513c79ac4cc -r 386fd5c0ccbf src/Pure/General/pretty.scala --- 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 } } diff -r 9513c79ac4cc -r 386fd5c0ccbf src/Pure/General/scan.scala --- 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 */ diff -r 9513c79ac4cc -r 386fd5c0ccbf src/Pure/General/xml_data.scala --- 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)) diff -r 9513c79ac4cc -r 386fd5c0ccbf src/Pure/IsaMakefile --- 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 \ diff -r 9513c79ac4cc -r 386fd5c0ccbf src/Pure/Isar/isar_document.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; - diff -r 9513c79ac4cc -r 386fd5c0ccbf src/Pure/Isar/isar_document.scala --- 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)) - } -} diff -r 9513c79ac4cc -r 386fd5c0ccbf src/Pure/Isar/keyword.ML --- 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) diff -r 9513c79ac4cc -r 386fd5c0ccbf src/Pure/Isar/token.scala --- 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) diff -r 9513c79ac4cc -r 386fd5c0ccbf src/Pure/PIDE/command.scala --- 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)) } diff -r 9513c79ac4cc -r 386fd5c0ccbf src/Pure/PIDE/document.ML --- 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 *) diff -r 9513c79ac4cc -r 386fd5c0ccbf src/Pure/PIDE/document.scala --- 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) - } - } -} diff -r 9513c79ac4cc -r 386fd5c0ccbf src/Pure/PIDE/markup_node.scala --- 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) diff -r 9513c79ac4cc -r 386fd5c0ccbf src/Pure/PIDE/state.scala --- 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) - } -} diff -r 9513c79ac4cc -r 386fd5c0ccbf src/Pure/ROOT.ML --- 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 *) diff -r 9513c79ac4cc -r 386fd5c0ccbf src/Pure/System/isabelle_process.scala --- 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 } diff -r 9513c79ac4cc -r 386fd5c0ccbf src/Pure/System/isabelle_system.scala --- 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) } diff -r 9513c79ac4cc -r 386fd5c0ccbf src/Pure/System/isar_document.ML --- /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; + diff -r 9513c79ac4cc -r 386fd5c0ccbf src/Pure/System/isar_document.scala --- /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)) + } +} diff -r 9513c79ac4cc -r 386fd5c0ccbf src/Pure/System/session.scala --- 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) } } diff -r 9513c79ac4cc -r 386fd5c0ccbf src/Pure/Thy/thy_syntax.scala --- 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)) + } + } } diff -r 9513c79ac4cc -r 386fd5c0ccbf src/Pure/build-jars --- 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 diff -r 9513c79ac4cc -r 386fd5c0ccbf src/Tools/jEdit/src/jedit/document_model.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) diff -r 9513c79ac4cc -r 386fd5c0ccbf src/Tools/jEdit/src/jedit/document_view.scala --- 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 } diff -r 9513c79ac4cc -r 386fd5c0ccbf src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala --- 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, diff -r 9513c79ac4cc -r 386fd5c0ccbf src/Tools/jEdit/src/jedit/isabelle_sidekick.scala --- 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 diff -r 9513c79ac4cc -r 386fd5c0ccbf src/Tools/jEdit/src/jedit/output_dockable.scala --- 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) }