src/Pure/Isar/isar_document.ML
author wenzelm
Thu, 15 Jan 2009 12:16:51 +0100
changeset 29490 8f0a481199e7
parent 29489 5dfe03f423c4
child 29499 2819ba5f0c32
permissions -rw-r--r--
tuned;
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
29468
c9bb4e06d173 misc internal rearrangements;
wenzelm
parents: 29467
diff changeset
    14
  val end_document: document_id -> unit
29459
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
    15
  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
    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
29484
15863d782ae3 misc cleanup and simplification;
wenzelm
parents: 29468
diff changeset
    23
type state_id = string;
29459
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
    24
type command_id = string;
29484
15863d782ae3 misc cleanup and simplification;
wenzelm
parents: 29468
diff changeset
    25
type document_id = string;
29459
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
    26
29468
c9bb4e06d173 misc internal rearrangements;
wenzelm
parents: 29467
diff changeset
    27
fun new_id () = "isabelle:" ^ serial_string ();
29467
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
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
    34
(** documents **)
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
    35
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
    36
(* command entries *)
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
    37
29484
15863d782ae3 misc cleanup and simplification;
wenzelm
parents: 29468
diff changeset
    38
datatype entry = Entry of {next: command_id option, state: state_id option};
15863d782ae3 misc cleanup and simplification;
wenzelm
parents: 29468
diff changeset
    39
fun make_entry next state = Entry {next = next, state = state};
29459
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
    40
29467
d98fe0c504a8 replaced sys_error by plain error;
wenzelm
parents: 29459
diff changeset
    41
fun the_entry entries (id: command_id) =
d98fe0c504a8 replaced sys_error by plain error;
wenzelm
parents: 29459
diff changeset
    42
  (case Symtab.lookup entries id of
d98fe0c504a8 replaced sys_error by plain error;
wenzelm
parents: 29459
diff changeset
    43
    NONE => err_undef "document entry" id
d98fe0c504a8 replaced sys_error by plain error;
wenzelm
parents: 29459
diff changeset
    44
  | SOME (Entry entry) => entry);
d98fe0c504a8 replaced sys_error by plain error;
wenzelm
parents: 29459
diff changeset
    45
d98fe0c504a8 replaced sys_error by plain error;
wenzelm
parents: 29459
diff changeset
    46
fun put_entry (id: command_id, entry: entry) = Symtab.update (id, entry);
d98fe0c504a8 replaced sys_error by plain error;
wenzelm
parents: 29459
diff changeset
    47
29489
5dfe03f423c4 edit_document: proper edits/edit markup, including the document id;
wenzelm
parents: 29487
diff changeset
    48
fun put_entry_state (id: command_id) state entries =
5dfe03f423c4 edit_document: proper edits/edit markup, including the document id;
wenzelm
parents: 29487
diff changeset
    49
  let val {next, ...} = the_entry entries id
5dfe03f423c4 edit_document: proper edits/edit markup, including the document id;
wenzelm
parents: 29487
diff changeset
    50
  in put_entry (id, make_entry next state) entries end;
5dfe03f423c4 edit_document: proper edits/edit markup, including the document id;
wenzelm
parents: 29487
diff changeset
    51
29490
wenzelm
parents: 29489
diff changeset
    52
fun reset_entry_state id = put_entry_state id NONE;
wenzelm
parents: 29489
diff changeset
    53
fun set_entry_state (id, state_id) = put_entry_state id (SOME state_id);
29489
5dfe03f423c4 edit_document: proper edits/edit markup, including the document id;
wenzelm
parents: 29487
diff changeset
    54
5dfe03f423c4 edit_document: proper edits/edit markup, including the document id;
wenzelm
parents: 29487
diff changeset
    55
29459
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
    56
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
    57
(* document *)
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
datatype document = Document of
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
    60
 {dir: Path.T,                    (*master directory*)
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
    61
  name: string,                   (*theory name*)
29467
d98fe0c504a8 replaced sys_error by plain error;
wenzelm
parents: 29459
diff changeset
    62
  start: command_id,              (*empty start command*)
d98fe0c504a8 replaced sys_error by plain error;
wenzelm
parents: 29459
diff changeset
    63
  entries: entry Symtab.table};   (*unique command entries indexed by command_id*)
