# HG changeset patch
# User wenzelm
# Date 1627988903 -7200
# Node ID d0527bb2e59009e6b164c40df74a94f9bda4e32e
# Parent  4984fad0e91d556d2956eec48d20481cd30e9bf2
more uniform signatures in ML and Scala;

diff -r 4984fad0e91d -r d0527bb2e590 src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Tue Aug 03 12:39:29 2021 +0200
+++ b/src/Pure/Isar/attrib.ML	Tue Aug 03 13:08:23 2021 +0200
@@ -93,7 +93,7 @@
 structure Attributes = Generic_Data
 (
   type T = ((Token.src -> attribute) * string) Name_Space.table;
-  val empty : T = Name_Space.empty_table "attribute";
+  val empty : T = Name_Space.empty_table Markup.attributeN;
   val extend = I;
   fun merge data : T = Name_Space.merge_tables data;
 );
diff -r 4984fad0e91d -r d0527bb2e590 src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Tue Aug 03 12:39:29 2021 +0200
+++ b/src/Pure/Isar/locale.ML	Tue Aug 03 13:08:23 2021 +0200
@@ -177,7 +177,7 @@
 structure Locales = Theory_Data
 (
   type T = locale Name_Space.table;
-  val empty : T = Name_Space.empty_table "locale";
+  val empty : T = Name_Space.empty_table Markup.localeN;
   val extend = I;
   val merge = Name_Space.join_tables (K merge_locale);
 );
diff -r 4984fad0e91d -r d0527bb2e590 src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Tue Aug 03 12:39:29 2021 +0200
+++ b/src/Pure/Isar/method.ML	Tue Aug 03 13:08:23 2021 +0200
@@ -292,7 +292,7 @@
     ml_tactic: (morphism -> thm list -> tactic) option,
     facts: thm list option};
   val empty : T =
-    {methods = Name_Space.empty_table "method", ml_tactic = NONE, facts = NONE};
+    {methods = Name_Space.empty_table Markup.methodN, ml_tactic = NONE, facts = NONE};
   val extend = I;
   fun merge
     ({methods = methods1, ml_tactic = ml_tactic1, facts = facts1},
diff -r 4984fad0e91d -r d0527bb2e590 src/Pure/PIDE/markup.ML
--- a/src/Pure/PIDE/markup.ML	Tue Aug 03 12:39:29 2021 +0200
+++ b/src/Pure/PIDE/markup.ML	Tue Aug 03 13:08:23 2021 +0200
@@ -89,12 +89,18 @@
   val sessionN: string
   val theoryN: string
   val classN: string
+  val localeN: string
   val type_nameN: string
   val constantN: string
+  val axiomN: string
+  val factN: string
+  val oracleN: string
   val fixedN: string val fixed: string -> T
   val caseN: string val case_: string -> T
   val dynamic_factN: string val dynamic_fact: string -> T
   val literal_factN: string val literal_fact: string -> T
+  val attributeN: string
+  val methodN: string
   val method_modifierN: string
   val tfreeN: string val tfree: T
   val tvarN: string val tvar: T
@@ -461,14 +467,20 @@
 
 val theoryN = "theory";
 val classN = "class";
+val localeN = "locale";
 val type_nameN = "type_name";
 val constantN = "constant";
+val axiomN = "axiom";
+val factN = "fact";
+val oracleN = "oracle";
 
 val (fixedN, fixed) = markup_string "fixed" nameN;
 val (caseN, case_) = markup_string "case" nameN;
 val (dynamic_factN, dynamic_fact) = markup_string "dynamic_fact" nameN;
 val (literal_factN, literal_fact) = markup_string "literal_fact" nameN;
 
+val attributeN = "attribute";
+val methodN = "method";
 val method_modifierN = "method_modifier";
 
 
diff -r 4984fad0e91d -r d0527bb2e590 src/Pure/PIDE/markup.scala
--- a/src/Pure/PIDE/markup.scala	Tue Aug 03 12:39:29 2021 +0200
+++ b/src/Pure/PIDE/markup.scala	Tue Aug 03 13:08:23 2021 +0200
@@ -292,13 +292,25 @@
 
   /* misc entities */
 
+  val SESSION = "session"
+
   val THEORY = "theory"
   val CLASS = "class"
+  val LOCALE = "locale"
   val TYPE_NAME = "type_name"
+  val CONSTANT = "constant"
+  val AXIOM = "axiom"
+  val FACT = "fact"
+  val ORACLE = "oracle"
+
   val FIXED = "fixed"
   val CASE = "case"
-  val CONSTANT = "constant"
   val DYNAMIC_FACT = "dynamic_fact"
+  val LITERAL_FACT = "literal_fact"
+
+  val ATTRIBUTE = "attribute"
+  val METHOD = "method"
+  val METHOD_MODIFIER = "method_modifier"
 
 
   /* inner syntax */
@@ -321,9 +333,6 @@
   val TYPING = "typing"
   val CLASS_PARAMETER = "class_parameter"
 
-  val ATTRIBUTE = "attribute"
-  val METHOD = "method"
-
 
   /* antiquotations */
 
diff -r 4984fad0e91d -r d0527bb2e590 src/Pure/facts.ML
--- a/src/Pure/facts.ML	Tue Aug 03 12:39:29 2021 +0200
+++ b/src/Pure/facts.ML	Tue Aug 03 13:08:23 2021 +0200
@@ -146,7 +146,7 @@
 
 fun make_facts facts props = Facts {facts = facts, props = props};
 
-val empty = make_facts (Name_Space.empty_table "fact") Net.empty;
+val empty = make_facts (Name_Space.empty_table Markup.factN) Net.empty;
 
 
 (* named facts *)
diff -r 4984fad0e91d -r d0527bb2e590 src/Pure/theory.ML
--- a/src/Pure/theory.ML	Tue Aug 03 12:39:29 2021 +0200
+++ b/src/Pure/theory.ML	Tue Aug 03 13:08:23 2021 +0200
@@ -88,7 +88,7 @@
 (
   type T = thy;
   val extend = I;
-  val empty = make_thy (Position.none, 0, Name_Space.empty_table "axiom", Defs.empty, ([], []));
+  val empty = make_thy (Position.none, 0, Name_Space.empty_table Markup.axiomN, Defs.empty, ([], []));
   fun merge old_thys (thy1, thy2) =
     let
       val Thy {pos, id, axioms = axioms1, defs = defs1, wrappers = (bgs1, ens1)} = thy1;
diff -r 4984fad0e91d -r d0527bb2e590 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Tue Aug 03 12:39:29 2021 +0200
+++ b/src/Pure/thm.ML	Tue Aug 03 13:08:23 2021 +0200
@@ -897,7 +897,7 @@
     unit Name_Space.table *  (*oracles: authentic derivation names*)
     classes;  (*type classes within the logic*)
 
-  val empty : T = (Name_Space.empty_table "oracle", empty_classes);
+  val empty : T = (Name_Space.empty_table Markup.oracleN, empty_classes);
   val extend = I;
   fun merge ((oracles1, sorts1), (oracles2, sorts2)) : T =
     (Name_Space.merge_tables (oracles1, oracles2), merge_classes (sorts1, sorts2));