1(* Title: Pure/Thy/thy_syntax.ML 2 Author: Makarius 3 4Theory syntax elements. 5*) 6 7signature THY_SYNTAX = 8sig 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 15end; 16 17structure Thy_Syntax: THY_SYNTAX = 18struct 19 20(* datatype element: command with optional proof *) 21 22datatype 'a element = Element of 'a * ('a element list * 'a) option; 23 24fun element (a, b) = Element (a, SOME b); 25fun atom a = Element (a, NONE); 26 27fun 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 31fun flat_element (Element (a, NONE)) = [a] 32 | flat_element (Element (a, SOME (elems, b))) = a :: maps flat_element elems @ [b]; 33 34fun last_element (Element (a, NONE)) = a 35 | last_element (Element (_, SOME (_, b))) = b; 36 37 38(* scanning spans *) 39 40val eof = Command_Span.Span (Command_Span.Command_Span ("", Position.none), []); 41 42fun is_eof (Command_Span.Span (Command_Span.Command_Span ("", _), _)) = true 43 | is_eof _ = false; 44 45val not_eof = not o is_eof; 46 47val stopper = Scan.stopper (K eof) is_eof; 48 49 50(* parse *) 51 52local 53 54fun command_with pred = 55 Scan.one 56 (fn (Command_Span.Span (Command_Span.Command_Span (name, _), _)) => pred name | _ => false); 57 58fun 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 74in 75 76fun parse_elements keywords = 77 Source.of_list #> 78 Source.source stopper (Scan.bulk (parse_element keywords)) #> 79 Source.exhaust; 80 81end; 82 83end; 84