Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Pure/Thy/thy_info.ML
changeset 68839 d8251a61cce8
parent 68506 cef6c6b009fb
child 69784 24bbc4e30e5b 
--- 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
isabelle