# HG changeset patch
# User wenzelm
# Date 1535723841 -7200
# Node ID a0769c7f51b4e3206c5a5b19b967287c3a7d9634
# Parent  f443ec10447da75b617294f84223cc6d3023ccfd# Parent  47e9912c53c3b6e3099926ae813e6e2794ac1a82
merged

diff -r f443ec10447d -r a0769c7f51b4 src/Pure/Isar/expression.ML
--- a/src/Pure/Isar/expression.ML	Thu Aug 30 17:20:54 2018 +0200
+++ b/src/Pure/Isar/expression.ML	Fri Aug 31 15:57:21 2018 +0200
@@ -531,12 +531,8 @@
 local
 
 fun props_of thy (name, morph) =
-  let
-    val (asm, defs) = Locale.specification_of thy name;
-  in
-    (case asm of NONE => defs | SOME asm => asm :: defs)
-    |> map (Morphism.term morph)
-  end;
+  let val (asm, defs) = Locale.specification_of thy name
+  in map (Morphism.term morph) (the_list asm @ defs) end;
 
 fun prep_goal_expression prep expression ctxt =
   let
diff -r f443ec10447d -r a0769c7f51b4 src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Thu Aug 30 17:20:54 2018 +0200
+++ b/src/Pure/Isar/locale.ML	Fri Aug 31 15:57:21 2018 +0200
@@ -42,6 +42,7 @@
     declaration list ->
     (string * Attrib.fact list) list ->
     (string * morphism) list -> theory -> theory
+  val locale_space: theory -> Name_Space.T
   val intern: theory -> xstring -> string
   val check: theory -> xstring * Position.T -> string
   val extern: theory -> string -> xstring
@@ -53,6 +54,14 @@
   val axioms_of: theory -> string -> thm list
   val instance_of: theory -> string -> morphism -> term list
   val specification_of: theory -> string -> term option * term list
+  val hyp_spec_of: theory -> string -> Element.context_i list
+
+  type content =
+   {type_params: (string * sort) list,
+    params: ((string * typ) * mixfix) list,
+    asm: term option,
+    defs: term list}
+  val dest_locales: theory -> (string * content) list
 
   (* Storing results *)
   val add_facts: string -> string -> Attrib.fact list -> Proof.context -> Proof.context
@@ -84,7 +93,6 @@
   val add_dependency: string -> registration -> theory -> theory
 
   (* Diagnostic *)
-  val hyp_spec_of: theory -> string -> Element.context_i list
   val print_locales: bool -> theory -> unit
   val print_locale: theory -> bool -> xstring * Position.T -> unit
   val print_registrations: Proof.context -> xstring * Position.T -> unit
@@ -207,6 +215,20 @@
   Locales.map o Name_Space.map_table_entry name o map_locale o apsnd;
 
 
+(* content *)
+
+type content =
+ {type_params: (string * sort) list,
+  params: ((string * typ) * mixfix) list,
+  asm: term option,
+  defs: term list};
+
+fun dest_locales thy =
+  (Locales.get thy, []) |-> Name_Space.fold_table
+    (fn (name, Loc {parameters = (type_params, params), spec = (asm, defs), ...}) =>
+      cons (name, {type_params = type_params, params = params, asm = asm, defs = defs}));
+
+
 (** Primitive operations **)
 
 fun params_of thy = snd o #parameters o the_locale thy;
@@ -220,8 +242,9 @@
 
 fun specification_of thy = #spec o the_locale thy;
 
-fun dependencies_of thy name = the_locale thy name |>
-  #dependencies;
+fun hyp_spec_of thy = #hyp_spec o the_locale thy;
+
+fun dependencies_of thy = #dependencies o the_locale thy;
 
 fun mixins_of thy name serial = the_locale thy name |>
   #mixins |> lookup_mixins serial;
@@ -693,8 +716,6 @@
 
 (*** diagnostic commands and interfaces ***)
 
-fun hyp_spec_of thy = #hyp_spec o the_locale thy;
-
 fun print_locales verbose thy =
   Pretty.block
     (Pretty.breaks
diff -r f443ec10447d -r a0769c7f51b4 src/Pure/Thy/export_theory.ML
--- a/src/Pure/Thy/export_theory.ML	Thu Aug 30 17:20:54 2018 +0200
+++ b/src/Pure/Thy/export_theory.ML	Fri Aug 31 15:57:21 2018 +0200
@@ -87,7 +87,6 @@
                     XML.Elem (entity_markup space name, body))))
           |> sort (int_ord o apply2 #1) |> map #2
         end;
-
       in if null elems then () else export_body thy export_name elems end;
 
 
@@ -196,6 +195,21 @@
     val _ = if null classrel then () else export_body thy "classrel" (encode_classrel classrel);
     val _ = if null arities then () else export_body thy "arities" (encode_arities arities);
 
+
+    (* locales *)
+
+    fun encode_locale {type_params, params, asm, defs} =
+      (type_params, (map #1 params, (asm, defs))) |>
+        let open XML.Encode Term_XML.Encode in
+          pair (list (pair string sort))
+            (pair (list (pair string typ))
+              (pair (option term) (list term)))
+        end;
+
+    val _ =
+      export_entities "locales" (fn _ => SOME o encode_locale) Locale.locale_space
+        (Locale.dest_locales thy);
+
   in () end);
 
 end;
diff -r f443ec10447d -r a0769c7f51b4 src/Pure/Thy/export_theory.scala
--- a/src/Pure/Thy/export_theory.scala	Thu Aug 30 17:20:54 2018 +0200
+++ b/src/Pure/Thy/export_theory.scala	Fri Aug 31 15:57:21 2018 +0200
@@ -30,9 +30,10 @@
     axioms: Boolean = true,
     facts: Boolean = true,
     classes: Boolean = true,
-    typedefs: Boolean = true,
+    locales: Boolean = true,
     classrel: Boolean = true,
     arities: Boolean = true,
+    typedefs: Boolean = true,
     cache: Term.Cache = Term.make_cache()): Session =
   {
     val thys =
@@ -42,7 +43,8 @@
           Export.read_theory_names(db, session_name).map((theory_name: String) =>
             read_theory(Export.Provider.database(db, session_name, theory_name),
               session_name, theory_name, types = types, consts = consts,
-              axioms = axioms, facts = facts, classes = classes, typedefs = typedefs,
+              axioms = axioms, facts = facts, classes = classes, locales = locales,
+              classrel = classrel, arities = arities, typedefs = typedefs,
               cache = Some(cache)))
         }
       })
