1.1 --- a/src/Pure/Isar/outer_syntax.ML	Fri Jul 01 16:05:38 2011 +0200
     1.2 +++ b/src/Pure/Isar/outer_syntax.ML	Fri Jul 01 17:36:25 2011 +0200
     1.3 @@ -249,13 +249,13 @@
     1.4      handle ERROR msg => (Toplevel.malformed range_pos msg, true)
     1.5    end;
     1.6  
     1.7 -fun prepare_atom commands init (cmd, proof, proper_proof) =
     1.8 +fun prepare_element commands init {head, proof, proper_proof} =
     1.9    let
    1.10 -    val (tr, proper_cmd) = prepare_span commands cmd |>> Toplevel.modify_init init;
    1.11 +    val (tr, proper_head) = prepare_span commands head |>> Toplevel.modify_init init;
    1.12      val proof_trs = map (prepare_span commands) proof |> filter #2 |> map #1;
    1.13    in
    1.14 -    if proper_cmd andalso proper_proof then [(tr, proof_trs)]
    1.15 -    else map (rpair []) (if proper_cmd then tr :: proof_trs else proof_trs)
    1.16 +    if proper_head andalso proper_proof then [(tr, proof_trs)]
    1.17 +    else map (rpair []) (if proper_head then tr :: proof_trs else proof_trs)
    1.18    end;
    1.19  
    1.20  fun prepare_command pos str =
    1.21 @@ -278,14 +278,14 @@
    1.22      val toks = Source.exhausted (Thy_Syntax.token_source lexs pos (Source.of_string text));
    1.23      val spans = Source.exhaust (Thy_Syntax.span_source toks);
    1.24      val _ = List.app Thy_Syntax.report_span spans;  (* FIXME ?? *)
    1.25 -    val atoms = Source.exhaust (Thy_Syntax.atom_source (Source.of_list spans))
    1.26 -      |> Par_List.map_name "Outer_Syntax.prepare_atom" (prepare_atom commands init) |> flat;
    1.27 +    val elements = Source.exhaust (Thy_Syntax.element_source (Source.of_list spans))
    1.28 +      |> Par_List.map_name "Outer_Syntax.prepare_element" (prepare_element commands init) |> flat;
    1.29  
    1.30      val _ = Present.theory_source name
    1.31        (fn () => HTML.html_mode (implode o map Thy_Syntax.present_span) spans);
    1.32  
    1.33      val _ = if time then writeln ("\n**** Starting theory " ^ quote name ^ " ****") else ();
    1.34 -    val (results, thy) = cond_timeit time "" (fn () => Toplevel.excursion atoms);
    1.35 +    val (results, thy) = cond_timeit time "" (fn () => Toplevel.excursion elements);
    1.36      val _ = if time then writeln ("**** Finished theory " ^ quote name ^ " ****\n") else ();
    1.37  
    1.38      val present =

     2.1 --- a/src/Pure/Thy/thy_syntax.ML	Fri Jul 01 16:05:38 2011 +0200
     2.2 +++ b/src/Pure/Thy/thy_syntax.ML	Fri Jul 01 17:36:25 2011 +0200
     2.3 @@ -21,8 +21,9 @@
     2.4    val parse_spans: Scan.lexicon * Scan.lexicon -> Position.T -> string -> span list
     2.5    val present_span: span -> Output.output
     2.6    val report_span: span -> unit
     2.7 -  val atom_source: (span, 'a) Source.source ->
     2.8 -    (span * span list * bool, (span, 'a) Source.source) Source.source
     2.9 +  type element = {head: span, proof: span list, proper_proof: bool}
    2.10 +  val element_source: (span, 'a) Source.source ->
    2.11 +    (element, (span, 'a) Source.source) Source.source
    2.12  end;
    2.13  
    2.14  structure Thy_Syntax: THY_SYNTAX =
    2.15 @@ -159,7 +160,13 @@
    2.16  
    2.17  
    2.18  
    2.19 -(** specification atoms: commands with optional proof **)
    2.20 +(** specification elements: commands with optional proof **)
    2.21 +
    2.22 +type element = {head: span, proof: span list, proper_proof: bool};
    2.23 +
    2.24 +fun make_element head proof proper_proof =
    2.25 +  {head = head, proof = proof, proper_proof = proper_proof};
    2.26 +
    2.27  
    2.28  (* scanning spans *)
    2.29  
    2.30 @@ -173,7 +180,7 @@
    2.31  val stopper = Scan.stopper (K eof) is_eof;
    2.32  
    2.33  
    2.34 -(* atom_source *)
    2.35 +(* element_source *)
    2.36  
    2.37  local
    2.38  
    2.39 @@ -187,13 +194,14 @@
    2.40      (if d = 0 then Scan.fail else command_with Keyword.is_qed >> pair (d - 1)) ||
    2.41      Scan.unless (command_with Keyword.is_theory) (Scan.one not_eof) >> pair d)) -- Scan.state);
    2.42  
    2.43 -val atom =
    2.44 -  command_with Keyword.is_theory_goal -- proof >> (fn (a, (bs, d)) => (a, bs, d >= 0)) ||
    2.45 -  Scan.one not_eof >> (fn a => (a, [], true));
    2.46 +val element =
    2.47 +  command_with Keyword.is_theory_goal -- proof
    2.48 +    >> (fn (a, (bs, d)) => make_element a bs (d >= 0)) ||
    2.49 +  Scan.one not_eof >> (fn a => make_element a [] true);
    2.50  
    2.51  in
    2.52  
    2.53 -fun atom_source src = Source.source stopper (Scan.bulk atom) NONE src;
    2.54 +fun element_source src = Source.source stopper (Scan.bulk element) NONE src;
    2.55  
    2.56  end;
    2.57