src/Pure/Isar/isar_document.ML

misc internal rearrangements;
fold_entries: really start from start, or optional position;
added find_first_entries, find_first_entries;
insert_entry: always invalidate next state;
added refresh_states (partial version);

(*  Title:      Pure/Isar/isar_document.ML
    Author:     Makarius

Interactive Isar documents.
*)

signature ISAR_DOCUMENT =
sig
  type state_id = string
  type command_id = string
  type document_id = string
  val define_command: command_id -> Toplevel.transition -> unit
  val begin_document: document_id -> Path.T -> unit
  val end_document: document_id -> unit
  val edit_document: document_id -> document_id -> (command_id * command_id option) list -> unit
end;

structure IsarDocument: ISAR_DOCUMENT =
struct


(* unique identifiers *)

type document_id = string;
type command_id = string;
type state_id = string;

fun new_id () = "isabelle:" ^ serial_string ();

fun err_dup kind id = error ("Duplicate " ^ kind ^ ": " ^ quote id);
fun err_undef kind id = error ("Unknown " ^ kind ^ ": " ^ quote id);


(** execution states **)

(* command status *)

datatype status =
  Unprocessed |
  Running of Toplevel.state option future |
  Failed |
  Finished of Toplevel.state;

fun markup_status Unprocessed = Markup.unprocessed
  | markup_status (Running future) = Markup.running (Task_Queue.str_of_task (Future.task_of future))
  | markup_status Failed = Markup.failed
  | markup_status (Finished _) = Markup.finished;

