tuned signature;
authorwenzelm
Fri Aug 26 16:06:58 2011 +0200 (2011-08-26)
changeset 44481bb42bc831570
parent 44480 38c5b085fb1c
child 44482 c7225307acf2
tuned signature;
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	Fri Aug 26 15:56:30 2011 +0200
     1.2 +++ b/src/Pure/PIDE/document.ML	Fri Aug 26 16:06:58 2011 +0200
     1.3 @@ -28,7 +28,7 @@
     1.4    val join_commands: state -> unit
     1.5    val cancel_execution: state -> Future.task list
     1.6    val update_perspective: version_id -> version_id -> string -> command_id list -> state -> state
     1.7 -  val edit: version_id -> version_id -> edit list -> state ->
     1.8 +  val update: version_id -> version_id -> edit list -> state ->
     1.9      ((command_id * exec_id option) list * (string * command_id option) list) * state
    1.10    val execute: version_id -> state -> state
    1.11    val state: unit -> state
    1.12 @@ -365,7 +365,7 @@
    1.13  
    1.14  
    1.15  
    1.16 -(** editing **)
    1.17 +(** update **)
    1.18  
    1.19  (* perspective *)
    1.20  
    1.21 @@ -377,7 +377,7 @@
    1.22    in define_version new_id new_version state end;
    1.23  
    1.24  
    1.25 -(* edit *)
    1.26 +(* edits *)
    1.27  
    1.28  local
    1.29  
    1.30 @@ -417,7 +417,7 @@
    1.31  
    1.32  in
    1.33  
    1.34 -fun edit (old_id: version_id) (new_id: version_id) edits state =
    1.35 +fun update (old_id: version_id) (new_id: version_id) edits state =
    1.36    let
    1.37      val old_version = the_version state old_id;
    1.38      val _ = Time.now ();  (* FIXME odd workaround for polyml-5.4.0/x86_64 *)
    1.39 @@ -436,7 +436,7 @@
    1.40                  NONE => Future.value (([], [], []), set_touched false node)
    1.41                | SOME (entry as ((prev, id), _)) =>
    1.42                    (singleton o Future.forks)
    1.43 -                    {name = "Document.edit", group = NONE,
    1.44 +                    {name = "Document.update", group = NONE,
    1.45                        deps = map (Future.task_of o #2) deps, pri = 0, interrupts = false}
    1.46                      (fn () =>
    1.47                        let
     2.1 --- a/src/Pure/PIDE/isar_document.ML	Fri Aug 26 15:56:30 2011 +0200
     2.2 +++ b/src/Pure/PIDE/isar_document.ML	Fri Aug 26 16:06:58 2011 +0200
     2.3 @@ -28,7 +28,7 @@
     2.4        end));
     2.5  
     2.6  val _ =
     2.7 -  Isabelle_Process.add_command "Isar_Document.edit_version"
     2.8 +  Isabelle_Process.add_command "Isar_Document.update"
     2.9      (fn [old_id_string, new_id_string, edits_yxml] => Document.change_state (fn state =>
    2.10        let
    2.11          val old_id = Document.parse_id old_id_string;
    2.12 @@ -48,7 +48,7 @@
    2.13              end;
    2.14  
    2.15          val running = Document.cancel_execution state;
    2.16 -        val (assignment, state') = Document.edit old_id new_id edits state;
    2.17 +        val (assignment, state') = Document.update old_id new_id edits state;
    2.18          val _ = Future.join_tasks running;
    2.19          val _ = Document.join_commands state';
    2.20          val _ =
     3.1 --- a/src/Pure/PIDE/isar_document.scala	Fri Aug 26 15:56:30 2011 +0200
     3.2 +++ b/src/Pure/PIDE/isar_document.scala	Fri Aug 26 16:06:58 2011 +0200
     3.3 @@ -146,7 +146,7 @@
     3.4        YXML.string_of_body(ids))
     3.5    }
     3.6  
     3.7 -  def edit_version(old_id: Document.Version_ID, new_id: Document.Version_ID,
     3.8 +  def update(old_id: Document.Version_ID, new_id: Document.Version_ID,
     3.9      edits: List[Document.Edit_Command])
    3.10    {
    3.11      val edits_yxml =
    3.12 @@ -163,7 +163,7 @@
    3.13              { case Document.Node.Perspective(a) => (a.commands.map(c => long_atom(c.id)), Nil) }))))
    3.14        YXML.string_of_body(encode(edits)) }
    3.15  
    3.16 -    input("Isar_Document.edit_version", Document.ID(old_id), Document.ID(new_id), edits_yxml)
    3.17 +    input("Isar_Document.update", Document.ID(old_id), Document.ID(new_id), edits_yxml)
    3.18    }
    3.19  
    3.20  
     4.1 --- a/src/Pure/System/session.scala	Fri Aug 26 15:56:30 2011 +0200
     4.2 +++ b/src/Pure/System/session.scala	Fri Aug 26 16:06:58 2011 +0200
     4.3 @@ -282,7 +282,7 @@
     4.4  
     4.5        val assignment = global_state().the_assignment(previous).check_finished
     4.6        global_state.change(_.define_version(version, assignment))
     4.7 -      prover.get.edit_version(previous.id, version.id, doc_edits)
     4.8 +      prover.get.update(previous.id, version.id, doc_edits)
     4.9      }
    4.10      //}}}
    4.11