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