Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Syntax.default_mode;
authorwenzelm
Wed, 09 Jun 2004 18:53:13 +0200
changeset 14900 c66394c408f7
parent 14899 d9b6c81b52ac
child 14901 c7a8a8eb7fc8
Syntax.default_mode;
src/Pure/Isar/isar_syn.ML file | annotate | diff | comparison | revisions
src/Pure/goals.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/Isar/isar_syn.ML	Wed Jun 09 18:52:55 2004 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Wed Jun 09 18:53:13 2004 +0200
@@ -140,7 +140,8 @@
 val mode_spec =
   (P.$$$ "output" >> K ("", false)) || P.name -- Scan.optional (P.$$$ "output" >> K false) true;
 
-val opt_mode = Scan.optional (P.$$$ "(" |-- P.!!! (mode_spec --| P.$$$ ")")) ("", true);
+val opt_mode =
+  Scan.optional (P.$$$ "(" |-- P.!!! (mode_spec --| P.$$$ ")")) Syntax.default_mode;
 
 val syntaxP =
   OuterSyntax.command "syntax" "declare syntactic constants" K.thy_decl
--- a/src/Pure/goals.ML	Wed Jun 09 18:52:55 2004 +0200
+++ b/src/Pure/goals.ML	Wed Jun 09 18:53:13 2004 +0200
@@ -507,7 +507,7 @@
 
     val syntax_thy =
       thy
-      |> Theory.add_modesyntax_i ("", true) loc_syn
+      |> Theory.add_modesyntax_i Syntax.default_mode loc_syn
       |> Theory.add_trfuns ([], loc_trfuns, [], []);
 
     val syntax_sign = Theory.sign_of syntax_thy;
isabelle