(*  Title:      Pure/Isar/isar_document.ML

     Author:     Makarius

 Interactive Isar documents.

 *)

 structure Isar_Document: sig end =

 struct

 (* unique identifiers *)

 type state_id = string;

 type command_id = string;

 type document_id = string;

 val no_id = "";

 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 **)

 (* command entries *)

 datatype entry = Entry of {next: command_id option, state: state_id option};

 fun make_entry next state = Entry {next = next, state = state};

 fun the_entry entries (id: command_id) =

   (case Symtab.lookup entries id of

     NONE => err_undef "document entry" id

   | SOME (Entry entry) => entry);

 fun put_entry (id: command_id, entry: entry) = Symtab.update (id, entry);

 fun put_entry_state (id: command_id) state entries =

   let val {next, ...} = the_entry entries id

   in put_entry (id, make_entry next state) entries 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);

 (* document *)

 datatype document = Document of

  {dir: Path.T,                   (*master directory*)

   name: string,                  (*theory name*)

   entries: entry Symtab.table};  (*unique command entries indexed by command_id, start with no_id*)

 fun make_document dir name entries =

   Document {dir = dir, name = name, entries = entries};

 fun map_entries f (Document {dir, name, entries}) =

   make_document dir name (f entries);

 (* iterate entries *)

 fun fold_entries id0 f (Document {entries, ...}) =

   let

     fun apply NONE x = x

       | apply (SOME id) x =

           let val entry = the_entry entries id

           in apply (#next entry) (f (id, entry) x) end;

   in if Symtab.defined entries id0 then apply (SOME id0) else I end;

 fun first_entry P (Document {entries, ...}) =

   let

     fun first _ NONE = NONE

       | first prev (SOME id) =

           let val entry = the_entry entries id

           in if P (id, entry) then SOME (prev, id, entry) else first (SOME id) (#next entry) end;

   in first NONE (SOME no_id) end;

 (* modify entries *)

 fun insert_after (id: command_id) (id2: command_id) = map_entries (fn entries =>

   let val {next, state} = the_entry entries id in

     entries

     |> put_entry (id, make_entry (SOME id2) state)

     |> put_entry (id2, make_entry next NONE)

   end);

 fun delete_after (id: command_id) = map_entries (fn entries =>

   let val {next, state} = the_entry entries id in

     (case next of

       NONE => error ("No next entry to delete: " ^ quote id)

     | SOME id2 =>

         entries |>

           (case #next (the_entry entries 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);

 (** global configuration **)

 (* states *)

 local

 val global_states = Unsynchronized.ref (Symtab.make [(no_id, Lazy.value (SOME Toplevel.toplevel))]);

 in

 fun define_state (id: 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: 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 [(no_id, Toplevel.empty)]);

 in

 fun define_command (id: command_id) tr =

   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);

 fun the_command (id: command_id) =

   (case Symtab.lookup (! global_commands) id of

     NONE => err_undef "command" id

   | SOME tr => tr);

 end;

 (* documents *)

 local

 val global_documents = Unsynchronized.ref (Symtab.empty: document Symtab.table);

 in

 fun define_document (id: document_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_id) =

   (case Symtab.lookup (! global_documents) id of

     NONE => err_undef "document" id

   | SOME document => document);

 end;

 (** main operations **)

 (* begin/end document *)

 val no_entries = Symtab.make [(no_id, make_entry NONE (SOME no_id))];

 fun begin_document (id: document_id) path =

   let

     val (dir, name) = Thy_Load.split_thy_path path;

     val _ = define_document id (make_document dir name no_entries);

   in () end;

 fun end_document (id: document_id) =

   NAMED_CRITICAL "Isar" (fn () =>

     let

       val document as Document {name, ...} = the_document id;

       val end_state =

         the_state (the (#state (#3 (the

           (first_entry (fn (_, {next, ...}) => is_none next) document)))));

       val _ =  (* FIXME regular execution (??) *)

         Future.fork (fn () =>

           (case Lazy.force end_state of

             SOME st =>

              (Toplevel.run_command name (Toplevel.put_id id (Toplevel.commit_exit Position.none)) st;

               Thy_Info.touch_child_thys name;

               Thy_Info.register_thy name)

           | NONE => error ("Failed to finish theory " ^ quote name)));

     in () end);

 (* document editing *)

 local

 fun is_changed entries' (id, {next = _, state}) =

   (case try (the_entry entries') id of

     NONE => true

   | SOME {next = _, state = state'} => state' <> state);

 fun new_state name (id: 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 report_updates updates =

   implode (map (fn (id, state_id) => Markup.markup (Markup.edit id state_id) "") updates)

   |> Markup.markup Markup.assign

   |> Output.status;

 fun force_state NONE = ()

   | force_state (SOME state_id) = ignore (Lazy.force (the_state state_id));

 val execution = Unsynchronized.ref (Future.value ());

 fun execute document =

   NAMED_CRITICAL "Isar" (fn () =>

     let

       val old_execution = ! execution;

       val _ = Future.cancel old_execution;

       val new_execution = Future.fork (fn () =>

        (Future.join_result old_execution;

         fold_entries no_id (fn (_, {state, ...}) => fn () => force_state state) document ()));

     in execution := new_execution end);

 in

 fun edit_document (old_id: document_id) (new_id: document_id) edits =

   NAMED_CRITICAL "Isar" (fn () =>

     let

       val old_document as Document {name, entries = old_entries, ...} = the_document old_id;

       val new_document as Document {entries = new_entries, ...} = old_document

         |> fold (fn (id, SOME id2) => insert_after id id2 | (id, NONE) => delete_after id) edits;

       val (updates, new_document') =

         (case first_entry (is_changed old_entries) new_document of

           NONE => ([], new_document)

         | SOME (prev, id, _) =>

             let

               val prev_state_id = the (#state (the_entry new_entries (the prev)));

               val (_, updates) =

                 fold_entries id (new_state name o #1) new_document (prev_state_id, []);

               val new_document' = new_document |> map_entries (fold set_entry_state updates);

             in (rev updates, new_document') end);

       val _ = define_document new_id new_document';

       val _ = report_updates updates;

       val _ = execute new_document';

     in () end);

 end;

 (** concrete syntax **)

 val _ =

   Outer_Syntax.internal_command "Isar.define_command"

     (Parse.string -- Parse.string >> (fn (id, text) =>

       Toplevel.position (Position.id_only id) o

       Toplevel.imperative (fn () =>

         define_command id (Outer_Syntax.prepare_command (Position.id id) text))));

 val _ =

   Outer_Syntax.internal_command "Isar.begin_document"

     (Parse.string -- Parse.string >> (fn (id, path) =>

       Toplevel.imperative (fn () => begin_document id (Path.explode path))));

 val _ =

   Outer_Syntax.internal_command "Isar.end_document"

     (Parse.string >> (fn id => Toplevel.imperative (fn () => end_document id)));

 val _ =

   Outer_Syntax.internal_command "Isar.edit_document"

     (Parse.string -- Parse.string --

         Parse_Value.list (Parse.string -- (Parse.string >> SOME) || Parse.string >> rpair NONE)

       >> (fn ((id, new_id), edits) =>

         Toplevel.position (Position.id_only new_id) o

         Toplevel.imperative (fn () => edit_document id new_id edits)));

 end;