@@ -69,9 +71,10 @@
     axioms: List[Fact_Single],
     facts: List[Fact_Multi],
     classes: List[Class],
-    typedefs: List[Typedef],
+    locales: List[Locale],
     classrel: List[Classrel],
-    arities: List[Arity])
+    arities: List[Arity],
+    typedefs: List[Typedef])
   {
     override def toString: String = name
 
@@ -81,7 +84,8 @@
         consts.iterator.map(_.entity.serial) ++
         axioms.iterator.map(_.entity.serial) ++
         facts.iterator.map(_.entity.serial) ++
-        classes.iterator.map(_.entity.serial)
+        classes.iterator.map(_.entity.serial) ++
+        locales.iterator.map(_.entity.serial)
 
     def cache(cache: Term.Cache): Theory =
       Theory(cache.string(name),
@@ -91,13 +95,14 @@
         axioms.map(_.cache(cache)),
         facts.map(_.cache(cache)),
         classes.map(_.cache(cache)),
-        typedefs.map(_.cache(cache)),
+        locales.map(_.cache(cache)),
         classrel.map(_.cache(cache)),
-        arities.map(_.cache(cache)))
+        arities.map(_.cache(cache)),
+        typedefs.map(_.cache(cache)))
   }
 
   def empty_theory(name: String): Theory =
-    Theory(name, Nil, Nil, Nil, Nil, Nil, Nil, Nil, Nil, Nil)
+    Theory(name, Nil, Nil, Nil, Nil, Nil, Nil, Nil, Nil, Nil, Nil)
 
   def read_theory(provider: Export.Provider, session_name: String, theory_name: String,
     types: Boolean = true,
@@ -105,9 +110,10 @@
     axioms: Boolean = true,
     facts: Boolean = true,
     classes: Boolean = true,
-    typedefs: Boolean = true,
+    locales: Boolean = true,
     classrel: Boolean = true,
     arities: Boolean = true,
+    typedefs: Boolean = true,
     cache: Option[Term.Cache] = None): Theory =
   {
     val parents =
@@ -124,9 +130,10 @@
         if (axioms) read_axioms(provider) else Nil,
         if (facts) read_facts(provider) else Nil,
         if (classes) read_classes(provider) else Nil,
-        if (typedefs) read_typedefs(provider) else Nil,
+        if (locales) read_locales(provider) else Nil,
         if (classrel) read_classrel(provider) else Nil,
-        if (arities) read_arities(provider) else Nil)
+        if (arities) read_arities(provider) else Nil,
+        if (typedefs) read_typedefs(provider) else Nil)
     if (cache.isDefined) theory.cache(cache.get) else theory
   }
 
@@ -154,6 +161,7 @@
     val AXIOM = Value("axiom")
     val FACT = Value("fact")
     val CLASS = Value("class")
+    val LOCALE = Value("locale")
   }
 
   sealed case class Entity(
@@ -316,6 +324,36 @@
       })
 
 
+  /* locales */
+
+  sealed case class Locale(
+    entity: Entity, type_params: List[(String, Term.Sort)], params: List[(String, Term.Typ)],
+      asm: Option[Term.Term], defs: List[Term.Term])
+  {
+    def cache(cache: Term.Cache): Locale =
+      Locale(entity.cache(cache),
+        type_params.map({ case (name, sort) => (cache.string(name), cache.sort(sort)) }),
+        params.map({ case (name, typ) => (cache.string(name), cache.typ(typ)) }),
+        asm.map(cache.term(_)),
+        defs.map(cache.term(_)))
+  }
+
+  def read_locales(provider: Export.Provider): List[Locale] =
+    provider.uncompressed_yxml(export_prefix + "locales").map((tree: XML.Tree) =>
+      {
+        val (entity, body) = decode_entity(Kind.LOCALE, tree)
+        val (type_params, (params, (asm, defs))) =
+        {
+          import XML.Decode._
+          import Term_XML.Decode._
+          pair(list(pair(string, sort)),
+            pair(list(pair(string, typ)),
+              pair(option(term), list(term))))(body)
+        }
+        Locale(entity, type_params, params, asm, defs)
+      })
+
+
   /* sort algebra */
 
   sealed case class Classrel(class_name: String, super_names: List[String])