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/Isar/local_theory.ML
changeset 81594 7e1b66416b7f
parent 81591 d570d215e380 
--- a/src/Pure/Isar/local_theory.ML	Sat Dec 14 22:26:27 2024 +0100
+++ b/src/Pure/Isar/local_theory.ML	Sat Dec 14 23:48:45 2024 +0100
@@ -67,6 +67,7 @@
     local_theory -> local_theory
   val syntax_cmd: bool -> Syntax.mode -> (string * string * mixfix) list ->
     local_theory -> local_theory
+  val syntax_deps: (string * string list) list -> Proof.context -> local_theory
   val translations: bool -> Ast.ast Syntax.trrule list -> local_theory -> local_theory
   val translations_cmd: bool -> (string * string) Syntax.trrule list -> local_theory -> local_theory
   val type_notation: bool -> Syntax.mode -> (typ * mixfix) list -> local_theory -> local_theory
@@ -335,6 +336,10 @@
 val syntax = gen_syntax (K I);
 val syntax_cmd = gen_syntax Proof_Context.read_typ_syntax;
 
+fun syntax_deps args =
+  declaration {syntax = true, pervasive = false, pos = Position.thread_data ()}
+    (fn _ => Proof_Context.generic_syntax_deps args);
+
 
 (* translations *)
isabelle