src/Pure/Isar/isar_document.ML
author wenzelm
Tue Sep 29 11:49:22 2009 +0200 (2009-09-29)
changeset 32738 15bb09ca0378
parent 32573 62b5b538408d
child 32793 24ba50c14ec5
permissions -rw-r--r--
explicit indication of Unsynchronized.ref;
     1 (*  Title:      Pure/Isar/isar_document.ML
     2     Author:     Makarius
     3 
     4 Interactive Isar documents.
     5 *)
     6 
     7 signature ISAR_DOCUMENT =
     8 sig
     9   type state_id = string
    10   type command_id = string
    11   type document_id = string
    12   val define_command: command_id -> Toplevel.transition -> unit
    13   val begin_document: document_id -> Path.T -> unit
    14   val end_document: document_id -> unit
    15   val edit_document: document_id -> document_id -> (command_id * command_id option) list -> unit
    16 end;
    17 
    18 structure Isar_Document: ISAR_DOCUMENT =
    19 struct
    20 
    21 (* unique identifiers *)
    22 
    23 type state_id = string;
    24 type command_id = string;
    25 type document_id = string;
    26 
    27 fun make_id () = "i" ^ serial_string ();
    28 
    29 fun err_dup kind id = error ("Duplicate " ^ kind ^ ": " ^ quote id);
    30 fun err_undef kind id = error ("Unknown " ^ kind ^ ": " ^ quote id);
    31 
    32 
    33 
    34 (** documents **)
    35 
    36 (* command entries *)
    37 
    38 datatype entry = Entry of {next: command_id option, state: state_id option};
    39 fun make_entry next state = Entry {next = next, state = state};
    40 
    41 fun the_entry entries (id: command_id) =
    42   (case Symtab.lookup entries id of
    43     NONE => err_undef "document entry" id
    44   | SOME (Entry entry) => entry);
    45 
    46 fun put_entry (id: command_id, entry: entry) = Symtab.update (id, entry);
    47 
    48 fun put_entry_state (id: command_id) state entries =
    49   let val {next, ...} = the_entry entries id
    50   in put_entry (id, make_entry next state) entries end;
    51 
    52 fun reset_entry_state id = put_entry_state id NONE;
    53 fun set_entry_state (id, state_id) = put_entry_state id (SOME state_id);
    54 
    55 
    56 (* document *)
    57 
    58 datatype document = Document of
    59  {dir: Path.T,                    (*master directory*)
    60   name: string,                   (*theory name*)
    61   start: command_id,              (*empty start command*)
    62   entries: entry Symtab.table};   (*unique command entries indexed by command_id*)
    63 
    64 fun make_document dir name start entries =
    65   Document {dir = dir, name = name, start = start, entries = entries};
    66 
    67 fun map_entries f (Document {dir, name, start, entries}) =
    68   make_document dir name start (f entries);
    69 
    70 
    71 (* iterate entries *)
    72 
    73 fun fold_entries id0 f (Document {entries, ...}) =
    74   let
    75     fun apply NONE x = x
    76       | apply (SOME id) x =
    77           let val entry = the_entry entries id
    78           in apply (#next entry) (f (id, entry) x) end;
    79   in if Symtab.defined entries id0 then apply (SOME id0) else I end;
    80 
    81 fun first_entry P (Document {start, entries, ...}) =
    82   let
    83     fun first _ NONE = NONE
    84       | first prev (SOME id) =
    85           let val entry = the_entry entries id
    86           in if P (id, entry) then SOME (prev, id, entry) else first (SOME id) (#next entry) end;
    87   in first NONE (SOME start) end;
    88 
    89 
    90 (* modify entries *)
    91 
    92 fun insert_after (id: command_id) (id2: command_id) = map_entries (fn entries =>
    93   let val {next, state} = the_entry entries id in
    94     entries
    95     |> put_entry (id, make_entry (SOME id2) state)
    96     |> put_entry (id2, make_entry next NONE)
    97   end);
    98 
    99 fun delete_after (id: command_id) = map_entries (fn entries =>
   100   let val {next, state} = the_entry entries id in
   101     (case next of
   102       NONE => error ("No next entry to delete: " ^ quote id)
   103     | SOME id2 =>
   104         entries |>
   105           (case #next (the_entry entries id2) of
   106             NONE => put_entry (id, make_entry NONE state)
   107           | SOME id3 => put_entry (id, make_entry (SOME id3) state) #> reset_entry_state id3))
   108   end);
   109 
   110 
   111 
   112 (** global configuration **)
   113 
   114 local
   115   val global_states = Unsynchronized.ref (Symtab.empty: Toplevel.state option future Symtab.table);
   116   val global_commands = Unsynchronized.ref (Symtab.empty: Toplevel.transition Symtab.table);
   117   val global_documents = Unsynchronized.ref (Symtab.empty: document Symtab.table);
   118 in
   119 
   120 fun change_states f = NAMED_CRITICAL "Isar" (fn () => Unsynchronized.change global_states f);
   121 fun get_states () = NAMED_CRITICAL "Isar" (fn () => ! global_states);
   122 
   123 fun change_commands f = NAMED_CRITICAL "Isar" (fn () => Unsynchronized.change global_commands f);
   124 fun get_commands () = NAMED_CRITICAL "Isar" (fn () => ! global_commands);
   125 
   126 fun change_documents f = NAMED_CRITICAL "Isar" (fn () => Unsynchronized.change global_documents f);
   127 fun get_documents () = NAMED_CRITICAL "Isar" (fn () => ! global_documents);
   128 
   129 fun init () = NAMED_CRITICAL "Isar" (fn () =>
   130  (global_states := Symtab.empty;
   131   global_commands := Symtab.empty;
   132   global_documents := Symtab.empty));
   133 
   134 end;
   135 
   136 
   137 (* state *)
   138 
   139 val empty_state = Future.value (SOME Toplevel.toplevel);
   140 
   141 fun define_state (id: state_id) =
   142   change_states (Symtab.update_new (id, empty_state))
   143     handle Symtab.DUP dup => err_dup "state" dup;
   144 
   145 fun put_state (id: state_id) state = change_states (Symtab.update (id, state));
   146 
   147 fun the_state (id: state_id) =
   148   (case Symtab.lookup (get_states ()) id of
   149     NONE => err_undef "state" id
   150   | SOME state => state);
   151 
   152 
   153 (* command *)
   154 
   155 fun define_command id tr =
   156   change_commands (Symtab.update_new (id, Toplevel.put_id id tr))
   157     handle Symtab.DUP dup => err_dup "command" dup;
   158 
   159 fun the_command (id: command_id) =
   160   (case Symtab.lookup (get_commands ()) id of
   161     NONE => err_undef "command" id
   162   | SOME tr => tr);
   163 
   164 
   165 (* document *)
   166 
   167 fun define_document (id: document_id) document =
   168   change_documents (Symtab.update_new (id, document))
   169     handle Symtab.DUP dup => err_dup "document" dup;
   170 
   171 fun the_document (id: document_id) =
   172   (case Symtab.lookup (get_documents ()) id of
   173     NONE => err_undef "document" id
   174   | SOME document => document);
   175 
   176 
   177 
   178 (** main operations **)
   179 
   180 (* begin/end document *)
   181 
   182 fun begin_document (id: document_id) path =
   183   let
   184     val (dir, name) = ThyLoad.split_thy_path path;
   185     val _ = define_command id Toplevel.empty;
   186     val _ = define_state id;
   187     val entries = Symtab.make [(id, make_entry NONE (SOME id))];
   188     val _ = define_document id (make_document dir name id entries);
   189   in () end;
   190 
   191 fun end_document (id: document_id) =
   192   let
   193     val document as Document {name, ...} = the_document id;
   194     val end_state =
   195       the_state (the (#state (#3 (the
   196         (first_entry (fn (_, {next, ...}) => is_none next) document)))));
   197     val _ =
   198       Future.fork_deps [end_state] (fn () =>
   199         (case Future.join end_state of
   200           SOME st =>
   201            (Toplevel.run_command name (Toplevel.put_id id (Toplevel.commit_exit Position.none)) st;
   202             ThyInfo.touch_child_thys name;
   203             ThyInfo.register_thy name)
   204         | NONE => error ("Failed to finish theory " ^ quote name)));
   205   in () end;
   206 
   207 
   208 (* document editing *)
   209 
   210 local
   211 
   212 fun is_changed entries' (id, {next = _, state}) =
   213   (case try (the_entry entries') id of
   214     NONE => true
   215   | SOME {next = _, state = state'} => state' <> state);
   216 
   217 fun new_state name (id, _) (state_id, updates) =
   218   let
   219     val state_id' = make_id ();
   220     val _ = define_state state_id';
   221     val tr = Toplevel.put_id state_id' (the_command id);
   222     fun make_state' () =
   223       let
   224         val state = the_state state_id;
   225         val state' =
   226           Future.fork_deps [state] (fn () =>
   227             (case Future.join state of
   228               NONE => NONE
   229             | SOME st => Toplevel.run_command name tr st));
   230       in put_state state_id' state' end;
   231   in (state_id', ((id, state_id'), make_state') :: updates) end;
   232 
   233 fun report_updates _ [] = ()
   234   | report_updates (document_id: document_id) updates =
   235       implode (map (fn (id, state_id) => Markup.markup (Markup.edit id state_id) "") updates)
   236       |> Markup.markup (Markup.edits document_id)
   237       |> Output.status;
   238 
   239 in
   240 
   241 fun edit_document (old_id: document_id) (new_id: document_id) edits =
   242   let
   243     val old_document as Document {name, entries = old_entries, ...} = the_document old_id;
   244     val new_document as Document {entries = new_entries, ...} = old_document
   245       |> fold (fn (id, SOME id2) => insert_after id id2 | (id, NONE) => delete_after id) edits;
   246 
   247     fun cancel_old id = fold_entries id
   248       (fn (_, {state = SOME state_id, ...}) => K (Future.cancel (the_state state_id)) | _ => K ())
   249       old_document ();
   250 
   251     val (updates, new_document') =
   252       (case first_entry (is_changed old_entries) new_document of
   253         NONE =>
   254           (case first_entry (is_changed new_entries) old_document of
   255             NONE => ([], new_document)
   256           | SOME (_, id, _) => (cancel_old id; ([], new_document)))
   257       | SOME (prev, id, _) =>
   258           let
   259             val _ = cancel_old id;
   260             val prev_state_id = the (#state (the_entry new_entries (the prev)));
   261             val (_, updates) = fold_entries id (new_state name) new_document (prev_state_id, []);
   262             val new_document' = new_document |> map_entries (fold (set_entry_state o #1) updates);
   263           in (rev updates, new_document') end);
   264 
   265     val _ = define_document new_id new_document';
   266     val _ = report_updates new_id (map #1 updates);
   267     val _ = List.app (fn (_, run) => run ()) updates;
   268   in () end;
   269 
   270 end;
   271 
   272 
   273 
   274 (** concrete syntax **)
   275 
   276 local structure P = OuterParse structure V = ValueParse in
   277 
   278 val _ =
   279   OuterSyntax.internal_command "Isar.define_command"
   280     (P.string -- P.string >> (fn (id, text) =>
   281       Toplevel.position (Position.id_only id) o
   282       Toplevel.imperative (fn () =>
   283         define_command id (OuterSyntax.prepare_command (Position.id id) text))));
   284 
   285 val _ =
   286   OuterSyntax.internal_command "Isar.begin_document"
   287     (P.string -- P.string >> (fn (id, path) =>
   288       Toplevel.imperative (fn () => begin_document id (Path.explode path))));
   289 
   290 val _ =
   291   OuterSyntax.internal_command "Isar.end_document"
   292     (P.string >> (fn id => Toplevel.imperative (fn () => end_document id)));
   293 
   294 val _ =
   295   OuterSyntax.internal_command "Isar.edit_document"
   296     (P.string -- P.string -- V.list (P.string -- (P.string >> SOME) || P.string >> rpair NONE)
   297       >> (fn ((id, new_id), edits) => Toplevel.imperative (fn () => edit_document id new_id edits)));
   298 
   299 end;
   300 
   301 end;
   302