--- a/src/Pure/Isar/toplevel.ML Wed Aug 29 07:50:28 2018 +0100
+++ b/src/Pure/Isar/toplevel.ML Wed Aug 29 11:44:28 2018 +0200
@@ -86,7 +86,7 @@
val reset_proof: state -> state option
type result
val join_results: result -> (transition * state) list
- val element_result: Keyword.keywords -> transition Thy_Syntax.element -> state -> result * state
+ val element_result: Keyword.keywords -> transition Thy_Element.element -> state -> result * state
end;
structure Toplevel: TOPLEVEL =
@@ -669,7 +669,7 @@
val put_result = Proof.map_context o Result.put;
fun timing_estimate elem =
- let val trs = tl (Thy_Syntax.flat_element elem)
+ let val trs = tl (Thy_Element.flat_element elem)
in fold (fn tr => fn t => get_timing tr + t) trs Time.zeroTime end;
fun future_proofs_enabled estimate st =
@@ -693,8 +693,8 @@
in
-fun element_result keywords (Thy_Syntax.Element (tr, NONE)) st = atom_result keywords tr st
- | element_result keywords (elem as Thy_Syntax.Element (head_tr, SOME element_rest)) st =
+fun element_result keywords (Thy_Element.Element (tr, NONE)) st = atom_result keywords tr st
+ | element_result keywords (elem as Thy_Element.Element (head_tr, SOME element_rest)) st =
let
val (head_result, st') = atom_result keywords head_tr st;
val (body_elems, end_tr) = element_rest;
@@ -703,7 +703,7 @@
if not (future_proofs_enabled estimate st')
then
let
- val proof_trs = maps Thy_Syntax.flat_element body_elems @ [end_tr];
+ val proof_trs = maps Thy_Element.flat_element body_elems @ [end_tr];
val (proof_results, st'') = fold_map (atom_result keywords) proof_trs st';
in (Result_List (head_result :: proof_results), st'') end
else
--- a/src/Pure/ROOT.ML Wed Aug 29 07:50:28 2018 +0100
+++ b/src/Pure/ROOT.ML Wed Aug 29 11:44:28 2018 +0200
@@ -222,7 +222,7 @@
ML_file "Isar/local_theory.ML";
ML_file "Isar/entity.ML";
ML_file "PIDE/command_span.ML";
-ML_file "Thy/thy_syntax.ML";
+ML_file "Thy/thy_element.ML";
ML_file "Thy/markdown.ML";
ML_file "Thy/html.ML";
ML_file "Thy/latex.ML";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Thy/thy_element.ML Wed Aug 29 11:44:28 2018 +0200
@@ -0,0 +1,83 @@
+(* Title: Pure/Thy/thy_element.ML
+ Author: Makarius
+
+Theory elements: statements with optional proof.
+*)
+
+signature THY_ELEMENT =
+sig
+ datatype 'a element = Element of 'a * ('a element list * 'a) option
+ val atom: 'a -> 'a element
+ val map_element: ('a -> 'b) -> 'a element -> 'b element
+ val flat_element: 'a element -> 'a list
+ val last_element: 'a element -> 'a
+ val parse_elements: Keyword.keywords -> Command_Span.span list -> Command_Span.span element list
+end;
+
+structure Thy_Element: THY_ELEMENT =
+struct
+
+(* datatype element: command with optional proof *)
+
+datatype 'a element = Element of 'a * ('a element list * 'a) option;
+
+fun element (a, b) = Element (a, SOME b);
+fun atom a = Element (a, NONE);
+
+fun map_element f (Element (a, NONE)) = Element (f a, NONE)
+ | map_element f (Element (a, SOME (elems, b))) =
+ Element (f a, SOME ((map o map_element) f elems, f b));
+
+fun flat_element (Element (a, NONE)) = [a]
+ | flat_element (Element (a, SOME (elems, b))) = a :: maps flat_element elems @ [b];
+
+fun last_element (Element (a, NONE)) = a
+ | last_element (Element (_, SOME (_, b))) = b;
+
+
+(* scanning spans *)
+
+val eof = Command_Span.Span (Command_Span.Command_Span ("", Position.none), []);
+
+fun is_eof (Command_Span.Span (Command_Span.Command_Span ("", _), _)) = true
+ | is_eof _ = false;
+
+val not_eof = not o is_eof;
+
+val stopper = Scan.stopper (K eof) is_eof;
+
+
+(* parse *)
+
+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 =
+ Scan.one
+ (fn (Command_Span.Span (Command_Span.Command_Span (name, _), _)) =>
+ Keyword.is_proof_body keywords name
+ | _ => true) >> atom;
+ 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;
+ in
+ command_with (Keyword.is_theory_goal keywords) -- proof_rest >> element ||
+ Scan.one not_eof >> atom
+ end;
+
+in
+
+fun parse_elements keywords =
+ Source.of_list #>
+ Source.source stopper (Scan.bulk (parse_element keywords)) #>
+ Source.exhaust;
+
+end;
+
+end;
--- a/src/Pure/Thy/thy_info.ML Wed Aug 29 07:50:28 2018 +0100
+++ b/src/Pure/Thy/thy_info.ML Wed Aug 29 11:44:28 2018 +0200
@@ -289,9 +289,9 @@
fun element_result span_elem (st, _) =
let
- val elem = Thy_Syntax.map_element (prepare_span st) span_elem;
+ val elem = Thy_Element.map_element (prepare_span st) span_elem;
val (results, st') = Toplevel.element_result keywords elem st;
- val pos' = Toplevel.pos_of (Thy_Syntax.last_element elem);
+ val pos' = Toplevel.pos_of (Thy_Element.last_element elem);
in (results, (st', pos')) end;
val (results, (end_state, end_pos)) =
@@ -309,7 +309,7 @@
(Keyword.add_keywords (#keywords header) Keyword.empty_keywords);
val spans = Outer_Syntax.parse_spans (Token.explode keywords text_pos text);
- val elements = Thy_Syntax.parse_elements keywords spans;
+ val elements = Thy_Element.parse_elements keywords spans;
fun init () =
Resources.begin_theory master_dir header parents
--- a/src/Pure/Thy/thy_syntax.ML Wed Aug 29 07:50:28 2018 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,83 +0,0 @@
-(* Title: Pure/Thy/thy_syntax.ML
- Author: Makarius
-
-Theory syntax elements.
-*)
-
-signature THY_SYNTAX =
-sig
- datatype 'a element = Element of 'a * ('a element list * 'a) option
- val atom: 'a -> 'a element
- val map_element: ('a -> 'b) -> 'a element -> 'b element
- val flat_element: 'a element -> 'a list
- val last_element: 'a element -> 'a
- val parse_elements: Keyword.keywords -> Command_Span.span list -> Command_Span.span element list
-end;
-
-structure Thy_Syntax: THY_SYNTAX =
-struct
-
-(* datatype element: command with optional proof *)
-
-datatype 'a element = Element of 'a * ('a element list * 'a) option;
-
-fun element (a, b) = Element (a, SOME b);
-fun atom a = Element (a, NONE);
-
-fun map_element f (Element (a, NONE)) = Element (f a, NONE)
- | map_element f (Element (a, SOME (elems, b))) =
- Element (f a, SOME ((map o map_element) f elems, f b));
-
-fun flat_element (Element (a, NONE)) = [a]
- | flat_element (Element (a, SOME (elems, b))) = a :: maps flat_element elems @ [b];
-
-fun last_element (Element (a, NONE)) = a
- | last_element (Element (_, SOME (_, b))) = b;
-
-
-(* scanning spans *)
-
-val eof = Command_Span.Span (Command_Span.Command_Span ("", Position.none), []);
-
-fun is_eof (Command_Span.Span (Command_Span.Command_Span ("", _), _)) = true
- | is_eof _ = false;
-
-val not_eof = not o is_eof;
-
-val stopper = Scan.stopper (K eof) is_eof;
-
-
-(* parse *)
-
-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 =
- Scan.one
- (fn (Command_Span.Span (Command_Span.Command_Span (name, _), _)) =>
- Keyword.is_proof_body keywords name
- | _ => true) >> atom;
- 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;
- in
- command_with (Keyword.is_theory_goal keywords) -- proof_rest >> element ||
- Scan.one not_eof >> atom
- end;
-
-in
-
-fun parse_elements keywords =
- Source.of_list #>
- Source.source stopper (Scan.bulk (parse_element keywords)) #>
- Source.exhaust;
-
-end;
-
-end;