src/Pure/Isar/isar_document.ML
author wenzelm
Tue, 13 Jan 2009 17:34:12 +0100
changeset 29467 d98fe0c504a8
parent 29459 8acad4f0a727
child 29468 c9bb4e06d173
permissions -rw-r--r--
replaced sys_error by plain error; some basic operations on command entries within a document;
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
29467
d98fe0c504a8 replaced sys_error by plain error;
wenzelm
parents: 29459
diff changeset
    27
val no_id = "";
d98fe0c504a8 replaced sys_error by plain error;
wenzelm
parents: 29459
diff changeset
    28
d98fe0c504a8 replaced sys_error by plain error;
wenzelm
parents: 29459
diff changeset
    29
fun err_dup kind id = error ("Duplicate " ^ kind ^ ": " ^ quote id);
d98fe0c504a8 replaced sys_error by plain error;
wenzelm
parents: 29459
diff changeset
    30
fun err_undef kind id = error ("Unknown " ^ kind ^ ": " ^ quote id);
d98fe0c504a8 replaced sys_error by plain error;
wenzelm
parents: 29459
diff changeset
    31
29459
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
    32
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
    33
(** execution states **)
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
    34
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
    35
(* command status *)
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
    36
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
    37
datatype status =
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
    38
  Unprocessed |
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
    39
  Running of Toplevel.state option future |
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
    40
  Failed |
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
    41
  Finished of Toplevel.state;
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_markup Unprocessed = Markup.unprocessed
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
    44
  | 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
    45
  | status_markup Failed = Markup.failed
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
    46
  | status_markup (Finished _) = Markup.finished;
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
    47
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
    48
