clarified define_command: store name as structural information;
authorwenzelm
Fri Sep 02 11:52:13 2011 +0200 (2011-09-02 ago)
changeset 44644317e4962dd0f
parent 44643 9987ae55e17b
child 44645 5938beb84adc
clarified define_command: store name as structural information;
src/Pure/PIDE/document.ML
src/Pure/PIDE/isar_document.ML
src/Pure/PIDE/isar_document.scala
src/Pure/System/session.scala
     1.1 --- a/src/Pure/PIDE/document.ML	Thu Sep 01 23:08:42 2011 +0200
     1.2 +++ b/src/Pure/PIDE/document.ML	Fri Sep 02 11:52:13 2011 +0200
     1.3 @@ -24,7 +24,7 @@
     1.4    type edit = string * node_edit
     1.5    type state
     1.6    val init_state: state
     1.7 -  val define_command: command_id -> string -> state -> state
     1.8 +  val define_command: command_id -> string -> string -> state -> state
     1.9    val join_commands: state -> state
    1.10    val cancel_execution: state -> Future.task list
    1.11    val update_perspective: version_id -> version_id -> string -> command_id list -> state -> state
    1.12 @@ -233,7 +233,7 @@
    1.13  abstype state = State of
    1.14   {versions: version Inttab.table,  (*version_id -> document content*)
    1.15    commands:
    1.16 -    Toplevel.transition future Inttab.table *  (*command_id -> transition (future parsing)*)
    1.17 +    (string * Toplevel.transition future) Inttab.table *  (*command_id -> name * transition*)
    1.18      Toplevel.transition future list,  (*recent commands to be joined*)
    1.19    execs: (command_id * (Toplevel.state * unit lazy) lazy) Inttab.table,
    1.20      (*exec_id -> command_id with eval/print process*)
    1.21 @@ -248,7 +248,7 @@
    1.22  
    1.23  val init_state =
    1.24    make_state (Inttab.make [(no_id, empty_version)],
    1.25 -    (Inttab.make [(no_id, Future.value Toplevel.empty)], []),
    1.26 +    (Inttab.make [(no_id, (Toplevel.name_of Toplevel.empty, Future.value Toplevel.empty))], []),
    1.27      Inttab.make [(no_id, (no_id, Lazy.value (Toplevel.toplevel, no_print)))],
    1.28      Future.new_group NONE);
    1.29  
    1.30 @@ -269,7 +269,7 @@
    1.31  
    1.32  (* commands *)
    1.33  
    1.34 -fun define_command (id: command_id) text =
    1.35 +fun define_command (id: command_id) name text =
    1.36    map_state (fn (versions, (commands, recent), execs, execution) =>
    1.37      let
    1.38        val id_string = print_id id;
    1.39 @@ -278,14 +278,14 @@
    1.40            Position.setmp_thread_data (Position.id_only id_string)
    1.41              (fn () => Outer_Syntax.read_command (Position.id id_string) text) ());
    1.42        val commands' =
    1.43 -        Inttab.update_new (id, tr) commands
    1.44 +        Inttab.update_new (id, (name, tr)) commands
    1.45            handle Inttab.DUP dup => err_dup "command" dup;
    1.46      in (versions, (commands', tr :: recent), execs, execution) end);
    1.47  
    1.48  fun the_command (State {commands, ...}) (id: command_id) =
    1.49    (case Inttab.lookup (#1 commands) id of
    1.50      NONE => err_undef "command" id
    1.51 -  | SOME tr => tr);
    1.52 +  | SOME command => command);
    1.53  
    1.54  val join_commands =
    1.55      map_state (fn (versions, (commands, recent), execs, execution) =>
    1.56 @@ -400,12 +400,12 @@
    1.57  
    1.58  fun new_exec state init command_id' (execs, exec) =
    1.59    let
    1.60 -    val command' = the_command state command_id';
    1.61 +    val (_, tr0) = the_command state command_id';
    1.62      val exec_id' = new_id ();
    1.63      val exec' =
    1.64        snd exec |> Lazy.map (fn (st, _) =>
    1.65          let val tr =
    1.66 -          Future.join command'
    1.67 +          Future.join tr0
    1.68            |> Toplevel.modify_init init
    1.69            |> Toplevel.put_id (print_id exec_id');
    1.70          in run_command tr st end)
     2.1 --- a/src/Pure/PIDE/isar_document.ML	Thu Sep 01 23:08:42 2011 +0200
     2.2 +++ b/src/Pure/PIDE/isar_document.ML	Fri Sep 02 11:52:13 2011 +0200
     2.3 @@ -9,7 +9,8 @@
     2.4  
     2.5  val _ =
     2.6    Isabelle_Process.add_command "Isar_Document.define_command"
     2.7 -    (fn [id, text] => Document.change_state (Document.define_command (Document.parse_id id) text));
     2.8 +    (fn [id, name, text] =>
     2.9 +      Document.change_state (Document.define_command (Document.parse_id id) name text));
    2.10  
    2.11  val _ =
    2.12    Isabelle_Process.add_command "Isar_Document.cancel_execution"
     3.1 --- a/src/Pure/PIDE/isar_document.scala	Thu Sep 01 23:08:42 2011 +0200
     3.2 +++ b/src/Pure/PIDE/isar_document.scala	Fri Sep 02 11:52:13 2011 +0200
     3.3 @@ -148,8 +148,9 @@
     3.4  {
     3.5    /* commands */
     3.6  
     3.7 -  def define_command(id: Document.Command_ID, text: String): Unit =
     3.8 -    input("Isar_Document.define_command", Document.ID(id), text)
     3.9 +  def define_command(command: Command): Unit =
    3.10 +    input("Isar_Document.define_command",
    3.11 +      Document.ID(command.id), Symbol.encode(command.name), Symbol.encode(command.source))
    3.12  
    3.13  
    3.14    /* document versions */
     4.1 --- a/src/Pure/System/session.scala	Thu Sep 01 23:08:42 2011 +0200
     4.2 +++ b/src/Pure/System/session.scala	Fri Sep 02 11:52:13 2011 +0200
     4.3 @@ -253,7 +253,7 @@
     4.4        {
     4.5          if (!global_state().defined_command(command.id)) {
     4.6            global_state.change(_.define_command(command))
     4.7 -          prover.get.define_command(command.id, Symbol.encode(command.source))
     4.8 +          prover.get.define_command(command)
     4.9          }
    4.10        }
    4.11        doc_edits foreach {