tuned;
authorwenzelm
Wed Aug 29 12:58:23 2018 +0200 (13 months ago)
changeset 6884272c4452f4b94
parent 68841 252b43600737
child 68843 d99d03d7755e
tuned;
src/Pure/Thy/thy_element.ML
     1.1 --- a/src/Pure/Thy/thy_element.ML	Wed Aug 29 12:44:17 2018 +0200
     1.2 +++ b/src/Pure/Thy/thy_element.ML	Wed Aug 29 12:58:23 2018 +0200
     1.3 @@ -51,23 +51,20 @@
     1.4  
     1.5  local
     1.6  
     1.7 -fun command_with pred =
     1.8 -  Scan.one
     1.9 -    (fn (Command_Span.Span (Command_Span.Command_Span (name, _), _)) => pred name | _ => false);
    1.10 -
    1.11  fun parse_element keywords =
    1.12    let
    1.13 -    val proof_atom =
    1.14 +    fun category pred other =
    1.15        Scan.one
    1.16          (fn (Command_Span.Span (Command_Span.Command_Span (name, _), _)) =>
    1.17 -              Keyword.is_proof_body keywords name
    1.18 -          | _ => true) >> atom;
    1.19 +            pred keywords name
    1.20 +          | _ => other);
    1.21 +
    1.22      fun proof_element x =
    1.23 -      (command_with (Keyword.is_proof_goal keywords) -- proof_rest >> element || proof_atom) x
    1.24 -    and proof_rest x =
    1.25 -      (Scan.repeat proof_element -- command_with (Keyword.is_qed keywords)) x;
    1.26 +      (category Keyword.is_proof_goal false -- proof_rest >> element ||
    1.27 +        category Keyword.is_proof_body true >> atom) x
    1.28 +    and proof_rest x = (Scan.repeat proof_element -- category Keyword.is_qed false) x;
    1.29    in
    1.30 -    command_with (Keyword.is_theory_goal keywords) -- proof_rest >> element ||
    1.31 +    category Keyword.is_theory_goal false -- proof_rest >> element ||
    1.32      Scan.one not_eof >> atom
    1.33    end;
    1.34