src/Pure/Isar/isar_document.ML
author wenzelm
Tue, 13 Jan 2009 13:47:35 +0100
changeset 29459 8acad4f0a727
child 29467 d98fe0c504a8
permissions -rw-r--r--
added Isar/isar_document.ML: Interactive Isar documents.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
29459
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/Isar/isar_document.ML
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
     3
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
     4
Interactive Isar documents.
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
     5
*)
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
     6
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
     7
signature ISAR_DOCUMENT =
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
     8
sig
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
     9
  type state_id = string
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
    10
  type command_id = string
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
    11
  type document_id = string
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
    12
  val define_command: command_id -> Toplevel.transition -> unit
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
    13
  val begin_document: document_id -> Path.T -> unit
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
    14
  val edit_document: document_id -> document_id -> (command_id * command_id option) list -> unit
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
    15
  val end_document: document_id -> unit
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
    16
end;
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
    17
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
    18
structure IsarDocument: ISAR_DOCUMENT =
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
    19
struct
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
    20
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
    21
(* unique identifiers *)
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
    22
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
    23
type document_id = string;
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
    24
type command_id = string;
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
    25
type state_id = string;
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
    26
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
    27
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
    28
(** execution states **)
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
    29
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
    30
(* command status *)
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
    31
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
    32
datatype status =
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
    33
  Unprocessed |
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
    34
  Running of Toplevel.state option future |
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
    35
  Failed |
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
    36
  Finished of Toplevel.state;
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
    37
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
    38
fun status_markup Unprocessed = Markup.unprocessed
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
    39
  | status_markup (Running future) = Markup.running (Task_Queue.str_of_task (Future.task_of future))
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
    40
  | status_markup Failed = Markup.failed
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
    41
  | status_markup (Finished _) = Markup.finished;
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
    42
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
    43