fun update_status retry tr state status =
  (case status of
    Unprocessed => SOME (Running (Future.fork_pri 1 (fn () =>
      (case Toplevel.transition true tr state of
        NONE => (Toplevel.error_msg tr (ERROR "Cannot terminate here!", ""); NONE)
      | SOME (_, SOME err) => (Toplevel.error_msg tr err; NONE)
      | SOME (state', NONE) => SOME state'))))
  | Running future =>
      (case Future.peek future of
        NONE => NONE
      | SOME (Exn.Result NONE) => SOME Failed
      | SOME (Exn.Result (SOME state')) => SOME (Finished state')
      | SOME (Exn.Exn exn) => (Toplevel.error_msg tr (exn, ""); SOME Failed))
  | Failed => if retry then SOME Unprocessed else NONE
  | _ => NONE);


(* state *)

datatype state = State of
 {prev: state_id option,
  command: command_id,
  status: status};

fun make_state prev command status = State {prev = prev, command = command, status = status};



(** documents **)

(* command entries *)

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

fun make_entry prev next state = Entry {prev = prev, 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 map_entry (id: command_id) f entries =
  let
    val {prev, next, state} = the_entry entries id;
    val (prev', next', state') = f (prev, next, state);
  in put_entry (id, make_entry prev' next' state') entries end;


(* document *)

datatype document = Document of
 {dir: Path.T,                    (*master directory*)
  name: string,                   (*theory name*)
  start: command_id,              (*empty start command*)
  entries: entry Symtab.table};   (*unique command entries indexed by command_id*)

fun make_document dir name start entries =
  Document {dir = dir, name = name, start = start, entries = entries};

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


(* iterating entries *)

fun fold_entries opt_id f (Document {start, entries, ...}) =
  let
    fun apply NONE x = x
      | apply (SOME id) x = apply (#next (the_entry entries id)) (f id x);
  in if is_some opt_id then apply opt_id else apply (SOME start) end;

fun get_first_entries opt_id f (Document {start, entries, ...}) =
  let
    fun get NONE = NONE
      | get (SOME id) = (case f id of NONE => get (#next (the_entry entries id)) | some => some);
  in if is_some opt_id then get opt_id else get (SOME start) end;

fun find_first_entries opt_id P =
  get_first_entries opt_id (fn x => if P x then SOME x else NONE);


(* modify entries *)

fun insert_entry (id: command_id, id2: command_id) = map_entries (fn entries =>
  let val {prev, next, state} = the_entry entries id in
    entries |>
      (case next of
        NONE => put_entry (id2, make_entry (SOME id) NONE NONE)
      | SOME id3 =>
          put_entry (id, make_entry prev (SOME id2) state) #>
          put_entry (id2, make_entry (SOME id) (SOME id3) NONE) #>
          put_entry (id3, make_entry (SOME id2) (#next (the_entry entries id3)) NONE))
  end);

fun delete_after (id: command_id) = map_entries (fn entries =>
  let val {prev, next, state} = the_entry entries id in
    entries |>
      (case next of
        NONE => error ("Missing next entry: " ^ quote id)
      | SOME id2 =>
          (case #next (the_entry entries id2) of
            NONE => put_entry (id, make_entry prev NONE state)
          | SOME id3 =>
              put_entry (id, make_entry prev (SOME id3) state) #>
              put_entry (id3, make_entry (SOME id) (#next (the_entry entries id3)) NONE)))
  end);



(** global configuration **)

local
  val global_states = ref (Symtab.empty: state Symtab.table);
  val global_commands = ref (Symtab.empty: Toplevel.transition Symtab.table);
  val global_documents = ref (Symtab.empty: document Symtab.table);
in

fun change_states f = NAMED_CRITICAL "Isar" (fn () => change global_states f);
fun get_states () = NAMED_CRITICAL "Isar" (fn () => ! global_states);

fun change_commands f = NAMED_CRITICAL "Isar" (fn () => change global_commands f);
fun get_commands () = NAMED_CRITICAL "Isar" (fn () => ! global_commands);

fun change_documents f = NAMED_CRITICAL "Isar" (fn () => change global_documents f);
fun get_documents () = NAMED_CRITICAL "Isar" (fn () => ! global_documents);

fun init () = NAMED_CRITICAL "Isar" (fn () =>
 (global_states := Symtab.empty;
  global_commands := Symtab.empty;
  global_documents := Symtab.empty));

end;


fun define_state (id: state_id) state =
  change_states (Symtab.update_new (id, state))
    handle Symtab.DUP dup => err_dup "state" dup;

fun the_state (id: state_id) =
  (case Symtab.lookup (get_states ()) id of
    NONE => err_undef "state" id
  | SOME (State state) => state);


fun define_command id tr =
  change_commands (Symtab.update_new (id, Toplevel.put_id id tr))
    handle Symtab.DUP dup => err_dup ("command " ^ Toplevel.name_of tr) dup;

fun the_command (id: command_id) =
  (case Symtab.lookup (get_commands ()) id of
    NONE => err_undef "command" id
  | SOME tr => tr);


fun define_document (id: document_id) document =
  change_documents (Symtab.update_new (id, document))
    handle Symtab.DUP dup => err_dup "document" dup;

fun the_document (id: document_id) =
  (case Symtab.lookup (get_documents ()) id of
    NONE => err_undef "document" id
  | SOME (Document doc) => doc);


(* begin/end document *)

fun begin_document (id: document_id) path =
  let
    val (dir, name) = ThyLoad.split_thy_path path;
    val _ = define_command id Toplevel.empty;
    val _ = define_state id (make_state NONE id (Finished Toplevel.toplevel));
    val entries = Symtab.make [(id, make_entry NONE NONE (SOME id))];
    val _ = define_document id (make_document dir name id entries);
  in () end;

fun end_document (id: document_id) = error "FIXME";


(* document editing *)

fun refresh_states old_document new_document =
  let
    val Document {entries = old_entries, ...} = old_document;
    val Document {entries = new_entries, ...} = new_document;

    fun is_changed id =
      (case try (the_entry new_entries) id of
        SOME {state = SOME _, ...} => false
      | _ => true);

    fun cancel_state id () =
      (case the_entry old_entries id of
        {state = SOME state_id, ...} =>
          (case the_state state_id of
            {status = Running future, ...} => Future.cancel future
          | _ => ())
      | _ => ());

    fun new_state id (prev_state_id, new_states) =
      let
        val state_id = new_id ();
        val state = make_state prev_state_id id Unprocessed;
        val _ = define_state state_id state;
      in (SOME state_id, (state_id, state) :: new_states) end;
  in
    (case find_first_entries NONE is_changed old_document of
      NONE => new_document
    | SOME id =>
        let
          val _ = fold_entries (SOME id) cancel_state old_document ();
          val (_, new_states) = fold_entries (SOME id) new_state new_document (NONE, []);
          (* FIXME update states *)
        in new_document end)
  end;

fun edit_document (id: document_id) (id': document_id) edits =
  let
    val document = Document (the_document id);
    val document' =
      document
      |> fold (fn (id, SOME id2) => insert_entry (id, id2) | (id, NONE) => delete_after id) edits
      |> refresh_states document;
    val _ = define_document id' document';
  in () end;



(** concrete syntax **)

local structure P = OuterParse structure V = ValueParse in

val _ =
  OuterSyntax.internal_command "Isar.define_command"
    (P.string -- P.string >> (fn (id, text) =>
      Toplevel.imperative (fn () =>
        define_command id (OuterSyntax.prepare_command (Position.id id) text))));

val _ =
  OuterSyntax.internal_command "Isar.begin_document"
    (P.string -- P.string >> (fn (id, path) =>
      Toplevel.imperative (fn () => begin_document id (Path.explode path))));

val _ =
  OuterSyntax.internal_command "Isar.end_document"
    (P.string >> (fn id => Toplevel.imperative (fn () => end_document id)));

val _ =
  OuterSyntax.internal_command "Isar.edit_document"
    (P.string -- P.string -- V.list (P.string -- (P.string >> SOME) || P.string >> rpair NONE)
      >> (fn ((id, new_id), edits) => Toplevel.imperative (fn () => end_document id new_id edits)));

end;

end;