# HG changeset patch
# User wenzelm
# Date 1314292378 -7200
# Node ID 4fdb1009a3706c4cf27c326c03e4e3eb6fec585b
# Parent  086bb10835528db0c0934583b95fd92636dc1d20
tuned signature -- emphasize traditional read/eval/print terminology, which is still relevant here;

diff -r 086bb1083552 -r 4fdb1009a370 src/Pure/Isar/outer_syntax.ML
--- a/src/Pure/Isar/outer_syntax.ML	Thu Aug 25 17:38:12 2011 +0200
+++ b/src/Pure/Isar/outer_syntax.ML	Thu Aug 25 19:12:58 2011 +0200
@@ -34,10 +34,10 @@
   val process_file: Path.T -> theory -> theory
   type isar
   val isar: TextIO.instream -> bool -> isar
-  val prepare_span: outer_syntax -> Thy_Syntax.span -> Toplevel.transition * bool
-  val prepare_element: outer_syntax -> (unit -> theory) -> Thy_Syntax.element ->
+  val read_span: outer_syntax -> Thy_Syntax.span -> Toplevel.transition * bool
+  val read_element: outer_syntax -> (unit -> theory) -> Thy_Syntax.element ->
     (Toplevel.transition * Toplevel.transition list) list
-  val prepare_command: Position.T -> string -> Toplevel.transition
+  val read_command: Position.T -> string -> Toplevel.transition
 end;
 
 structure Outer_Syntax: OUTER_SYNTAX =
@@ -251,11 +251,11 @@
   |> toplevel_source term (SOME true) lookup_commands_dynamic;
 
 
-(* prepare toplevel commands -- fail-safe *)
+(* read toplevel commands -- fail-safe *)
 
 val not_singleton = "Exactly one command expected";
 
-fun prepare_span outer_syntax span =
+fun read_span outer_syntax span =
   let
     val commands = lookup_commands outer_syntax;
     val range_pos = Position.set_range (Thy_Syntax.span_range span);
@@ -272,19 +272,19 @@
     handle ERROR msg => (Toplevel.malformed range_pos msg, true)
   end;
 
-fun prepare_element outer_syntax init {head, proof, proper_proof} =
+fun read_element outer_syntax init {head, proof, proper_proof} =
   let
-    val (tr, proper_head) = prepare_span outer_syntax head |>> Toplevel.modify_init init;
-    val proof_trs = map (prepare_span outer_syntax) proof |> filter #2 |> map #1;
+    val (tr, proper_head) = read_span outer_syntax head |>> Toplevel.modify_init init;
+    val proof_trs = map (read_span outer_syntax) proof |> filter #2 |> map #1;
   in
     if proper_head andalso proper_proof then [(tr, proof_trs)]
     else map (rpair []) (if proper_head then tr :: proof_trs else proof_trs)
   end;
 
-fun prepare_command pos str =
+fun read_command pos str =
   let val (lexs, outer_syntax) = get_syntax () in
     (case Thy_Syntax.parse_spans lexs pos str of
-      [span] => #1 (prepare_span outer_syntax span)
+      [span] => #1 (read_span outer_syntax span)
     | _ => Toplevel.malformed pos not_singleton)
   end;
 
diff -r 086bb1083552 -r 4fdb1009a370 src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Thu Aug 25 17:38:12 2011 +0200
+++ b/src/Pure/PIDE/document.ML	Thu Aug 25 19:12:58 2011 +0200
@@ -2,7 +2,7 @@
     Author:     Makarius
 
 Document as collection of named nodes, each consisting of an editable
-list of commands, associated with asynchronous execution process.
+list of commands, with asynchronous read/eval/print processes.
 *)
 
 signature DOCUMENT =
@@ -265,7 +265,7 @@
       val tr =
         Future.fork_pri 2 (fn () =>
           Position.setmp_thread_data (Position.id_only id_string)
-            (fn () => Outer_Syntax.prepare_command (Position.id id_string) text) ());
+            (fn () => Outer_Syntax.read_command (Position.id id_string) text) ());
       val commands' =
         Inttab.update_new (id, tr) commands
           handle Inttab.DUP dup => err_dup "command" dup;
diff -r 086bb1083552 -r 4fdb1009a370 src/Pure/Thy/thy_load.ML
--- a/src/Pure/Thy/thy_load.ML	Thu Aug 25 17:38:12 2011 +0200
+++ b/src/Pure/Thy/thy_load.ML	Thu Aug 25 19:12:58 2011 +0200
@@ -175,7 +175,7 @@
     val spans = Source.exhaust (Thy_Syntax.span_source toks);
     val elements =
       Source.exhaust (Thy_Syntax.element_source (Source.of_list spans))
-      |> maps (Outer_Syntax.prepare_element outer_syntax init);
+      |> maps (Outer_Syntax.read_element outer_syntax init);
 
     val _ = Present.theory_source name
       (fn () => HTML.html_mode (implode o map Thy_Syntax.present_span) spans);