fun status_update tr state status =
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
    44
  (case status of
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
    45
    Unprocessed => SOME (Running (Future.fork_pri 1 (fn () =>
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
    46
      (case Toplevel.transition true tr state of
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
    47
        NONE => (Toplevel.error_msg tr (SYS_ERROR "Cannot terminate here!", ""); NONE)
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
    48
      | SOME (_, SOME err) => (Toplevel.error_msg tr err; NONE)
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
    49
      | SOME (state', NONE) => SOME state'))))
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
    50
  | Running future =>
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
    51
      (case Future.peek future of
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
    52
        NONE => NONE
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
    53
      | SOME (Exn.Result NONE) => SOME Failed
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
    54
      | SOME (Exn.Result (SOME state')) => SOME (Finished state')
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
    55
      | SOME (Exn.Exn exn) => (Toplevel.error_msg tr (exn, ""); SOME Failed))
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
    56
  | _ => NONE);
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
    57
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
    58
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
    59
(* state *)
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
    60
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
    61
datatype state = State of
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
    62
 {prev: state_id option,
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
    63
  command: command_id,
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
    64
  status: status};
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
    65
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
    66
fun make_state prev command status = State {prev = prev, command = command, status = status};
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
    67
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
    68
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
    69
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
    70
(** documents **)
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
    71
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
    72
(* command entries *)
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
    73
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
    74
datatype entry = Entry of
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
    75
 {prev: command_id option,
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
    76
  next: command_id option,
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
    77
  state: state_id};
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
    78
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
    79
fun make_entry prev next state = Entry {prev = prev, next = next, state = state};
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
    80
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
    81
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
    82
(* document *)
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
    83
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
    84
datatype document = Document of
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
    85
 {dir: Path.T,                    (*master directory*)
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
    86
  name: string,                   (*theory name*)
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
    87
  commands: entry Symtab.table};  (*unique command entries indexed by command_id*)
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
    88
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
    89
fun make_document dir name commands = Document {dir = dir, name = name, commands = commands};
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
    90
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
    91
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
    92
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
    93
(** global configuration **)
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
    94
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
    95
fun err_dup kind id = sys_error ("Duplicate " ^ kind ^ ": " ^ quote id);
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
    96
fun err_undef kind id = sys_error ("Unknown " ^ kind ^ ": " ^ quote id);
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
    97
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
    98
local
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
    99
  val global_states = ref (Symtab.empty: state Symtab.table);
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   100
  val global_commands = ref (Symtab.empty: Toplevel.transition Symtab.table);
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   101
  val global_documents = ref (Symtab.empty: document Symtab.table);
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   102
in
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   103
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   104
fun change_states f = NAMED_CRITICAL "Isar" (fn () => change global_states f);
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   105
fun get_states () = NAMED_CRITICAL "Isar" (fn () => ! global_states);
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   106
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   107
fun change_commands f = NAMED_CRITICAL "Isar" (fn () => change global_commands f);
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   108
fun get_commands () = NAMED_CRITICAL "Isar" (fn () => ! global_commands);
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   109
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   110
fun change_documents f = NAMED_CRITICAL "Isar" (fn () => change global_documents f);
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   111
fun get_documents () = NAMED_CRITICAL "Isar" (fn () => ! global_documents);
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   112
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   113
fun init () = NAMED_CRITICAL "Isar" (fn () =>
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   114
 (global_states := Symtab.empty;
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   115
  global_commands := Symtab.empty;
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   116
  global_documents := Symtab.empty));
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   117
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   118
end;
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   119
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   120
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   121
fun define_state (id: state_id) state =
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   122
  change_states (Symtab.update_new (id, state))
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   123
    handle Symtab.DUP dup => err_dup "state" dup;
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   124
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   125
fun the_state (id: state_id) =
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   126
  (case Symtab.lookup (get_states ()) id of
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   127
    NONE => err_undef "state" id
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   128
  | SOME (State {status as Finished state, ...}) => state
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   129
  | _ => sys_error ("Unfinished state " ^ id));
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   130
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   131
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   132
fun define_command id tr =
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   133
  change_commands (Symtab.update_new (id, Toplevel.put_id id tr))
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   134
    handle Symtab.DUP dup => err_dup ("command " ^ Toplevel.name_of tr) dup;
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   135
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   136
fun the_command (id: command_id) =
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   137
  (case Symtab.lookup (get_commands ()) id of
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   138
    NONE => err_undef "command" id
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   139
  | SOME cmd => cmd);
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   140
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   141
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   142
fun define_document (id: document_id) document =
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   143
  change_documents (Symtab.update_new (id, document))
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   144
    handle Symtab.DUP dup => err_dup "document" dup;
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   145
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   146
fun the_document (id: document_id) =
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   147
  (case Symtab.lookup (get_documents ()) id of
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   148
    NONE => err_undef "document" id
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   149
  | SOME doc => doc);
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   150
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   151
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   152
fun begin_document (id: document_id) path =
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   153
  let
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   154
    val (dir, name) = ThyLoad.split_thy_path path;
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   155
    val _ = define_command id Toplevel.empty;
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   156
    val _ = define_state id (make_state NONE id (Finished Toplevel.toplevel));
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   157
    val commands = Symtab.make [(id, make_entry NONE NONE id)];
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   158
    val _ = define_document id (make_document dir name commands);
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   159
  in () end;
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   160
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   161
fun edit_document (id: document_id) (new_id: document_id) edits =
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   162
  let
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   163
    val Document {dir, name, commands} = the_document id;
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   164
    val commands' = sys_error "FIXME";
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   165
    val _ = define_document new_id (make_document dir name commands');
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   166
  in () end;
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   167
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   168
fun end_document (id: document_id) = sys_error "FIXME";
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   169
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   170
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   171
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   172
(** concrete syntax **)
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   173
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   174
local structure P = OuterParse structure V = ValueParse in
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   175
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   176
val _ =
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   177
  OuterSyntax.internal_command "Isar.define_command"
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   178
    (P.string -- P.string >> (fn (id, text) =>
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   179
      Toplevel.imperative (fn () =>
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   180
        define_command id (OuterSyntax.prepare_command (Position.id id) text))));
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   181
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   182
val _ =
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   183
  OuterSyntax.internal_command "Isar.begin_document"
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   184
    (P.string -- P.string >> (fn (id, path) =>
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   185
      Toplevel.imperative (fn () => begin_document id (Path.explode path))));
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   186
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   187
val _ =
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   188
  OuterSyntax.internal_command "Isar.edit_document"
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   189
    (P.string -- P.string -- V.list (P.string -- (P.string >> SOME) || P.string >> rpair NONE)
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   190
      >> (fn ((id, new_id), edits) => Toplevel.imperative (fn () => end_document id new_id edits)));
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   191
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   192
val _ =
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   193
  OuterSyntax.internal_command "Isar.end_document"
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   194
    (P.string >> (fn id => Toplevel.imperative (fn () => end_document id)));
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   195
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   196
end;
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   197
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   198
end;