d98fe0c504a8 replaced sys_error by plain error;
wenzelm
parents: 29459
diff changeset
    64
d98fe0c504a8 replaced sys_error by plain error;
wenzelm
parents: 29459
diff changeset
    65
fun make_document dir name start entries =
d98fe0c504a8 replaced sys_error by plain error;
wenzelm
parents: 29459
diff changeset
    66
  Document {dir = dir, name = name, start = start, entries = entries};
d98fe0c504a8 replaced sys_error by plain error;
wenzelm
parents: 29459
diff changeset
    67
d98fe0c504a8 replaced sys_error by plain error;
wenzelm
parents: 29459
diff changeset
    68
fun map_entries f (Document {dir, name, start, entries}) =
d98fe0c504a8 replaced sys_error by plain error;
wenzelm
parents: 29459
diff changeset
    69
  make_document dir name start (f entries);
d98fe0c504a8 replaced sys_error by plain error;
wenzelm
parents: 29459
diff changeset
    70
d98fe0c504a8 replaced sys_error by plain error;
wenzelm
parents: 29459
diff changeset
    71
29484
15863d782ae3 misc cleanup and simplification;
wenzelm
parents: 29468
diff changeset
    72
(* iterate entries *)
29468
c9bb4e06d173 misc internal rearrangements;
wenzelm
parents: 29467
diff changeset
    73
c9bb4e06d173 misc internal rearrangements;
wenzelm
parents: 29467
diff changeset
    74
fun fold_entries opt_id f (Document {start, entries, ...}) =
c9bb4e06d173 misc internal rearrangements;
wenzelm
parents: 29467
diff changeset
    75
  let
c9bb4e06d173 misc internal rearrangements;
wenzelm
parents: 29467
diff changeset
    76
    fun apply NONE x = x
