moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
authorwenzelm
Sat Aug 14 18:43:45 2010 +0200 (2010-08-14)
changeset 38412c23f3abbf42d
parent 38411 001f2f44984c
child 38413 224efb14f258
moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
src/Pure/IsaMakefile
src/Pure/Isar/isar_document.ML
src/Pure/Isar/isar_document.scala
src/Pure/ROOT.ML
src/Pure/System/isar_document.ML
src/Pure/System/isar_document.scala
src/Pure/build-jars
     1.1 --- a/src/Pure/IsaMakefile	Sat Aug 14 13:24:06 2010 +0200
     1.2 +++ b/src/Pure/IsaMakefile	Sat Aug 14 18:43:45 2010 +0200
     1.3 @@ -119,7 +119,6 @@
     1.4    Isar/expression.ML					\
     1.5    Isar/generic_target.ML				\
     1.6    Isar/isar_cmd.ML					\
     1.7 -  Isar/isar_document.ML					\
     1.8    Isar/isar_syn.ML					\
     1.9    Isar/keyword.ML					\
    1.10    Isar/local_defs.ML					\
    1.11 @@ -191,6 +190,7 @@
    1.12    Syntax/type_ext.ML					\
    1.13    System/isabelle_process.ML				\
    1.14    System/isar.ML					\
    1.15 +  System/isar_document.ML				\
    1.16    System/session.ML					\
    1.17    Thy/html.ML						\
    1.18    Thy/latex.ML						\
     2.1 --- a/src/Pure/Isar/isar_document.ML	Sat Aug 14 13:24:06 2010 +0200
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,297 +0,0 @@
     2.4 -(*  Title:      Pure/Isar/isar_document.ML
     2.5 -    Author:     Makarius
     2.6 -
     2.7 -Interactive Isar documents, which are structured as follows:
     2.8 -
     2.9 -  - history: tree of documents (i.e. changes without merge)
    2.10 -  - document: graph of nodes (cf. theory files)
    2.11 -  - node: linear set of commands, potentially with proof structure
    2.12 -*)
    2.13 -
    2.14 -structure Isar_Document: sig end =
    2.15 -struct
    2.16 -
    2.17 -(* unique identifiers *)
    2.18 -
    2.19 -local
    2.20 -  val id_count = Synchronized.var "id" 0;
    2.21 -in
    2.22 -  fun create_id () =
    2.23 -    Synchronized.change_result id_count
    2.24 -      (fn i =>
    2.25 -        let val i' = i + 1
    2.26 -        in (i', i') end);
    2.27 -end;
    2.28 -
    2.29 -fun err_dup kind id = error ("Duplicate " ^ kind ^ ": " ^ Document.print_id id);
    2.30 -fun err_undef kind id = error ("Undefined " ^ kind ^ ": " ^ Document.print_id id);
    2.31 -
    2.32 -
    2.33 -(** documents **)
    2.34 -
    2.35 -datatype entry = Entry of {next: Document.command_id option, exec: Document.exec_id option};
    2.36 -type node = entry Inttab.table; (*unique command entries indexed by command_id, start with no_id*)
    2.37 -type document = node Graph.T;   (*development graph via static imports*)
    2.38 -
    2.39 -
    2.40 -(* command entries *)
    2.41 -
    2.42 -fun make_entry next exec = Entry {next = next, exec = exec};
    2.43 -
    2.44 -fun the_entry (node: node) (id: Document.command_id) =
    2.45 -  (case Inttab.lookup node id of
    2.46 -    NONE => err_undef "command entry" id
    2.47 -  | SOME (Entry entry) => entry);
    2.48 -
    2.49 -fun put_entry (id: Document.command_id, entry: entry) = Inttab.update (id, entry);
    2.50 -
    2.51 -fun put_entry_exec (id: Document.command_id) exec (node: node) =
    2.52 -  let val {next, ...} = the_entry node id
    2.53 -  in put_entry (id, make_entry next exec) node end;
    2.54 -
    2.55 -fun reset_entry_exec id = put_entry_exec id NONE;
    2.56 -fun set_entry_exec (id, exec_id) = put_entry_exec id (SOME exec_id);
    2.57 -
    2.58 -
    2.59 -(* iterate entries *)
    2.60 -
    2.61 -fun fold_entries id0 f (node: node) =
    2.62 -  let
    2.63 -    fun apply NONE x = x
    2.64 -      | apply (SOME id) x =
    2.65 -          let val entry = the_entry node id
    2.66 -          in apply (#next entry) (f (id, entry) x) end;
    2.67 -  in if Inttab.defined node id0 then apply (SOME id0) else I end;
    2.68 -
    2.69 -fun first_entry P (node: node) =
    2.70 -  let
    2.71 -    fun first _ NONE = NONE
    2.72 -      | first prev (SOME id) =
    2.73 -          let val entry = the_entry node id
    2.74 -          in if P (id, entry) then SOME (prev, id, entry) else first (SOME id) (#next entry) end;
    2.75 -  in first NONE (SOME Document.no_id) end;
    2.76 -
    2.77 -
    2.78 -(* modify entries *)
    2.79 -
    2.80 -fun insert_after (id: Document.command_id) (id2: Document.command_id) (node: node) =
    2.81 -  let val {next, exec} = the_entry node id in
    2.82 -    node
    2.83 -    |> put_entry (id, make_entry (SOME id2) exec)
    2.84 -    |> put_entry (id2, make_entry next NONE)
    2.85 -  end;
    2.86 -
    2.87 -fun delete_after (id: Document.command_id) (node: node) =
    2.88 -  let val {next, exec} = the_entry node id in
    2.89 -    (case next of
    2.90 -      NONE => error ("No next entry to delete: " ^ Document.print_id id)
    2.91 -    | SOME id2 =>
    2.92 -        node |>
    2.93 -          (case #next (the_entry node id2) of
    2.94 -            NONE => put_entry (id, make_entry NONE exec)
    2.95 -          | SOME id3 => put_entry (id, make_entry (SOME id3) exec) #> reset_entry_exec id3))
    2.96 -  end;
    2.97 -
    2.98 -
    2.99 -(* node operations *)
   2.100 -
   2.101 -val empty_node: node = Inttab.make [(Document.no_id, make_entry NONE (SOME Document.no_id))];
   2.102 -
   2.103 -fun the_node (document: document) name =
   2.104 -  Graph.get_node document name handle Graph.UNDEF _ => empty_node;
   2.105 -
   2.106 -fun edit_node (id, SOME id2) = insert_after id id2
   2.107 -  | edit_node (id, NONE) = delete_after id;
   2.108 -
   2.109 -fun edit_nodes (name, SOME edits) =
   2.110 -      Graph.default_node (name, empty_node) #>
   2.111 -      Graph.map_node name (fold edit_node edits)
   2.112 -  | edit_nodes (name, NONE) = Graph.del_node name;
   2.113 -
   2.114 -
   2.115 -
   2.116 -(** global configuration **)
   2.117 -
   2.118 -(* command executions *)
   2.119 -
   2.120 -local
   2.121 -
   2.122 -val global_execs =
   2.123 -  Unsynchronized.ref (Inttab.make [(Document.no_id, Lazy.value (SOME Toplevel.toplevel))]);
   2.124 -
   2.125 -in
   2.126 -
   2.127 -fun define_exec (id: Document.exec_id) exec =
   2.128 -  NAMED_CRITICAL "Isar" (fn () =>
   2.129 -    Unsynchronized.change global_execs (Inttab.update_new (id, exec))
   2.130 -      handle Inttab.DUP dup => err_dup "exec" dup);
   2.131 -
   2.132 -fun the_exec (id: Document.exec_id) =
   2.133 -  (case Inttab.lookup (! global_execs) id of
   2.134 -    NONE => err_undef "exec" id
   2.135 -  | SOME exec => exec);
   2.136 -
   2.137 -end;
   2.138 -
   2.139 -
   2.140 -(* commands *)
   2.141 -
   2.142 -local
   2.143 -
   2.144 -val global_commands = Unsynchronized.ref (Inttab.make [(Document.no_id, Toplevel.empty)]);
   2.145 -
   2.146 -in
   2.147 -
   2.148 -fun define_command (id: Document.command_id) text =
   2.149 -  let
   2.150 -    val id_string = Document.print_id id;
   2.151 -    val tr =
   2.152 -      Position.setmp_thread_data (Position.id_only id_string) (fn () =>
   2.153 -        Outer_Syntax.prepare_command (Position.id id_string) text) ();
   2.154 -  in
   2.155 -    NAMED_CRITICAL "Isar" (fn () =>
   2.156 -      Unsynchronized.change global_commands (Inttab.update_new (id, Toplevel.put_id id_string tr))
   2.157 -        handle Inttab.DUP dup => err_dup "command" dup)
   2.158 -  end;
   2.159 -
   2.160 -fun the_command (id: Document.command_id) =
   2.161 -  (case Inttab.lookup (! global_commands) id of
   2.162 -    NONE => err_undef "command" id
   2.163 -  | SOME tr => tr);
   2.164 -
   2.165 -end;
   2.166 -
   2.167 -
   2.168 -(* document versions *)
   2.169 -
   2.170 -local
   2.171 -
   2.172 -val global_documents = Unsynchronized.ref (Inttab.make [(Document.no_id, Graph.empty: document)]);
   2.173 -
   2.174 -in
   2.175 -
   2.176 -fun define_document (id: Document.version_id) document =
   2.177 -  NAMED_CRITICAL "Isar" (fn () =>
   2.178 -    Unsynchronized.change global_documents (Inttab.update_new (id, document))
   2.179 -      handle Inttab.DUP dup => err_dup "document" dup);
   2.180 -
   2.181 -fun the_document (id: Document.version_id) =
   2.182 -  (case Inttab.lookup (! global_documents) id of
   2.183 -    NONE => err_undef "document" id
   2.184 -  | SOME document => document);
   2.185 -
   2.186 -end;
   2.187 -
   2.188 -
   2.189 -
   2.190 -(** document editing **)
   2.191 -
   2.192 -(* execution *)
   2.193 -
   2.194 -local
   2.195 -
   2.196 -val execution: unit future list Unsynchronized.ref = Unsynchronized.ref [];
   2.197 -
   2.198 -fun force_exec NONE = ()
   2.199 -  | force_exec (SOME exec_id) = ignore (Lazy.force (the_exec exec_id));
   2.200 -
   2.201 -in
   2.202 -
   2.203 -fun execute document =
   2.204 -  NAMED_CRITICAL "Isar" (fn () =>
   2.205 -    let
   2.206 -      val old_execution = ! execution;
   2.207 -      val _ = List.app Future.cancel old_execution;
   2.208 -      fun await_cancellation () = uninterruptible (K Future.join_results) old_execution;
   2.209 -      (* FIXME proper node deps *)
   2.210 -      val new_execution = Graph.keys document |> map (fn name =>
   2.211 -        Future.fork_pri 1 (fn () =>
   2.212 -          let
   2.213 -            val _ = await_cancellation ();
   2.214 -            val exec =
   2.215 -              fold_entries Document.no_id (fn (_, {exec, ...}) => fn () => force_exec exec)
   2.216 -                (the_node document name);
   2.217 -          in exec () end));
   2.218 -    in execution := new_execution end);
   2.219 -
   2.220 -end;
   2.221 -
   2.222 -
   2.223 -(* editing *)
   2.224 -
   2.225 -local
   2.226 -
   2.227 -fun is_changed node' (id, {next = _, exec}) =
   2.228 -  (case try (the_entry node') id of
   2.229 -    NONE => true
   2.230 -  | SOME {next = _, exec = exec'} => exec' <> exec);
   2.231 -
   2.232 -fun new_exec name (id: Document.command_id) (exec_id, updates) =
   2.233 -  let
   2.234 -    val exec = the_exec exec_id;
   2.235 -    val exec_id' = create_id ();
   2.236 -    val tr = Toplevel.put_id (Document.print_id exec_id') (the_command id);
   2.237 -    val exec' =
   2.238 -      Lazy.lazy (fn () =>
   2.239 -        (case Lazy.force exec of
   2.240 -          NONE => NONE
   2.241 -        | SOME st => Toplevel.run_command name tr st));
   2.242 -    val _ = define_exec exec_id' exec';
   2.243 -  in (exec_id', (id, exec_id') :: updates) end;
   2.244 -
   2.245 -fun updates_status new_id updates =
   2.246 -  implode (map (fn (id, exec_id) =>
   2.247 -      Markup.markup (Markup.edit (Document.print_id id) (Document.print_id exec_id)) "") updates)
   2.248 -  |> Markup.markup Markup.assign
   2.249 -  |> Position.setmp_thread_data (Position.id_only (Document.print_id new_id)) Output.status;
   2.250 -  (*FIXME avoid setmp -- direct message argument*)
   2.251 -
   2.252 -in
   2.253 -
   2.254 -fun edit_document (old_id: Document.version_id) (new_id: Document.version_id) edits =
   2.255 -  NAMED_CRITICAL "Isar" (fn () =>
   2.256 -    let
   2.257 -      val old_document = the_document old_id;
   2.258 -      val new_document = fold edit_nodes edits old_document;
   2.259 -
   2.260 -      fun update_node name node =
   2.261 -        (case first_entry (is_changed (the_node old_document name)) node of
   2.262 -          NONE => ([], node)
   2.263 -        | SOME (prev, id, _) =>
   2.264 -            let
   2.265 -              val prev_exec_id = the (#exec (the_entry node (the prev)));
   2.266 -              val (_, updates) = fold_entries id (new_exec name o #1) node (prev_exec_id, []);
   2.267 -              val node' = fold set_entry_exec updates node;
   2.268 -            in (rev updates, node') end);
   2.269 -
   2.270 -      (* FIXME proper node deps *)
   2.271 -      val (updatess, new_document') =
   2.272 -        (Graph.keys new_document, new_document)
   2.273 -          |-> fold_map (fn name => Graph.map_node_yield name (update_node name));
   2.274 -
   2.275 -      val _ = define_document new_id new_document';
   2.276 -      val _ = updates_status new_id (flat updatess);
   2.277 -      val _ = execute new_document';
   2.278 -    in () end);
   2.279 -
   2.280 -end;
   2.281 -
   2.282 -
   2.283 -
   2.284 -(** Isabelle process commands **)
   2.285 -
   2.286 -val _ =
   2.287 -  Isabelle_Process.add_command "Isar_Document.define_command"
   2.288 -    (fn [id, text] => define_command (Document.parse_id id) text);
   2.289 -
   2.290 -val _ =
   2.291 -  Isabelle_Process.add_command "Isar_Document.edit_document"
   2.292 -    (fn [old_id, new_id, edits] =>
   2.293 -      edit_document (Document.parse_id old_id) (Document.parse_id new_id)
   2.294 -        (XML_Data.dest_list (XML_Data.dest_pair XML_Data.dest_string
   2.295 -            (XML_Data.dest_option (XML_Data.dest_list
   2.296 -                (XML_Data.dest_pair XML_Data.dest_int
   2.297 -                  (XML_Data.dest_option XML_Data.dest_int))))) (YXML.parse_body edits)));
   2.298 -
   2.299 -end;
   2.300 -
     3.1 --- a/src/Pure/Isar/isar_document.scala	Sat Aug 14 13:24:06 2010 +0200
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,67 +0,0 @@
     3.4 -/*  Title:      Pure/Isar/isar_document.scala
     3.5 -    Author:     Makarius
     3.6 -
     3.7 -Interactive Isar documents.
     3.8 -*/
     3.9 -
    3.10 -package isabelle
    3.11 -
    3.12 -
    3.13 -object Isar_Document
    3.14 -{
    3.15 -  /* protocol messages */
    3.16 -
    3.17 -  object Assign {
    3.18 -    def unapply(msg: XML.Tree): Option[List[(Document.Command_ID, Document.Exec_ID)]] =
    3.19 -      msg match {
    3.20 -        case XML.Elem(Markup.Assign, edits) =>
    3.21 -          val id_edits = edits.map(Edit.unapply)
    3.22 -          if (id_edits.forall(_.isDefined)) Some(id_edits.map(_.get))
    3.23 -          else None
    3.24 -        case _ => None
    3.25 -      }
    3.26 -  }
    3.27 -
    3.28 -  object Edit {
    3.29 -    def unapply(msg: XML.Tree): Option[(Document.Command_ID, Document.Exec_ID)] =
    3.30 -      msg match {
    3.31 -        case XML.Elem(Markup(Markup.EDIT, List((Markup.ID, cmd_id), (Markup.STATE, state_id))), Nil) =>
    3.32 -          (Markup.parse_long(cmd_id), Markup.parse_long(state_id)) match {
    3.33 -            case (Some(i), Some(j)) => Some((i, j))
    3.34 -            case _ => None
    3.35 -          }
    3.36 -        case _ => None
    3.37 -      }
    3.38 -  }
    3.39 -}
    3.40 -
    3.41 -
    3.42 -trait Isar_Document extends Isabelle_Process
    3.43 -{
    3.44 -  import Isar_Document._
    3.45 -
    3.46 -
    3.47 -  /* commands */
    3.48 -
    3.49 -  def define_command(id: Document.Command_ID, text: String): Unit =
    3.50 -    input("Isar_Document.define_command", Document.print_id(id), text)
    3.51 -
    3.52 -
    3.53 -  /* documents */
    3.54 -
    3.55 -  def edit_document(old_id: Document.Version_ID, new_id: Document.Version_ID,
    3.56 -      edits: List[Document.Edit[Document.Command_ID]])
    3.57 -  {
    3.58 -    def make_id1(id1: Option[Document.Command_ID]): XML.Body =
    3.59 -      XML_Data.make_long(id1 getOrElse Document.NO_ID)
    3.60 -
    3.61 -    val arg =
    3.62 -      XML_Data.make_list(
    3.63 -        XML_Data.make_pair(XML_Data.make_string)(
    3.64 -          XML_Data.make_option(XML_Data.make_list(
    3.65 -              XML_Data.make_pair(make_id1)(XML_Data.make_option(XML_Data.make_long))))))(edits)
    3.66 -
    3.67 -    input("Isar_Document.edit_document",
    3.68 -      Document.print_id(old_id), Document.print_id(new_id), YXML.string_of_body(arg))
    3.69 -  }
    3.70 -}
     4.1 --- a/src/Pure/ROOT.ML	Sat Aug 14 13:24:06 2010 +0200
     4.2 +++ b/src/Pure/ROOT.ML	Sat Aug 14 18:43:45 2010 +0200
     4.3 @@ -255,9 +255,9 @@
     4.4  (* Isabelle/Isar system *)
     4.5  
     4.6  use "System/session.ML";
     4.7 +use "System/isabelle_process.ML";
     4.8 +use "System/isar_document.ML";
     4.9  use "System/isar.ML";
    4.10 -use "System/isabelle_process.ML";
    4.11 -use "Isar/isar_document.ML";
    4.12  
    4.13  
    4.14  (* miscellaneous tools and packages for Pure Isabelle *)
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/Pure/System/isar_document.ML	Sat Aug 14 18:43:45 2010 +0200
     5.3 @@ -0,0 +1,297 @@
     5.4 +(*  Title:      Pure/System/isar_document.ML
     5.5 +    Author:     Makarius
     5.6 +
     5.7 +Interactive Isar documents, which are structured as follows:
     5.8 +
     5.9 +  - history: tree of documents (i.e. changes without merge)
    5.10 +  - document: graph of nodes (cf. theory files)
    5.11 +  - node: linear set of commands, potentially with proof structure
    5.12 +*)
    5.13 +
    5.14 +structure Isar_Document: sig end =
    5.15 +struct
    5.16 +
    5.17 +(* unique identifiers *)
    5.18 +
    5.19 +local
    5.20 +  val id_count = Synchronized.var "id" 0;
    5.21 +in
    5.22 +  fun create_id () =
    5.23 +    Synchronized.change_result id_count
    5.24 +      (fn i =>
    5.25 +        let val i' = i + 1
    5.26 +        in (i', i') end);
    5.27 +end;
    5.28 +
    5.29 +fun err_dup kind id = error ("Duplicate " ^ kind ^ ": " ^ Document.print_id id);
    5.30 +fun err_undef kind id = error ("Undefined " ^ kind ^ ": " ^ Document.print_id id);
    5.31 +
    5.32 +
    5.33 +(** documents **)
    5.34 +
    5.35 +datatype entry = Entry of {next: Document.command_id option, exec: Document.exec_id option};
    5.36 +type node = entry Inttab.table; (*unique command entries indexed by command_id, start with no_id*)
    5.37 +type document = node Graph.T;   (*development graph via static imports*)
    5.38 +
    5.39 +
    5.40 +(* command entries *)
    5.41 +
    5.42 +fun make_entry next exec = Entry {next = next, exec = exec};
    5.43 +
    5.44 +fun the_entry (node: node) (id: Document.command_id) =
    5.45 +  (case Inttab.lookup node id of
    5.46 +    NONE => err_undef "command entry" id
    5.47 +  | SOME (Entry entry) => entry);
    5.48 +
    5.49 +fun put_entry (id: Document.command_id, entry: entry) = Inttab.update (id, entry);
    5.50 +
    5.51 +fun put_entry_exec (id: Document.command_id) exec (node: node) =
    5.52 +  let val {next, ...} = the_entry node id
    5.53 +  in put_entry (id, make_entry next exec) node end;
    5.54 +
    5.55 +fun reset_entry_exec id = put_entry_exec id NONE;
    5.56 +fun set_entry_exec (id, exec_id) = put_entry_exec id (SOME exec_id);
    5.57 +
    5.58 +
    5.59 +(* iterate entries *)
    5.60 +
    5.61 +fun fold_entries id0 f (node: node) =
    5.62 +  let
    5.63 +    fun apply NONE x = x
    5.64 +      | apply (SOME id) x =
    5.65 +          let val entry = the_entry node id
    5.66 +          in apply (#next entry) (f (id, entry) x) end;
    5.67 +  in if Inttab.defined node id0 then apply (SOME id0) else I end;
    5.68 +
    5.69 +fun first_entry P (node: node) =
    5.70 +  let
    5.71 +    fun first _ NONE = NONE
    5.72 +      | first prev (SOME id) =
    5.73 +          let val entry = the_entry node id
    5.74 +          in if P (id, entry) then SOME (prev, id, entry) else first (SOME id) (#next entry) end;
    5.75 +  in first NONE (SOME Document.no_id) end;
    5.76 +
    5.77 +
    5.78 +(* modify entries *)
    5.79 +
    5.80 +fun insert_after (id: Document.command_id) (id2: Document.command_id) (node: node) =
    5.81 +  let val {next, exec} = the_entry node id in
    5.82 +    node
    5.83 +    |> put_entry (id, make_entry (SOME id2) exec)
    5.84 +    |> put_entry (id2, make_entry next NONE)
    5.85 +  end;
    5.86 +
    5.87 +fun delete_after (id: Document.command_id) (node: node) =
    5.88 +  let val {next, exec} = the_entry node id in
    5.89 +    (case next of
    5.90 +      NONE => error ("No next entry to delete: " ^ Document.print_id id)
    5.91 +    | SOME id2 =>
    5.92 +        node |>
    5.93 +          (case #next (the_entry node id2) of
    5.94 +            NONE => put_entry (id, make_entry NONE exec)
    5.95 +          | SOME id3 => put_entry (id, make_entry (SOME id3) exec) #> reset_entry_exec id3))
    5.96 +  end;
    5.97 +
    5.98 +
    5.99 +(* node operations *)
   5.100 +
   5.101 +val empty_node: node = Inttab.make [(Document.no_id, make_entry NONE (SOME Document.no_id))];
   5.102 +
   5.103 +fun the_node (document: document) name =
   5.104 +  Graph.get_node document name handle Graph.UNDEF _ => empty_node;
   5.105 +
   5.106 +fun edit_node (id, SOME id2) = insert_after id id2
   5.107 +  | edit_node (id, NONE) = delete_after id;
   5.108 +
   5.109 +fun edit_nodes (name, SOME edits) =
   5.110 +      Graph.default_node (name, empty_node) #>
   5.111 +      Graph.map_node name (fold edit_node edits)
   5.112 +  | edit_nodes (name, NONE) = Graph.del_node name;
   5.113 +
   5.114 +
   5.115 +
   5.116 +(** global configuration **)
   5.117 +
   5.118 +(* command executions *)
   5.119 +
   5.120 +local
   5.121 +
   5.122 +val global_execs =
   5.123 +  Unsynchronized.ref (Inttab.make [(Document.no_id, Lazy.value (SOME Toplevel.toplevel))]);
   5.124 +
   5.125 +in
   5.126 +
   5.127 +fun define_exec (id: Document.exec_id) exec =
   5.128 +  NAMED_CRITICAL "Isar" (fn () =>
   5.129 +    Unsynchronized.change global_execs (Inttab.update_new (id, exec))
   5.130 +      handle Inttab.DUP dup => err_dup "exec" dup);
   5.131 +
   5.132 +fun the_exec (id: Document.exec_id) =
   5.133 +  (case Inttab.lookup (! global_execs) id of
   5.134 +    NONE => err_undef "exec" id
   5.135 +  | SOME exec => exec);
   5.136 +
   5.137 +end;
   5.138 +
   5.139 +
   5.140 +(* commands *)
   5.141 +
   5.142 +local
   5.143 +
   5.144 +val global_commands = Unsynchronized.ref (Inttab.make [(Document.no_id, Toplevel.empty)]);
   5.145 +
   5.146 +in
   5.147 +
   5.148 +fun define_command (id: Document.command_id) text =
   5.149 +  let
   5.150 +    val id_string = Document.print_id id;
   5.151 +    val tr =
   5.152 +      Position.setmp_thread_data (Position.id_only id_string) (fn () =>
   5.153 +        Outer_Syntax.prepare_command (Position.id id_string) text) ();
   5.154 +  in
   5.155 +    NAMED_CRITICAL "Isar" (fn () =>
   5.156 +      Unsynchronized.change global_commands (Inttab.update_new (id, Toplevel.put_id id_string tr))
   5.157 +        handle Inttab.DUP dup => err_dup "command" dup)
   5.158 +  end;
   5.159 +
   5.160 +fun the_command (id: Document.command_id) =
   5.161 +  (case Inttab.lookup (! global_commands) id of
   5.162 +    NONE => err_undef "command" id
   5.163 +  | SOME tr => tr);
   5.164 +
   5.165 +end;
   5.166 +
   5.167 +
   5.168 +(* document versions *)
   5.169 +
   5.170 +local
   5.171 +
   5.172 +val global_documents = Unsynchronized.ref (Inttab.make [(Document.no_id, Graph.empty: document)]);
   5.173 +
   5.174 +in
   5.175 +
   5.176 +fun define_document (id: Document.version_id) document =
   5.177 +  NAMED_CRITICAL "Isar" (fn () =>
   5.178 +    Unsynchronized.change global_documents (Inttab.update_new (id, document))
   5.179 +      handle Inttab.DUP dup => err_dup "document" dup);
   5.180 +
   5.181 +fun the_document (id: Document.version_id) =
   5.182 +  (case Inttab.lookup (! global_documents) id of
   5.183 +    NONE => err_undef "document" id
   5.184 +  | SOME document => document);
   5.185 +
   5.186 +end;
   5.187 +
   5.188 +
   5.189 +
   5.190 +(** document editing **)
   5.191 +
   5.192 +(* execution *)
   5.193 +
   5.194 +local
   5.195 +
   5.196 +val execution: unit future list Unsynchronized.ref = Unsynchronized.ref [];
   5.197 +
   5.198 +fun force_exec NONE = ()
   5.199 +  | force_exec (SOME exec_id) = ignore (Lazy.force (the_exec exec_id));
   5.200 +
   5.201 +in
   5.202 +
   5.203 +fun execute document =
   5.204 +  NAMED_CRITICAL "Isar" (fn () =>
   5.205 +    let
   5.206 +      val old_execution = ! execution;
   5.207 +      val _ = List.app Future.cancel old_execution;
   5.208 +      fun await_cancellation () = uninterruptible (K Future.join_results) old_execution;
   5.209 +      (* FIXME proper node deps *)
   5.210 +      val new_execution = Graph.keys document |> map (fn name =>
   5.211 +        Future.fork_pri 1 (fn () =>
   5.212 +          let
   5.213 +            val _ = await_cancellation ();
   5.214 +            val exec =
   5.215 +              fold_entries Document.no_id (fn (_, {exec, ...}) => fn () => force_exec exec)
   5.216 +                (the_node document name);
   5.217 +          in exec () end));
   5.218 +    in execution := new_execution end);
   5.219 +
   5.220 +end;
   5.221 +
   5.222 +
   5.223 +(* editing *)
   5.224 +
   5.225 +local
   5.226 +
   5.227 +fun is_changed node' (id, {next = _, exec}) =
   5.228 +  (case try (the_entry node') id of
   5.229 +    NONE => true
   5.230 +  | SOME {next = _, exec = exec'} => exec' <> exec);
   5.231 +
   5.232 +fun new_exec name (id: Document.command_id) (exec_id, updates) =
   5.233 +  let
   5.234 +    val exec = the_exec exec_id;
   5.235 +    val exec_id' = create_id ();
   5.236 +    val tr = Toplevel.put_id (Document.print_id exec_id') (the_command id);
   5.237 +    val exec' =
   5.238 +      Lazy.lazy (fn () =>
   5.239 +        (case Lazy.force exec of
   5.240 +          NONE => NONE
   5.241 +        | SOME st => Toplevel.run_command name tr st));
   5.242 +    val _ = define_exec exec_id' exec';
   5.243 +  in (exec_id', (id, exec_id') :: updates) end;
   5.244 +
   5.245 +fun updates_status new_id updates =
   5.246 +  implode (map (fn (id, exec_id) =>
   5.247 +      Markup.markup (Markup.edit (Document.print_id id) (Document.print_id exec_id)) "") updates)
   5.248 +  |> Markup.markup Markup.assign
   5.249 +  |> Position.setmp_thread_data (Position.id_only (Document.print_id new_id)) Output.status;
   5.250 +  (*FIXME avoid setmp -- direct message argument*)
   5.251 +
   5.252 +in
   5.253 +
   5.254 +fun edit_document (old_id: Document.version_id) (new_id: Document.version_id) edits =
   5.255 +  NAMED_CRITICAL "Isar" (fn () =>
   5.256 +    let
   5.257 +      val old_document = the_document old_id;
   5.258 +      val new_document = fold edit_nodes edits old_document;
   5.259 +
   5.260 +      fun update_node name node =
   5.261 +        (case first_entry (is_changed (the_node old_document name)) node of
   5.262 +          NONE => ([], node)
   5.263 +        | SOME (prev, id, _) =>
   5.264 +            let
   5.265 +              val prev_exec_id = the (#exec (the_entry node (the prev)));
   5.266 +              val (_, updates) = fold_entries id (new_exec name o #1) node (prev_exec_id, []);
   5.267 +              val node' = fold set_entry_exec updates node;
   5.268 +            in (rev updates, node') end);
   5.269 +
   5.270 +      (* FIXME proper node deps *)
   5.271 +      val (updatess, new_document') =
   5.272 +        (Graph.keys new_document, new_document)
   5.273 +          |-> fold_map (fn name => Graph.map_node_yield name (update_node name));
   5.274 +
   5.275 +      val _ = define_document new_id new_document';
   5.276 +      val _ = updates_status new_id (flat updatess);
   5.277 +      val _ = execute new_document';
   5.278 +    in () end);
   5.279 +
   5.280 +end;
   5.281 +
   5.282 +
   5.283 +
   5.284 +(** Isabelle process commands **)
   5.285 +
   5.286 +val _ =
   5.287 +  Isabelle_Process.add_command "Isar_Document.define_command"
   5.288 +    (fn [id, text] => define_command (Document.parse_id id) text);
   5.289 +
   5.290 +val _ =
   5.291 +  Isabelle_Process.add_command "Isar_Document.edit_document"
   5.292 +    (fn [old_id, new_id, edits] =>
   5.293 +      edit_document (Document.parse_id old_id) (Document.parse_id new_id)
   5.294 +        (XML_Data.dest_list (XML_Data.dest_pair XML_Data.dest_string
   5.295 +            (XML_Data.dest_option (XML_Data.dest_list
   5.296 +                (XML_Data.dest_pair XML_Data.dest_int
   5.297 +                  (XML_Data.dest_option XML_Data.dest_int))))) (YXML.parse_body edits)));
   5.298 +
   5.299 +end;
   5.300 +
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/src/Pure/System/isar_document.scala	Sat Aug 14 18:43:45 2010 +0200
     6.3 @@ -0,0 +1,67 @@
     6.4 +/*  Title:      Pure/System/isar_document.scala
     6.5 +    Author:     Makarius
     6.6 +
     6.7 +Interactive Isar documents.
     6.8 +*/
     6.9 +
    6.10 +package isabelle
    6.11 +
    6.12 +
    6.13 +object Isar_Document
    6.14 +{
    6.15 +  /* protocol messages */
    6.16 +
    6.17 +  object Assign {
    6.18 +    def unapply(msg: XML.Tree): Option[List[(Document.Command_ID, Document.Exec_ID)]] =
    6.19 +      msg match {
    6.20 +        case XML.Elem(Markup.Assign, edits) =>
    6.21 +          val id_edits = edits.map(Edit.unapply)
    6.22 +          if (id_edits.forall(_.isDefined)) Some(id_edits.map(_.get))
    6.23 +          else None
    6.24 +        case _ => None
    6.25 +      }
    6.26 +  }
    6.27 +
    6.28 +  object Edit {
    6.29 +    def unapply(msg: XML.Tree): Option[(Document.Command_ID, Document.Exec_ID)] =
    6.30 +      msg match {
    6.31 +        case XML.Elem(Markup(Markup.EDIT, List((Markup.ID, cmd_id), (Markup.STATE, state_id))), Nil) =>
    6.32 +          (Markup.parse_long(cmd_id), Markup.parse_long(state_id)) match {
    6.33 +            case (Some(i), Some(j)) => Some((i, j))
    6.34 +            case _ => None
    6.35 +          }
    6.36 +        case _ => None
    6.37 +      }
    6.38 +  }
    6.39 +}
    6.40 +
    6.41 +
    6.42 +trait Isar_Document extends Isabelle_Process
    6.43 +{
    6.44 +  import Isar_Document._
    6.45 +
    6.46 +
    6.47 +  /* commands */
    6.48 +
    6.49 +  def define_command(id: Document.Command_ID, text: String): Unit =
    6.50 +    input("Isar_Document.define_command", Document.print_id(id), text)
    6.51 +
    6.52 +
    6.53 +  /* documents */
    6.54 +
    6.55 +  def edit_document(old_id: Document.Version_ID, new_id: Document.Version_ID,
    6.56 +      edits: List[Document.Edit[Document.Command_ID]])
    6.57 +  {
    6.58 +    def make_id1(id1: Option[Document.Command_ID]): XML.Body =
    6.59 +      XML_Data.make_long(id1 getOrElse Document.NO_ID)
    6.60 +
    6.61 +    val arg =
    6.62 +      XML_Data.make_list(
    6.63 +        XML_Data.make_pair(XML_Data.make_string)(
    6.64 +          XML_Data.make_option(XML_Data.make_list(
    6.65 +              XML_Data.make_pair(make_id1)(XML_Data.make_option(XML_Data.make_long))))))(edits)
    6.66 +
    6.67 +    input("Isar_Document.edit_document",
    6.68 +      Document.print_id(old_id), Document.print_id(new_id), YXML.string_of_body(arg))
    6.69 +  }
    6.70 +}
     7.1 --- a/src/Pure/build-jars	Sat Aug 14 13:24:06 2010 +0200
     7.2 +++ b/src/Pure/build-jars	Sat Aug 14 18:43:45 2010 +0200
     7.3 @@ -33,7 +33,6 @@
     7.4    General/xml.scala
     7.5    General/xml_data.scala
     7.6    General/yxml.scala
     7.7 -  Isar/isar_document.scala
     7.8    Isar/keyword.scala
     7.9    Isar/outer_syntax.scala
    7.10    Isar/parse.scala
    7.11 @@ -49,6 +48,7 @@
    7.12    System/isabelle_process.scala
    7.13    System/isabelle_syntax.scala
    7.14    System/isabelle_system.scala
    7.15 +  System/isar_document.scala
    7.16    System/platform.scala
    7.17    System/session.scala
    7.18    System/session_manager.scala