fun status_update tr state status =
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
    49
  (case status of
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
    50
    Unprocessed => SOME (Running (Future.fork_pri 1 (fn () =>
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
    51
      (case Toplevel.transition true tr state of
29467
d98fe0c504a8 replaced sys_error by plain error;
wenzelm
parents: 29459
diff changeset
    52
        NONE => (Toplevel.error_msg tr (ERROR "Cannot terminate here!", ""); NONE)
29459
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
    53
      | SOME (_, SOME err) => (Toplevel.error_msg tr err; NONE)
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
    54
      | SOME (state', NONE) => SOME state'))))
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
    55
  | Running future =>
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
    56
      (case Future.peek future of
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
    57
        NONE => NONE
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
    58
      | SOME (Exn.Result NONE) => SOME Failed
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
    59
      | SOME (Exn.Result (SOME state')) => SOME (Finished state')
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
    60
      | SOME (Exn.Exn exn) => (Toplevel.error_msg tr (exn, ""); SOME Failed))
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
    61
  | _ => NONE);
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
    62
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
    63
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
    64
(* state *)
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
datatype state = State of
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
    67
 {prev: state_id option,
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
    68
  command: command_id,
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
    69
  status: status};
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
    70
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
    71
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
    72
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
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
    75
(** documents **)
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
    76
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
    77
(* command entries *)
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
datatype entry = Entry of
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
    80
 {prev: command_id option,
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
    81
  next: command_id option,
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
    82
  state: state_id};
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
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
    85
29467
d98fe0c504a8 replaced sys_error by plain error;
wenzelm
parents: 29459
diff changeset
    86
fun the_entry entries (id: command_id) =
d98fe0c504a8 replaced sys_error by plain error;
wenzelm
parents: 29459
diff changeset
    87
  (case Symtab.lookup entries id of
d98fe0c504a8 replaced sys_error by plain error;
wenzelm
parents: 29459
diff changeset
    88
    NONE => err_undef "document entry" id
d98fe0c504a8 replaced sys_error by plain error;
wenzelm
parents: 29459
diff changeset
    89
  | SOME (Entry entry) => entry);
d98fe0c504a8 replaced sys_error by plain error;
wenzelm
parents: 29459
diff changeset
    90
d98fe0c504a8 replaced sys_error by plain error;
wenzelm
parents: 29459
diff changeset
    91
fun put_entry (id: command_id, entry: entry) = Symtab.update (id, entry);
d98fe0c504a8 replaced sys_error by plain error;
wenzelm
parents: 29459
diff changeset
    92
d98fe0c504a8 replaced sys_error by plain error;
wenzelm
parents: 29459
diff changeset
    93
fun map_entry (id: command_id) f entries =
d98fe0c504a8 replaced sys_error by plain error;
wenzelm
parents: 29459
diff changeset
    94
  let
d98fe0c504a8 replaced sys_error by plain error;
wenzelm
parents: 29459
diff changeset
    95
    val {prev, next, state} = the_entry entries id;
d98fe0c504a8 replaced sys_error by plain error;
wenzelm
parents: 29459
diff changeset
    96
    val (prev', next', state') = f (prev, next, state);
d98fe0c504a8 replaced sys_error by plain error;
wenzelm
parents: 29459
diff changeset
    97
  in put_entry (id, make_entry prev' next' state') entries end;
d98fe0c504a8 replaced sys_error by plain error;
wenzelm
parents: 29459
diff changeset
    98
29459
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
    99
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   100
(* document *)
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   101
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   102
datatype document = Document of
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   103
 {dir: Path.T,                    (*master directory*)
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   104
  name: string,                   (*theory name*)
29467
d98fe0c504a8 replaced sys_error by plain error;
wenzelm
parents: 29459
diff changeset
   105
  start: command_id,              (*empty start command*)
d98fe0c504a8 replaced sys_error by plain error;
wenzelm
parents: 29459
diff changeset
   106
  entries: entry Symtab.table};   (*unique command entries indexed by command_id*)
d98fe0c504a8 replaced sys_error by plain error;
wenzelm
parents: 29459
diff changeset
   107
d98fe0c504a8 replaced sys_error by plain error;
wenzelm
parents: 29459
diff changeset
   108
fun make_document dir name start entries =
d98fe0c504a8 replaced sys_error by plain error;
wenzelm
parents: 29459
diff changeset
   109
  Document {dir = dir, name = name, start = start, entries = entries};
d98fe0c504a8 replaced sys_error by plain error;
wenzelm
parents: 29459
diff changeset
   110
d98fe0c504a8 replaced sys_error by plain error;
wenzelm
parents: 29459
diff changeset
   111
fun map_entries f (Document {dir, name, start, entries}) =
d98fe0c504a8 replaced sys_error by plain error;
wenzelm
parents: 29459
diff changeset
   112
  make_document dir name start (f entries);
d98fe0c504a8 replaced sys_error by plain error;
wenzelm
parents: 29459
diff changeset
   113
d98fe0c504a8 replaced sys_error by plain error;
wenzelm
parents: 29459
diff changeset
   114
d98fe0c504a8 replaced sys_error by plain error;
wenzelm
parents: 29459
diff changeset
   115
fun fold_entries f (Document {start, entries, ...}) =
d98fe0c504a8 replaced sys_error by plain error;
wenzelm
parents: 29459
diff changeset
   116
  let
d98fe0c504a8 replaced sys_error by plain error;
wenzelm
parents: 29459
diff changeset
   117
    fun descend NONE x = x
d98fe0c504a8 replaced sys_error by plain error;
wenzelm
parents: 29459
diff changeset
   118
      | descend (SOME id) x = descend_next id (f id x)
d98fe0c504a8 replaced sys_error by plain error;
wenzelm
parents: 29459
diff changeset
   119
    and descend_next id = descend (#next (the_entry entries id));
d98fe0c504a8 replaced sys_error by plain error;
wenzelm
parents: 29459
diff changeset
   120
  in descend_next start end;
d98fe0c504a8 replaced sys_error by plain error;
wenzelm
parents: 29459
diff changeset
   121
29459
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   122
29467
d98fe0c504a8 replaced sys_error by plain error;
wenzelm
parents: 29459
diff changeset
   123
fun insert_entry (id: command_id, id2: command_id) = map_entries (fn entries =>
d98fe0c504a8 replaced sys_error by plain error;
wenzelm
parents: 29459
diff changeset
   124
  let
d98fe0c504a8 replaced sys_error by plain error;
wenzelm
parents: 29459
diff changeset
   125
    val {prev, next, state} = the_entry entries id;
d98fe0c504a8 replaced sys_error by plain error;
wenzelm
parents: 29459
diff changeset
   126
    val state2 = no_id;
d98fe0c504a8 replaced sys_error by plain error;
wenzelm
parents: 29459
diff changeset
   127
  in
d98fe0c504a8 replaced sys_error by plain error;
wenzelm
parents: 29459
diff changeset
   128
    entries |>
d98fe0c504a8 replaced sys_error by plain error;
wenzelm
parents: 29459
diff changeset
   129
      (case next of
d98fe0c504a8 replaced sys_error by plain error;
wenzelm
parents: 29459
diff changeset
   130
        NONE => put_entry (id2, make_entry (SOME id) NONE state2)
d98fe0c504a8 replaced sys_error by plain error;
wenzelm
parents: 29459
diff changeset
   131
      | SOME id3 =>
d98fe0c504a8 replaced sys_error by plain error;
wenzelm
parents: 29459
diff changeset
   132
          let val {next = next3, state = state3, ...} = the_entry entries id3 in
d98fe0c504a8 replaced sys_error by plain error;
wenzelm
parents: 29459
diff changeset
   133
            put_entry (id, make_entry prev (SOME id2) state) #>
d98fe0c504a8 replaced sys_error by plain error;
wenzelm
parents: 29459
diff changeset
   134
            put_entry (id2, make_entry (SOME id) (SOME id3) state2) #>
d98fe0c504a8 replaced sys_error by plain error;
wenzelm
parents: 29459
diff changeset
   135
            put_entry (id3, make_entry (SOME id2) next3 state3)
d98fe0c504a8 replaced sys_error by plain error;
wenzelm
parents: 29459
diff changeset
   136
          end)
d98fe0c504a8 replaced sys_error by plain error;
wenzelm
parents: 29459
diff changeset
   137
  end);
d98fe0c504a8 replaced sys_error by plain error;
wenzelm
parents: 29459
diff changeset
   138
d98fe0c504a8 replaced sys_error by plain error;
wenzelm
parents: 29459
diff changeset
   139
fun delete_after_entry (id: command_id) = map_entries (fn entries =>
d98fe0c504a8 replaced sys_error by plain error;
wenzelm
parents: 29459
diff changeset
   140
  let val {prev, next, state} = the_entry entries id in
d98fe0c504a8 replaced sys_error by plain error;
wenzelm
parents: 29459
diff changeset
   141
    entries |>
d98fe0c504a8 replaced sys_error by plain error;
wenzelm
parents: 29459
diff changeset
   142
      (case next of
d98fe0c504a8 replaced sys_error by plain error;
wenzelm
parents: 29459
diff changeset
   143
        NONE => error ("Missing next entry: " ^ quote id)
d98fe0c504a8 replaced sys_error by plain error;
wenzelm
parents: 29459
diff changeset
   144
      | SOME id2 =>
d98fe0c504a8 replaced sys_error by plain error;
wenzelm
parents: 29459
diff changeset
   145
          (case #next (the_entry entries id2) of
d98fe0c504a8 replaced sys_error by plain error;
wenzelm
parents: 29459
diff changeset
   146
            NONE => put_entry (id, make_entry prev NONE state)
d98fe0c504a8 replaced sys_error by plain error;
wenzelm
parents: 29459
diff changeset
   147
          | SOME id3 =>
d98fe0c504a8 replaced sys_error by plain error;
wenzelm
parents: 29459
diff changeset
   148
              let val {next = next3, state = state3, ...} = the_entry entries id3 in
d98fe0c504a8 replaced sys_error by plain error;
wenzelm
parents: 29459
diff changeset
   149
                put_entry (id, make_entry prev (SOME id3) state) #>
d98fe0c504a8 replaced sys_error by plain error;
wenzelm
parents: 29459
diff changeset
   150
                put_entry (id3, make_entry (SOME id) next3 state3)
d98fe0c504a8 replaced sys_error by plain error;
wenzelm
parents: 29459
diff changeset
   151
              end))
d98fe0c504a8 replaced sys_error by plain error;
wenzelm
parents: 29459
diff changeset
   152
  end);
29459
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   153
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   154
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   155
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   156
(** global configuration **)
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   157
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   158
local
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   159
  val global_states = ref (Symtab.empty: state Symtab.table);
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   160
  val global_commands = ref (Symtab.empty: Toplevel.transition Symtab.table);
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   161
  val global_documents = ref (Symtab.empty: document Symtab.table);
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   162
in
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   163
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   164
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
   165
fun get_states () = NAMED_CRITICAL "Isar" (fn () => ! global_states);
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   166
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   167
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
   168
fun get_commands () = NAMED_CRITICAL "Isar" (fn () => ! global_commands);
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
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
   171
fun get_documents () = NAMED_CRITICAL "Isar" (fn () => ! global_documents);
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   172
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   173
fun init () = NAMED_CRITICAL "Isar" (fn () =>
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   174
 (global_states := Symtab.empty;
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   175
  global_commands := Symtab.empty;
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   176
  global_documents := Symtab.empty));
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   177
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   178
end;
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   179
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   180
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   181
fun define_state (id: state_id) state =
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   182
  change_states (Symtab.update_new (id, state))
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   183
    handle Symtab.DUP dup => err_dup "state" dup;
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   184
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   185
fun the_state (id: state_id) =
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   186
  (case Symtab.lookup (get_states ()) id of
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   187
    NONE => err_undef "state" id
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   188
  | SOME (State {status as Finished state, ...}) => state
29467
d98fe0c504a8 replaced sys_error by plain error;
wenzelm
parents: 29459
diff changeset
   189
  | _ => error ("Unfinished state " ^ id));
29459
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   190
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
fun define_command id tr =
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   193
  change_commands (Symtab.update_new (id, Toplevel.put_id id tr))
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   194
    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
   195
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   196
fun the_command (id: command_id) =
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   197
  (case Symtab.lookup (get_commands ()) id of
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   198
    NONE => err_undef "command" id
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   199
  | SOME cmd => cmd);
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   200
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   201
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   202
fun define_document (id: document_id) document =
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   203
  change_documents (Symtab.update_new (id, document))
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   204
    handle Symtab.DUP dup => err_dup "document" dup;
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   205
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   206
fun the_document (id: document_id) =
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   207
  (case Symtab.lookup (get_documents ()) id of
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   208
    NONE => err_undef "document" id
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   209
  | SOME doc => doc);
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   210
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   211
29467
d98fe0c504a8 replaced sys_error by plain error;
wenzelm
parents: 29459
diff changeset
   212
(* document editing *)
d98fe0c504a8 replaced sys_error by plain error;
wenzelm
parents: 29459
diff changeset
   213
29459
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   214
fun begin_document (id: document_id) path =
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   215
  let
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   216
    val (dir, name) = ThyLoad.split_thy_path path;
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   217
    val _ = define_command id Toplevel.empty;
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   218
    val _ = define_state id (make_state NONE id (Finished Toplevel.toplevel));
29467
d98fe0c504a8 replaced sys_error by plain error;
wenzelm
parents: 29459
diff changeset
   219
    val entries = Symtab.make [(id, make_entry NONE NONE id)];
d98fe0c504a8 replaced sys_error by plain error;
wenzelm
parents: 29459
diff changeset
   220
    val _ = define_document id (make_document dir name id entries);
29459
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   221
  in () end;
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   222
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   223
fun edit_document (id: document_id) (new_id: document_id) edits =
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   224
  let
29467
d98fe0c504a8 replaced sys_error by plain error;
wenzelm
parents: 29459
diff changeset
   225
    val document' =
d98fe0c504a8 replaced sys_error by plain error;
wenzelm
parents: 29459
diff changeset
   226
      fold (fn (id, SOME id2) => insert_entry (id, id2) | (id, NONE) => delete_after_entry id)
d98fe0c504a8 replaced sys_error by plain error;
wenzelm
parents: 29459
diff changeset
   227
        edits (the_document id);
d98fe0c504a8 replaced sys_error by plain error;
wenzelm
parents: 29459
diff changeset
   228
    (* FIXME update states *)
d98fe0c504a8 replaced sys_error by plain error;
wenzelm
parents: 29459
diff changeset
   229
    val _ = define_document new_id document';
29459
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   230
  in () end;
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   231
29467
d98fe0c504a8 replaced sys_error by plain error;
wenzelm
parents: 29459
diff changeset
   232
fun end_document (id: document_id) = error "FIXME";
29459
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   233
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   234
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   235
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   236
(** concrete syntax **)
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   237
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   238
local structure P = OuterParse structure V = ValueParse in
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   239
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   240
val _ =
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   241
  OuterSyntax.internal_command "Isar.define_command"
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   242
    (P.string -- P.string >> (fn (id, text) =>
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   243
      Toplevel.imperative (fn () =>
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   244
        define_command id (OuterSyntax.prepare_command (Position.id id) text))));
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   245
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   246
val _ =
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   247
  OuterSyntax.internal_command "Isar.begin_document"
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   248
    (P.string -- P.string >> (fn (id, path) =>
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   249
      Toplevel.imperative (fn () => begin_document id (Path.explode path))));
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   250
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   251
val _ =
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   252
  OuterSyntax.internal_command "Isar.edit_document"
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   253
    (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
   254
      >> (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
   255
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   256
val _ =
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   257
  OuterSyntax.internal_command "Isar.end_document"
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   258
    (P.string >> (fn id => Toplevel.imperative (fn () => end_document id)));
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   259
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   260
end;
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   261
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   262
end;
29467
d98fe0c504a8 replaced sys_error by plain error;
wenzelm
parents: 29459
diff changeset
   263