--- a/src/Pure/Isar/outer_syntax.ML Sun Aug 15 20:13:07 2010 +0200
+++ b/src/Pure/Isar/outer_syntax.ML Sun Aug 15 20:19:56 2010 +0200
@@ -249,7 +249,7 @@
handle ERROR msg => (Toplevel.malformed range_pos msg, true)
end;
-fun prepare_unit commands init (cmd, proof, proper_proof) =
+fun prepare_atom commands init (cmd, proof, proper_proof) =
let
val (tr, proper_cmd) = prepare_span commands cmd |>> Toplevel.modify_init init;
val proof_trs = map (prepare_span commands) proof |> filter #2 |> map #1;
@@ -278,14 +278,14 @@
val toks = Source.exhausted (Thy_Syntax.token_source lexs pos (Source.of_string text));
val spans = Source.exhaust (Thy_Syntax.span_source toks);
val _ = List.app Thy_Syntax.report_span spans; (* FIXME ?? *)
- val units = Source.exhaust (Thy_Syntax.unit_source (Source.of_list spans))
- |> Par_List.map (prepare_unit commands init) |> flat;
+ val atoms = Source.exhaust (Thy_Syntax.atom_source (Source.of_list spans))
+ |> Par_List.map (prepare_atom commands init) |> flat;
val _ = Present.theory_source name
(fn () => HTML.html_mode (implode o map Thy_Syntax.present_span) spans);
val _ = if time then writeln ("\n**** Starting theory " ^ quote name ^ " ****") else ();
- val (results, thy) = cond_timeit time "" (fn () => Toplevel.excursion units);
+ val (results, thy) = cond_timeit time "" (fn () => Toplevel.excursion atoms);
val _ = if time then writeln ("**** Finished theory " ^ quote name ^ " ****\n") else ();
fun after_load () =
--- a/src/Pure/Thy/thy_syntax.ML Sun Aug 15 20:13:07 2010 +0200
+++ b/src/Pure/Thy/thy_syntax.ML Sun Aug 15 20:19:56 2010 +0200
@@ -21,7 +21,7 @@
val parse_spans: Scan.lexicon * Scan.lexicon -> Position.T -> string -> span list
val present_span: span -> output
val report_span: span -> unit
- val unit_source: (span, 'a) Source.source ->
+ val atom_source: (span, 'a) Source.source ->
(span * span list * bool, (span, 'a) Source.source) Source.source
end;
@@ -160,7 +160,7 @@
-(** units: commands with proof **)
+(** specification atoms: commands with optional proof **)
(* scanning spans *)
@@ -174,7 +174,7 @@
val stopper = Scan.stopper (K eof) is_eof;
-(* unit_source *)
+(* atom_source *)
local
@@ -188,13 +188,13 @@
(if d = 0 then Scan.fail else command_with Keyword.is_qed >> pair (d - 1)) ||
Scan.unless (command_with Keyword.is_theory) (Scan.one not_eof) >> pair d)) -- Scan.state);
-val unit =
+val atom =
command_with Keyword.is_theory_goal -- proof >> (fn (a, (bs, d)) => (a, bs, d >= 0)) ||
Scan.one not_eof >> (fn a => (a, [], true));
in
-fun unit_source src = Source.source stopper (Scan.bulk unit) NONE src;
+fun atom_source src = Source.source stopper (Scan.bulk atom) NONE src;
end;