# HG changeset patch # User wenzelm # Date 1345465400 -7200 # Node ID 9824fd676bf40100e520247bf1c25dddfd406af7 # Parent 3ee314ae1e0abb9bd7a65d3448371ad57e78c385 tuned; diff -r 3ee314ae1e0a -r 9824fd676bf4 src/Pure/Thy/thy_syntax.ML --- a/src/Pure/Thy/thy_syntax.ML Mon Aug 20 14:09:09 2012 +0200 +++ b/src/Pure/Thy/thy_syntax.ML Mon Aug 20 14:23:20 2012 +0200 @@ -13,8 +13,8 @@ type span val span_kind: span -> span_kind val span_content: span -> Token.T list + val present_span: span -> Output.output val parse_spans: Token.T list -> span list - val present_span: span -> Output.output type element = {head: span, proof: span list, proper_proof: bool} val parse_elements: span list -> element list end; @@ -106,6 +106,8 @@ fun span_kind (Span (k, _)) = k; fun span_content (Span (_, toks)) = toks; +val present_span = implode o map present_token o span_content; + (* parse *) @@ -129,11 +131,6 @@ end; -(* present *) - -val present_span = implode o map present_token o span_content; - - (** specification elements: commands with optional proof **)