# HG changeset patch
# User wenzelm
# Date 1535535868 -7200
# Node ID d8251a61cce8f3934173d2e7e074d732ef8f43c8
# Parent  5e013478bced3c56e308806bf8ac8e5996025394
clarified modules;

diff -r 5e013478bced -r d8251a61cce8 src/Pure/Isar/toplevel.ML
--- 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
diff -r 5e013478bced -r d8251a61cce8 src/Pure/ROOT.ML
--- 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";
diff -r 5e013478bced -r d8251a61cce8 src/Pure/Thy/thy_element.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;
diff -r 5e013478bced -r d8251a61cce8 src/Pure/Thy/thy_info.ML
--- 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
diff -r 5e013478bced -r d8251a61cce8 src/Pure/Thy/thy_syntax.ML
--- 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;