# HG changeset patch # User wenzelm # Date 1535540303 -7200 # Node ID 72c4452f4b9404d9e8e74075516c812b6f5c4014 # Parent 252b4360073778a72adc2d9e84fac746cc46cb10 tuned; diff -r 252b43600737 -r 72c4452f4b94 src/Pure/Thy/thy_element.ML --- a/src/Pure/Thy/thy_element.ML Wed Aug 29 12:44:17 2018 +0200 +++ b/src/Pure/Thy/thy_element.ML Wed Aug 29 12:58:23 2018 +0200 @@ -51,23 +51,20 @@ local -fun command_with pred = - Scan.one - (fn (Command_Span.Span (Command_Span.Command_Span (name, _), _)) => pred name | _ => false); - fun parse_element keywords = let - val proof_atom = + fun category pred other = Scan.one (fn (Command_Span.Span (Command_Span.Command_Span (name, _), _)) => - Keyword.is_proof_body keywords name - | _ => true) >> atom; + pred keywords name + | _ => other); + fun proof_element x = - (command_with (Keyword.is_proof_goal keywords) -- proof_rest >> element || proof_atom) x - and proof_rest x = - (Scan.repeat proof_element -- command_with (Keyword.is_qed keywords)) x; + (category Keyword.is_proof_goal false -- proof_rest >> element || + category Keyword.is_proof_body true >> atom) x + and proof_rest x = (Scan.repeat proof_element -- category Keyword.is_qed false) x; in - command_with (Keyword.is_theory_goal keywords) -- proof_rest >> element || + category Keyword.is_theory_goal false -- proof_rest >> element || Scan.one not_eof >> atom end;