c9bb4e06d173 misc internal rearrangements;
wenzelm
parents: 29467
diff changeset
    77
      | apply (SOME id) x = apply (#next (the_entry entries id)) (f id x);
c9bb4e06d173 misc internal rearrangements;
wenzelm
parents: 29467
diff changeset
    78
  in if is_some opt_id then apply opt_id else apply (SOME start) end;
c9bb4e06d173 misc internal rearrangements;
wenzelm
parents: 29467
diff changeset
    79
29484
15863d782ae3 misc cleanup and simplification;
wenzelm
parents: 29468
diff changeset
    80
fun find_entries P (Document {start, entries, ...}) =
29467
d98fe0c504a8 replaced sys_error by plain error;
wenzelm
parents: 29459
diff changeset
    81
  let
29484
15863d782ae3 misc cleanup and simplification;
wenzelm
parents: 29468
diff changeset
    82
    fun find _ NONE = NONE
15863d782ae3 misc cleanup and simplification;
wenzelm
parents: 29468
diff changeset
    83
      | find prev (SOME id) =
15863d782ae3 misc cleanup and simplification;
wenzelm
parents: 29468
diff changeset
    84
          if P id then SOME (prev, id)
15863d782ae3 misc cleanup and simplification;
wenzelm
parents: 29468
diff changeset
    85
          else find (SOME id) (#next (the_entry entries id));
15863d782ae3 misc cleanup and simplification;
wenzelm
parents: 29468
diff changeset
    86
  in find NONE (SOME start) end;
29468
c9bb4e06d173 misc internal rearrangements;
wenzelm
parents: 29467
diff changeset
    87
c9bb4e06d173 misc internal rearrangements;
wenzelm
parents: 29467
diff changeset
    88
c9bb4e06d173 misc internal rearrangements;
wenzelm
parents: 29467
diff changeset
    89
(* modify entries *)
29459
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
    90
29484
15863d782ae3 misc cleanup and simplification;
wenzelm
parents: 29468
diff changeset
    91
fun insert_after (id: command_id) (id2: command_id) = map_entries (fn entries =>
15863d782ae3 misc cleanup and simplification;
wenzelm
parents: 29468
diff changeset
    92
  let val {next, state} = the_entry entries id in
15863d782ae3 misc cleanup and simplification;
wenzelm
parents: 29468
diff changeset
    93
    entries
15863d782ae3 misc cleanup and simplification;
wenzelm
parents: 29468
diff changeset
    94
    |> put_entry (id, make_entry (SOME id2) state)
15863d782ae3 misc cleanup and simplification;
wenzelm
parents: 29468
diff changeset
    95
    |> put_entry (id2, make_entry next NONE)
29467
d98fe0c504a8 replaced sys_error by plain error;
wenzelm
parents: 29459
diff changeset
    96
  end);
d98fe0c504a8 replaced sys_error by plain error;
wenzelm
parents: 29459
diff changeset
    97
29468
c9bb4e06d173 misc internal rearrangements;
wenzelm
parents: 29467
diff changeset
    98
fun delete_after (id: command_id) = map_entries (fn entries =>
29484
15863d782ae3 misc cleanup and simplification;
wenzelm
parents: 29468
diff changeset
    99
  let val {next, state} = the_entry entries id in
15863d782ae3 misc cleanup and simplification;
wenzelm
parents: 29468
diff changeset
   100
    (case next of
15863d782ae3 misc cleanup and simplification;
wenzelm
parents: 29468
diff changeset
   101
      NONE => error ("No next entry to delete: " ^ quote id)
15863d782ae3 misc cleanup and simplification;
wenzelm
parents: 29468
diff changeset
   102
    | SOME id2 =>
15863d782ae3 misc cleanup and simplification;
wenzelm
parents: 29468
diff changeset
   103
        entries |>
29467
d98fe0c504a8 replaced sys_error by plain error;
wenzelm
parents: 29459
diff changeset
   104
          (case #next (the_entry entries id2) of
29484
15863d782ae3 misc cleanup and simplification;
wenzelm
parents: 29468
diff changeset
   105
            NONE => put_entry (id, make_entry NONE state)
29490
wenzelm
parents: 29489
diff changeset
   106
          | SOME id3 => put_entry (id, make_entry (SOME id3) state) #> reset_entry_state id3))
29467
d98fe0c504a8 replaced sys_error by plain error;
wenzelm
parents: 29459
diff changeset
   107
  end);
29459
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   108
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
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   111
(** global configuration **)
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
local
29484
15863d782ae3 misc cleanup and simplification;
wenzelm
parents: 29468
diff changeset
   114
  val global_states = ref (Symtab.empty: Toplevel.state option future Symtab.table);
29459
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   115
  val global_commands = ref (Symtab.empty: Toplevel.transition Symtab.table);
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   116
  val global_documents = ref (Symtab.empty: document Symtab.table);
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   117
in
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   118
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   119
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
   120
fun get_states () = NAMED_CRITICAL "Isar" (fn () => ! global_states);
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   121
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   122
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
   123
fun get_commands () = NAMED_CRITICAL "Isar" (fn () => ! global_commands);
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 change_documents f = NAMED_CRITICAL "Isar" (fn () => change global_documents f);
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   126
fun get_documents () = NAMED_CRITICAL "Isar" (fn () => ! global_documents);
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   127
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   128
fun init () = NAMED_CRITICAL "Isar" (fn () =>
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   129
 (global_states := Symtab.empty;
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   130
  global_commands := Symtab.empty;
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   131
  global_documents := Symtab.empty));
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   132
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   133
end;
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   134
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 define_state (id: state_id) state =
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   137
  change_states (Symtab.update_new (id, state))
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   138
    handle Symtab.DUP dup => err_dup "state" dup;
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   139
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   140
fun the_state (id: state_id) =
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   141
  (case Symtab.lookup (get_states ()) id of
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   142
    NONE => err_undef "state" id
29484
15863d782ae3 misc cleanup and simplification;
wenzelm
parents: 29468
diff changeset
   143
  | SOME state => state);
29459
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   144
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 define_command id tr =
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   147
  change_commands (Symtab.update_new (id, Toplevel.put_id id tr))
29484
15863d782ae3 misc cleanup and simplification;
wenzelm
parents: 29468
diff changeset
   148
    handle Symtab.DUP dup => err_dup "command" dup;
29459
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   149
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   150
fun the_command (id: command_id) =
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   151
  (case Symtab.lookup (get_commands ()) id of
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   152
    NONE => err_undef "command" id
29468
c9bb4e06d173 misc internal rearrangements;
wenzelm
parents: 29467
diff changeset
   153
  | SOME tr => tr);
29459
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
fun define_document (id: document_id) document =
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   157
  change_documents (Symtab.update_new (id, document))
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   158
    handle Symtab.DUP dup => err_dup "document" dup;
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   159
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   160
fun the_document (id: document_id) =
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   161
  (case Symtab.lookup (get_documents ()) id of
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   162
    NONE => err_undef "document" id
29468
c9bb4e06d173 misc internal rearrangements;
wenzelm
parents: 29467
diff changeset
   163
  | SOME (Document doc) => doc);
29459
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   164
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   165
29468
c9bb4e06d173 misc internal rearrangements;
wenzelm
parents: 29467
diff changeset
   166
(* begin/end document *)
29467
d98fe0c504a8 replaced sys_error by plain error;
wenzelm
parents: 29459
diff changeset
   167
29459
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   168
fun begin_document (id: document_id) path =
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   169
  let
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   170
    val (dir, name) = ThyLoad.split_thy_path path;
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   171
    val _ = define_command id Toplevel.empty;
29484
15863d782ae3 misc cleanup and simplification;
wenzelm
parents: 29468
diff changeset
   172
    val _ = define_state id (Future.value (SOME Toplevel.toplevel));
15863d782ae3 misc cleanup and simplification;
wenzelm
parents: 29468
diff changeset
   173
    val entries = Symtab.make [(id, make_entry NONE (SOME id))];
29467
d98fe0c504a8 replaced sys_error by plain error;
wenzelm
parents: 29459
diff changeset
   174
    val _ = define_document id (make_document dir name id entries);
29459
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   175
  in () end;
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   176
29468
c9bb4e06d173 misc internal rearrangements;
wenzelm
parents: 29467
diff changeset
   177
fun end_document (id: document_id) = error "FIXME";
c9bb4e06d173 misc internal rearrangements;
wenzelm
parents: 29467
diff changeset
   178
c9bb4e06d173 misc internal rearrangements;
wenzelm
parents: 29467
diff changeset
   179
c9bb4e06d173 misc internal rearrangements;
wenzelm
parents: 29467
diff changeset
   180
(* document editing *)
c9bb4e06d173 misc internal rearrangements;
wenzelm
parents: 29467
diff changeset
   181
29484
15863d782ae3 misc cleanup and simplification;
wenzelm
parents: 29468
diff changeset
   182
fun update_state tr state = Future.fork_deps [state] (fn () =>
15863d782ae3 misc cleanup and simplification;
wenzelm
parents: 29468
diff changeset
   183
  (case Future.join state of NONE => NONE | SOME st => Toplevel.run_command tr st));
15863d782ae3 misc cleanup and simplification;
wenzelm
parents: 29468
diff changeset
   184
15863d782ae3 misc cleanup and simplification;
wenzelm
parents: 29468
diff changeset
   185
fun update_states old_document new_document =
29459
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   186
  let
29468
c9bb4e06d173 misc internal rearrangements;
wenzelm
parents: 29467
diff changeset
   187
    val Document {entries = old_entries, ...} = old_document;
c9bb4e06d173 misc internal rearrangements;
wenzelm
parents: 29467
diff changeset
   188
    val Document {entries = new_entries, ...} = new_document;
c9bb4e06d173 misc internal rearrangements;
wenzelm
parents: 29467
diff changeset
   189
c9bb4e06d173 misc internal rearrangements;
wenzelm
parents: 29467
diff changeset
   190
    fun is_changed id =
c9bb4e06d173 misc internal rearrangements;
wenzelm
parents: 29467
diff changeset
   191
      (case try (the_entry new_entries) id of
c9bb4e06d173 misc internal rearrangements;
wenzelm
parents: 29467
diff changeset
   192
        SOME {state = SOME _, ...} => false
c9bb4e06d173 misc internal rearrangements;
wenzelm
parents: 29467
diff changeset
   193
      | _ => true);
c9bb4e06d173 misc internal rearrangements;
wenzelm
parents: 29467
diff changeset
   194
c9bb4e06d173 misc internal rearrangements;
wenzelm
parents: 29467
diff changeset
   195
    fun cancel_state id () =
c9bb4e06d173 misc internal rearrangements;
wenzelm
parents: 29467
diff changeset
   196
      (case the_entry old_entries id of
29484
15863d782ae3 misc cleanup and simplification;
wenzelm
parents: 29468
diff changeset
   197
        {state = SOME state_id, ...} => Future.cancel (the_state state_id)
29468
c9bb4e06d173 misc internal rearrangements;
wenzelm
parents: 29467
diff changeset
   198
      | _ => ());
c9bb4e06d173 misc internal rearrangements;
wenzelm
parents: 29467
diff changeset
   199
29484
15863d782ae3 misc cleanup and simplification;
wenzelm
parents: 29468
diff changeset
   200
    fun new_state id (state_id, updates) =
29468
c9bb4e06d173 misc internal rearrangements;
wenzelm
parents: 29467
diff changeset
   201
      let
29484
15863d782ae3 misc cleanup and simplification;
wenzelm
parents: 29468
diff changeset
   202
        val state_id' = new_id ();
15863d782ae3 misc cleanup and simplification;
wenzelm
parents: 29468
diff changeset
   203
        val state' = update_state (the_command id) (the_state state_id);
15863d782ae3 misc cleanup and simplification;
wenzelm
parents: 29468
diff changeset
   204
        val _ = define_state state_id' state';
15863d782ae3 misc cleanup and simplification;
wenzelm
parents: 29468
diff changeset
   205
      in (state_id', (id, state_id') :: updates) end;
29468
c9bb4e06d173 misc internal rearrangements;
wenzelm
parents: 29467
diff changeset
   206
  in
29484
15863d782ae3 misc cleanup and simplification;
wenzelm
parents: 29468
diff changeset
   207
    (case find_entries is_changed old_document of
29489
5dfe03f423c4 edit_document: proper edits/edit markup, including the document id;
wenzelm
parents: 29487
diff changeset
   208
      NONE => ([], new_document)
29484
15863d782ae3 misc cleanup and simplification;
wenzelm
parents: 29468
diff changeset
   209
    | SOME (prev, id) =>
29468
c9bb4e06d173 misc internal rearrangements;
wenzelm
parents: 29467
diff changeset
   210
        let
c9bb4e06d173 misc internal rearrangements;
wenzelm
parents: 29467
diff changeset
   211
          val _ = fold_entries (SOME id) cancel_state old_document ();
29484
15863d782ae3 misc cleanup and simplification;
wenzelm
parents: 29468
diff changeset
   212
          val prev_state_id = the (#state (the_entry new_entries (the prev)));
15863d782ae3 misc cleanup and simplification;
wenzelm
parents: 29468
diff changeset
   213
          val (_, updates) = fold_entries (SOME id) new_state new_document (prev_state_id, []);
29490
wenzelm
parents: 29489
diff changeset
   214
          val new_document' = new_document |> map_entries (fold set_entry_state updates);
29489
5dfe03f423c4 edit_document: proper edits/edit markup, including the document id;
wenzelm
parents: 29487
diff changeset
   215
        in (updates, new_document') end)
29468
c9bb4e06d173 misc internal rearrangements;
wenzelm
parents: 29467
diff changeset
   216
  end;
c9bb4e06d173 misc internal rearrangements;
wenzelm
parents: 29467
diff changeset
   217
29489
5dfe03f423c4 edit_document: proper edits/edit markup, including the document id;
wenzelm
parents: 29487
diff changeset
   218
fun report_updates _ [] = ()
5dfe03f423c4 edit_document: proper edits/edit markup, including the document id;
wenzelm
parents: 29487
diff changeset
   219
  | report_updates (document_id: document_id) updates =
5dfe03f423c4 edit_document: proper edits/edit markup, including the document id;
wenzelm
parents: 29487
diff changeset
   220
      implode (map (fn (id, state_id) => Markup.markup (Markup.edit id state_id) "") updates)
5dfe03f423c4 edit_document: proper edits/edit markup, including the document id;
wenzelm
parents: 29487
diff changeset
   221
      |> Markup.markup (Markup.edits document_id)
5dfe03f423c4 edit_document: proper edits/edit markup, including the document id;
wenzelm
parents: 29487
diff changeset
   222
      |> Output.status;
5dfe03f423c4 edit_document: proper edits/edit markup, including the document id;
wenzelm
parents: 29487
diff changeset
   223
29468
c9bb4e06d173 misc internal rearrangements;
wenzelm
parents: 29467
diff changeset
   224
fun edit_document (id: document_id) (id': document_id) edits =
c9bb4e06d173 misc internal rearrangements;
wenzelm
parents: 29467
diff changeset
   225
  let
c9bb4e06d173 misc internal rearrangements;
wenzelm
parents: 29467
diff changeset
   226
    val document = Document (the_document id);
29489
5dfe03f423c4 edit_document: proper edits/edit markup, including the document id;
wenzelm
parents: 29487
diff changeset
   227
    val (updates, document') =
29468
c9bb4e06d173 misc internal rearrangements;
wenzelm
parents: 29467
diff changeset
   228
      document
29484
15863d782ae3 misc cleanup and simplification;
wenzelm
parents: 29468
diff changeset
   229
      |> fold (fn (id, SOME id2) => insert_after id id2 | (id, NONE) => delete_after id) edits
15863d782ae3 misc cleanup and simplification;
wenzelm
parents: 29468
diff changeset
   230
      |> update_states document;
29468
c9bb4e06d173 misc internal rearrangements;
wenzelm
parents: 29467
diff changeset
   231
    val _ = define_document id' document';
29489
5dfe03f423c4 edit_document: proper edits/edit markup, including the document id;
wenzelm
parents: 29487
diff changeset
   232
    val _ = report_updates id' updates;
29459
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   233
  in () end;
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
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   237
(** concrete syntax **)
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   238
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   239
local structure P = OuterParse structure V = ValueParse in
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   240
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   241
val _ =
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   242
  OuterSyntax.internal_command "Isar.define_command"
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   243
    (P.string -- P.string >> (fn (id, text) =>
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   244
      Toplevel.imperative (fn () =>
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   245
        define_command id (OuterSyntax.prepare_command (Position.id id) text))));
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   246
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   247
val _ =
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   248
  OuterSyntax.internal_command "Isar.begin_document"
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   249
    (P.string -- P.string >> (fn (id, path) =>
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   250
      Toplevel.imperative (fn () => begin_document id (Path.explode path))));
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   251
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   252
val _ =
29468
c9bb4e06d173 misc internal rearrangements;
wenzelm
parents: 29467
diff changeset
   253
  OuterSyntax.internal_command "Isar.end_document"
c9bb4e06d173 misc internal rearrangements;
wenzelm
parents: 29467
diff changeset
   254
    (P.string >> (fn id => Toplevel.imperative (fn () => end_document id)));
c9bb4e06d173 misc internal rearrangements;
wenzelm
parents: 29467
diff changeset
   255
c9bb4e06d173 misc internal rearrangements;
wenzelm
parents: 29467
diff changeset
   256
val _ =
29459
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   257
  OuterSyntax.internal_command "Isar.edit_document"
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   258
    (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
   259
      >> (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
   260
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   261
end;
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   262
8acad4f0a727 added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff changeset
   263
end;
29467
d98fe0c504a8 replaced sys_error by plain error;
wenzelm
parents: 29459
diff changeset
   264