src/Pure/Thy/thy_syntax.ML
author wenzelm
Mon Feb 23 14:50:30 2015 +0100 (2015-02-23)
changeset 59564 fdc03c8daacc
parent 59125 ee19c92ae8b4
child 59809 87641097d0f3
permissions -rw-r--r--
Goal.prove_multi is superseded by the fully general Goal.prove_common;
     1 (*  Title:      Pure/Thy/thy_syntax.ML
     2     Author:     Makarius
     3 
     4 Superficial theory syntax: tokens and spans.
     5 *)
     6 
     7 signature THY_SYNTAX =
     8 sig
     9   val reports_of_tokens: Keyword.keywords -> Token.T list -> bool * Position.report_text list
    10   val present_token: Keyword.keywords -> Token.T -> Output.output
    11   val present_span: Keyword.keywords -> Command_Span.span -> Output.output
    12   datatype 'a element = Element of 'a * ('a element list * 'a) option
    13   val atom: 'a -> 'a element
    14   val map_element: ('a -> 'b) -> 'a element -> 'b element
    15   val flat_element: 'a element -> 'a list
    16   val last_element: 'a element -> 'a
    17   val parse_elements: Keyword.keywords -> Command_Span.span list -> Command_Span.span element list
    18 end;
    19 
    20 structure Thy_Syntax: THY_SYNTAX =
    21 struct
    22 
    23 (** presentation **)
    24 
    25 local
    26 
    27 fun reports_of_token keywords tok =
    28   let
    29     val malformed_symbols =
    30       Input.source_explode (Token.source_position_of tok)
    31       |> map_filter (fn (sym, pos) =>
    32           if Symbol.is_malformed sym
    33           then SOME ((pos, Markup.bad), "Malformed symbolic character") else NONE);
    34     val is_malformed = Token.is_error tok orelse not (null malformed_symbols);
    35     val reports = Token.reports keywords tok @ Token.completion_report tok @ malformed_symbols;
    36   in (is_malformed, reports) end;
    37 
    38 in
    39 
    40 fun reports_of_tokens keywords toks =
    41   let val results = map (reports_of_token keywords) toks
    42   in (exists fst results, maps snd results) end;
    43 
    44 end;
    45 
    46 fun present_token keywords tok =
    47   fold_rev Markup.enclose (Token.markups keywords tok) (Output.output (Token.unparse tok));
    48 
    49 fun present_span keywords = implode o map (present_token keywords) o Command_Span.content;
    50 
    51 
    52 
    53 (** specification elements: commands with optional proof **)
    54 
    55 datatype 'a element = Element of 'a * ('a element list * 'a) option;
    56 
    57 fun element (a, b) = Element (a, SOME b);
    58 fun atom a = Element (a, NONE);
    59 
    60 fun map_element f (Element (a, NONE)) = Element (f a, NONE)
    61   | map_element f (Element (a, SOME (elems, b))) =
    62       Element (f a, SOME ((map o map_element) f elems, f b));
    63 
    64 fun flat_element (Element (a, NONE)) = [a]
    65   | flat_element (Element (a, SOME (elems, b))) = a :: maps flat_element elems @ [b];
    66 
    67 fun last_element (Element (a, NONE)) = a
    68   | last_element (Element (_, SOME (_, b))) = b;
    69 
    70 
    71 (* scanning spans *)
    72 
    73 val eof = Command_Span.Span (Command_Span.Command_Span ("", Position.none), []);
    74 
    75 fun is_eof (Command_Span.Span (Command_Span.Command_Span ("", _), _)) = true
    76   | is_eof _ = false;
    77 
    78 val not_eof = not o is_eof;
    79 
    80 val stopper = Scan.stopper (K eof) is_eof;
    81 
    82 
    83 (* parse *)
    84 
    85 local
    86 
    87 fun command_with pred =
    88   Scan.one
    89     (fn (Command_Span.Span (Command_Span.Command_Span (name, _), _)) => pred name | _ => false);
    90 
    91 fun parse_element keywords =
    92   let
    93     val proof_atom =
    94       Scan.one
    95         (fn (Command_Span.Span (Command_Span.Command_Span (name, _), _)) =>
    96               Keyword.is_proof_body keywords name
    97           | _ => true) >> atom;
    98     fun proof_element x =
    99       (command_with (Keyword.is_proof_goal keywords) -- proof_rest >> element || proof_atom) x
   100     and proof_rest x =
   101       (Scan.repeat proof_element -- command_with (Keyword.is_qed keywords)) x;
   102   in
   103     command_with (Keyword.is_theory_goal keywords) -- proof_rest >> element ||
   104     Scan.one not_eof >> atom
   105   end;
   106 
   107 in
   108 
   109 fun parse_elements keywords =
   110   Source.of_list #>
   111   Source.source stopper (Scan.bulk (parse_element keywords)) #>
   112   Source.exhaust;
   113 
   114 end;
   115 
   116 end;