src/Pure/Isar/outer_syntax.ML
changeset 44478 4fdb1009a370
parent 44357 5f5649ac8235
child 44658 5bec9c15ef29
     1.1 --- a/src/Pure/Isar/outer_syntax.ML	Thu Aug 25 17:38:12 2011 +0200
     1.2 +++ b/src/Pure/Isar/outer_syntax.ML	Thu Aug 25 19:12:58 2011 +0200
     1.3 @@ -34,10 +34,10 @@
     1.4    val process_file: Path.T -> theory -> theory
     1.5    type isar
     1.6    val isar: TextIO.instream -> bool -> isar
     1.7 -  val prepare_span: outer_syntax -> Thy_Syntax.span -> Toplevel.transition * bool
     1.8 -  val prepare_element: outer_syntax -> (unit -> theory) -> Thy_Syntax.element ->
     1.9 +  val read_span: outer_syntax -> Thy_Syntax.span -> Toplevel.transition * bool
    1.10 +  val read_element: outer_syntax -> (unit -> theory) -> Thy_Syntax.element ->
    1.11      (Toplevel.transition * Toplevel.transition list) list
    1.12 -  val prepare_command: Position.T -> string -> Toplevel.transition
    1.13 +  val read_command: Position.T -> string -> Toplevel.transition
    1.14  end;
    1.15  
    1.16  structure Outer_Syntax: OUTER_SYNTAX =
    1.17 @@ -251,11 +251,11 @@
    1.18    |> toplevel_source term (SOME true) lookup_commands_dynamic;
    1.19  
    1.20  
    1.21 -(* prepare toplevel commands -- fail-safe *)
    1.22 +(* read toplevel commands -- fail-safe *)
    1.23  
    1.24  val not_singleton = "Exactly one command expected";
    1.25  
    1.26 -fun prepare_span outer_syntax span =
    1.27 +fun read_span outer_syntax span =
    1.28    let
    1.29      val commands = lookup_commands outer_syntax;
    1.30      val range_pos = Position.set_range (Thy_Syntax.span_range span);
    1.31 @@ -272,19 +272,19 @@
    1.32      handle ERROR msg => (Toplevel.malformed range_pos msg, true)
    1.33    end;
    1.34  
    1.35 -fun prepare_element outer_syntax init {head, proof, proper_proof} =
    1.36 +fun read_element outer_syntax init {head, proof, proper_proof} =
    1.37    let
    1.38 -    val (tr, proper_head) = prepare_span outer_syntax head |>> Toplevel.modify_init init;
    1.39 -    val proof_trs = map (prepare_span outer_syntax) proof |> filter #2 |> map #1;
    1.40 +    val (tr, proper_head) = read_span outer_syntax head |>> Toplevel.modify_init init;
    1.41 +    val proof_trs = map (read_span outer_syntax) proof |> filter #2 |> map #1;
    1.42    in
    1.43      if proper_head andalso proper_proof then [(tr, proof_trs)]
    1.44      else map (rpair []) (if proper_head then tr :: proof_trs else proof_trs)
    1.45    end;
    1.46  
    1.47 -fun prepare_command pos str =
    1.48 +fun read_command pos str =
    1.49    let val (lexs, outer_syntax) = get_syntax () in
    1.50      (case Thy_Syntax.parse_spans lexs pos str of
    1.51 -      [span] => #1 (prepare_span outer_syntax span)
    1.52 +      [span] => #1 (read_span outer_syntax span)
    1.53      | _ => Toplevel.malformed pos not_singleton)
    1.54    end;
    1.55