src/Pure/Thy/thy_syntax.ML
author wenzelm
Thu Nov 02 10:16:22 2017 +0100 (19 months ago)
changeset 66987 352b23c97ac8
parent 61379 c57820ceead3
permissions -rw-r--r--
support focus_session, for much faster startup of Isabelle/jEdit;
more options for "isabelle jedit";
     1 (*  Title:      Pure/Thy/thy_syntax.ML
     2     Author:     Makarius
     3 
     4 Theory syntax elements.
     5 *)
     6 
     7 signature THY_SYNTAX =
     8 sig
     9   datatype 'a element = Element of 'a * ('a element list * 'a) option
    10   val atom: 'a -> 'a element
    11   val map_element: ('a -> 'b) -> 'a element -> 'b element
    12   val flat_element: 'a element -> 'a list
    13   val last_element: 'a element -> 'a
    14   val parse_elements: Keyword.keywords -> Command_Span.span list -> Command_Span.span element list
    15 end;
    16 
    17 structure Thy_Syntax: THY_SYNTAX =
    18 struct
    19 
    20 (* datatype element: command with optional proof *)
    21 
    22 datatype 'a element = Element of 'a * ('a element list * 'a) option;
    23 
    24 fun element (a, b) = Element (a, SOME b);
    25 fun atom a = Element (a, NONE);
    26 
    27 fun map_element f (Element (a, NONE)) = Element (f a, NONE)
    28   | map_element f (Element (a, SOME (elems, b))) =
    29       Element (f a, SOME ((map o map_element) f elems, f b));
    30 
    31 fun flat_element (Element (a, NONE)) = [a]
    32   | flat_element (Element (a, SOME (elems, b))) = a :: maps flat_element elems @ [b];
    33 
    34 fun last_element (Element (a, NONE)) = a
    35   | last_element (Element (_, SOME (_, b))) = b;
    36 
    37 
    38 (* scanning spans *)
    39 
    40 val eof = Command_Span.Span (Command_Span.Command_Span ("", Position.none), []);
    41 
    42 fun is_eof (Command_Span.Span (Command_Span.Command_Span ("", _), _)) = true
    43   | is_eof _ = false;
    44 
    45 val not_eof = not o is_eof;
    46 
    47 val stopper = Scan.stopper (K eof) is_eof;
    48 
    49 
    50 (* parse *)
    51 
    52 local
    53 
    54 fun command_with pred =
    55   Scan.one
    56     (fn (Command_Span.Span (Command_Span.Command_Span (name, _), _)) => pred name | _ => false);
    57 
    58 fun parse_element keywords =
    59   let
    60     val proof_atom =
    61       Scan.one
    62         (fn (Command_Span.Span (Command_Span.Command_Span (name, _), _)) =>
    63               Keyword.is_proof_body keywords name
    64           | _ => true) >> atom;
    65     fun proof_element x =
    66       (command_with (Keyword.is_proof_goal keywords) -- proof_rest >> element || proof_atom) x
    67     and proof_rest x =
    68       (Scan.repeat proof_element -- command_with (Keyword.is_qed keywords)) x;
    69   in
    70     command_with (Keyword.is_theory_goal keywords) -- proof_rest >> element ||
    71     Scan.one not_eof >> atom
    72   end;
    73 
    74 in
    75 
    76 fun parse_elements keywords =
    77   Source.of_list #>
    78   Source.source stopper (Scan.bulk (parse_element keywords)) #>
    79   Source.exhaust;
    80 
    81 end;
    82 
    83 end;