1.1 --- a/src/Pure/Isar/outer_syntax.ML	Tue Sep 30 22:02:55 2008 +0200
     1.2 +++ b/src/Pure/Isar/outer_syntax.ML	Tue Sep 30 23:31:36 2008 +0200
     1.3 @@ -245,10 +245,14 @@
     1.4      handle ERROR msg => (Toplevel.malformed range_pos msg, true)
     1.5    end;
     1.6  
     1.7 -fun prepare_unit parser (cmd, proof) =
     1.8 -  (case prepare_span parser cmd of
     1.9 -    (_, false) => NONE
    1.10 -  | (tr, true) => SOME (tr, map (prepare_span parser) proof |> filter #2 |> map #1));
    1.11 +fun prepare_unit parser (cmd, proof, proper_proof) =
    1.12 +  let
    1.13 +    val (tr, proper_cmd) = prepare_span parser cmd;
    1.14 +    val proof_trs = map (prepare_span parser) proof |> filter #2 |> map #1;
    1.15 +  in
    1.16 +    if proper_cmd andalso proper_proof then [(tr, proof_trs)]
    1.17 +    else map (rpair []) (if proper_cmd then tr :: proof_trs else proof_trs)
    1.18 +  end;
    1.19  
    1.20  fun prepare_command pos str =
    1.21    let val (lexs, parser) = get_syntax () in
    1.22 @@ -270,7 +274,7 @@
    1.23      val spans = Source.exhaust (ThyEdit.span_source toks);
    1.24      val _ = List.app ThyEdit.report_span spans;
    1.25      val units = Source.exhaust (ThyEdit.unit_source (Source.of_list spans))
    1.26 -      |> map_filter (prepare_unit parser);
    1.27 +      |> maps (prepare_unit parser);
    1.28  
    1.29      val _ = Present.theory_source name
    1.30        (fn () => HTML.html_mode (implode o map ThyEdit.present_span) spans);