src/Pure/Isar/isar_document.ML
author wenzelm
Sun May 30 21:34:19 2010 +0200 (2010-05-30)
changeset 37198 3af985b10550
parent 37184 79fe8e753e84
child 37216 3165bc303f66
permissions -rw-r--r--
replaced ML_Lex.read_antiq by more concise ML_Lex.read, which includes full read/report with explicit position information;
ML_Context.eval/expression expect explicit ML_Lex source, which allows surrounding further text without loosing position information;
fall back on ML_Context.eval_text if there is no position or no surrounding text;
proper Args.name_source_position for method "tactic" and "raw_tactic";
tuned;
     1 (*  Title:      Pure/Isar/isar_document.ML
     2     Author:     Makarius
     3 
     4 Interactive Isar documents.
     5 *)
     6 
     7 structure Isar_Document: sig end =
     8 struct
     9 
    10 (* unique identifiers *)
    11 
    12 type state_id = string;
    13 type command_id = string;
    14 type document_id = string;
    15 
    16 val no_id = "";
    17 
    18 local
    19   val id_count = Synchronized.var "id" 0;
    20 in
    21   fun create_id () =
    22     Synchronized.change_result id_count
    23       (fn i =>
    24         let val i' = i + 1
    25         in ("i" ^ string_of_int i', i') end);
    26 end;
    27 
    28 fun err_dup kind id = error ("Duplicate " ^ kind ^ ": " ^ quote id);
    29 fun err_undef kind id = error ("Undefined " ^ kind ^ ": " ^ quote id);
    30 
    31 
    32 
    33 (** documents **)
    34 
    35 (* command entries *)
    36 
    37 datatype entry = Entry of {next: command_id option, state: state_id option};
    38 fun make_entry next state = Entry {next = next, state = state};
    39 
    40 fun the_entry entries (id: command_id) =
    41   (case Symtab.lookup entries id of
    42     NONE => err_undef "document entry" id
    43   | SOME (Entry entry) => entry);
    44 
    45 fun put_entry (id: command_id, entry: entry) = Symtab.update (id, entry);
    46 
    47 fun put_entry_state (id: command_id) state entries =
    48   let val {next, ...} = the_entry entries id
    49   in put_entry (id, make_entry next state) entries end;
    50 
    51 fun reset_entry_state id = put_entry_state id NONE;
    52 fun set_entry_state (id, state_id) = put_entry_state id (SOME state_id);
    53 
    54 
    55 (* document *)
    56 
    57 datatype document = Document of
    58  {dir: Path.T,                   (*master directory*)
    59   name: string,                  (*theory name*)
    60   entries: entry Symtab.table};  (*unique command entries indexed by command_id, start with no_id*)
    61 
    62 fun make_document dir name entries =
    63   Document {dir = dir, name = name, entries = entries};
    64 
    65 fun map_entries f (Document {dir, name, entries}) =
    66   make_document dir name (f entries);
    67 
    68 
    69 (* iterate entries *)
    70 
    71 fun fold_entries id0 f (Document {entries, ...}) =
    72   let
    73     fun apply NONE x = x
    74       | apply (SOME id) x =
    75           let val entry = the_entry entries id
    76           in apply (#next entry) (f (id, entry) x) end;
    77   in if Symtab.defined entries id0 then apply (SOME id0) else I end;
    78 
    79 fun first_entry P (Document {entries, ...}) =
    80   let
    81     fun first _ NONE = NONE
    82       | first prev (SOME id) =
    83           let val entry = the_entry entries id
    84           in if P (id, entry) then SOME (prev, id, entry) else first (SOME id) (#next entry) end;
    85   in first NONE (SOME no_id) end;
    86 
    87 
    88 (* modify entries *)
    89 
    90 fun insert_after (id: command_id) (id2: command_id) = map_entries (fn entries =>
    91   let val {next, state} = the_entry entries id in
    92     entries
    93     |> put_entry (id, make_entry (SOME id2) state)
    94     |> put_entry (id2, make_entry next NONE)
    95   end);
    96 
    97 fun delete_after (id: command_id) = map_entries (fn entries =>
    98   let val {next, state} = the_entry entries id in
    99     (case next of
   100       NONE => error ("No next entry to delete: " ^ quote id)
   101     | SOME id2 =>
   102         entries |>
   103           (case #next (the_entry entries id2) of
   104             NONE => put_entry (id, make_entry NONE state)
   105           | SOME id3 => put_entry (id, make_entry (SOME id3) state) #> reset_entry_state id3))
   106   end);
   107 
   108 
   109 
   110 (** global configuration **)
   111 
   112 (* states *)
   113 
   114 local
   115 
   116 val global_states = Unsynchronized.ref (Symtab.make [(no_id, Lazy.value (SOME Toplevel.toplevel))]);
   117 
   118 in
   119 
   120 fun define_state (id: state_id) state =
   121   NAMED_CRITICAL "Isar" (fn () =>
   122     Unsynchronized.change global_states (Symtab.update_new (id, state))
   123       handle Symtab.DUP dup => err_dup "state" dup);
   124 
   125 fun the_state (id: state_id) =
   126   (case Symtab.lookup (! global_states) id of
   127     NONE => err_undef "state" id
   128   | SOME state => state);
   129 
   130 end;
   131 
   132 
   133 (* commands *)
   134 
   135 local
   136 
   137 val global_commands = Unsynchronized.ref (Symtab.make [(no_id, Toplevel.empty)]);
   138 
   139 in
   140 
   141 fun define_command (id: command_id) tr =
   142   NAMED_CRITICAL "Isar" (fn () =>
   143     Unsynchronized.change global_commands (Symtab.update_new (id, Toplevel.put_id id tr))
   144       handle Symtab.DUP dup => err_dup "command" dup);
   145 
   146 fun the_command (id: command_id) =
   147   (case Symtab.lookup (! global_commands) id of
   148     NONE => err_undef "command" id
   149   | SOME tr => tr);
   150 
   151 end;
   152 
   153 
   154 (* documents *)
   155 
   156 local
   157 
   158 val global_documents = Unsynchronized.ref (Symtab.empty: document Symtab.table);
   159 
   160 in
   161 
   162 fun define_document (id: document_id) document =
   163   NAMED_CRITICAL "Isar" (fn () =>
   164     Unsynchronized.change global_documents (Symtab.update_new (id, document))
   165       handle Symtab.DUP dup => err_dup "document" dup);
   166 
   167 fun the_document (id: document_id) =
   168   (case Symtab.lookup (! global_documents) id of
   169     NONE => err_undef "document" id
   170   | SOME document => document);
   171 
   172 end;
   173 
   174 
   175 
   176 (** main operations **)
   177 
   178 (* begin/end document *)
   179 
   180 val no_entries = Symtab.make [(no_id, make_entry NONE (SOME no_id))];
   181 
   182 fun begin_document (id: document_id) path =
   183   let
   184     val (dir, name) = ThyLoad.split_thy_path path;
   185     val _ = define_document id (make_document dir name no_entries);
   186   in () end;
   187 
   188 fun end_document (id: document_id) =
   189   NAMED_CRITICAL "Isar" (fn () =>
   190     let
   191       val document as Document {name, ...} = the_document id;
   192       val end_state =
   193         the_state (the (#state (#3 (the
   194           (first_entry (fn (_, {next, ...}) => is_none next) document)))));
   195       val _ =  (* FIXME regular execution (??) *)
   196         Future.fork (fn () =>
   197           (case Lazy.force end_state of
   198             SOME st =>
   199              (Toplevel.run_command name (Toplevel.put_id id (Toplevel.commit_exit Position.none)) st;
   200               ThyInfo.touch_child_thys name;
   201               ThyInfo.register_thy name)
   202           | NONE => error ("Failed to finish theory " ^ quote name)));
   203     in () end);
   204 
   205 
   206 (* document editing *)
   207 
   208 local
   209 
   210 fun is_changed entries' (id, {next = _, state}) =
   211   (case try (the_entry entries') id of
   212     NONE => true
   213   | SOME {next = _, state = state'} => state' <> state);
   214 
   215 fun new_state name (id: command_id) (state_id, updates) =
   216   let
   217     val state = the_state state_id;
   218     val state_id' = create_id ();
   219     val tr = Toplevel.put_id state_id' (the_command id);
   220     val state' =
   221       Lazy.lazy (fn () =>
   222         (case Lazy.force state of
   223           NONE => NONE
   224         | SOME st => Toplevel.run_command name tr st));
   225     val _ = define_state state_id' state';
   226   in (state_id', (id, state_id') :: updates) end;
   227 
   228 fun report_updates updates =
   229   implode (map (fn (id, state_id) => Markup.markup (Markup.edit id state_id) "") updates)
   230   |> Markup.markup Markup.assign
   231   |> Output.status;
   232 
   233 
   234 fun force_state NONE = ()
   235   | force_state (SOME state_id) = ignore (Lazy.force (the_state state_id));
   236 
   237 val execution = Unsynchronized.ref (Future.value ());
   238 
   239 fun execute document =
   240   NAMED_CRITICAL "Isar" (fn () =>
   241     let
   242       val old_execution = ! execution;
   243       val _ = Future.cancel old_execution;
   244       val new_execution = Future.fork (fn () =>
   245        (Future.join_result old_execution;
   246         fold_entries no_id (fn (_, {state, ...}) => fn () => force_state state) document ()));
   247     in execution := new_execution end);
   248 
   249 in
   250 
   251 fun edit_document (old_id: document_id) (new_id: document_id) edits =
   252   NAMED_CRITICAL "Isar" (fn () =>
   253     let
   254       val old_document as Document {name, entries = old_entries, ...} = the_document old_id;
   255       val new_document as Document {entries = new_entries, ...} = old_document
   256         |> fold (fn (id, SOME id2) => insert_after id id2 | (id, NONE) => delete_after id) edits;
   257 
   258       val (updates, new_document') =
   259         (case first_entry (is_changed old_entries) new_document of
   260           NONE => ([], new_document)
   261         | SOME (prev, id, _) =>
   262             let
   263               val prev_state_id = the (#state (the_entry new_entries (the prev)));
   264               val (_, updates) =
   265                 fold_entries id (new_state name o #1) new_document (prev_state_id, []);
   266               val new_document' = new_document |> map_entries (fold set_entry_state updates);
   267             in (rev updates, new_document') end);
   268 
   269       val _ = define_document new_id new_document';
   270       val _ = report_updates updates;
   271       val _ = execute new_document';
   272     in () end);
   273 
   274 end;
   275 
   276 
   277 
   278 (** concrete syntax **)
   279 
   280 val _ =
   281   Outer_Syntax.internal_command "Isar.define_command"
   282     (Parse.string -- Parse.string >> (fn (id, text) =>
   283       Toplevel.position (Position.id_only id) o
   284       Toplevel.imperative (fn () =>
   285         define_command id (Outer_Syntax.prepare_command (Position.id id) text))));
   286 
   287 val _ =
   288   Outer_Syntax.internal_command "Isar.begin_document"
   289     (Parse.string -- Parse.string >> (fn (id, path) =>
   290       Toplevel.imperative (fn () => begin_document id (Path.explode path))));
   291 
   292 val _ =
   293   Outer_Syntax.internal_command "Isar.end_document"
   294     (Parse.string >> (fn id => Toplevel.imperative (fn () => end_document id)));
   295 
   296 val _ =
   297   Outer_Syntax.internal_command "Isar.edit_document"
   298     (Parse.string -- Parse.string --
   299         Parse_Value.list (Parse.string -- (Parse.string >> SOME) || Parse.string >> rpair NONE)
   300       >> (fn ((id, new_id), edits) =>
   301         Toplevel.position (Position.id_only new_id) o
   302         Toplevel.imperative (fn () => edit_document id new_id edits)));
   303 
   304 end;
   305