prefer explicit datatype over implicit sum;
given up separate implementation to pretty-print locale specifications

--- a/src/Pure/Isar/locale.ML	Fri Aug 04 08:12:37 2017 +0200
+++ b/src/Pure/Isar/locale.ML	Fri Aug 04 08:12:37 2017 +0200
@@ -88,6 +88,7 @@
   val print_locale: theory -> bool -> xstring * Position.T -> unit
   val print_registrations: Proof.context -> xstring * Position.T -> unit
   val print_dependencies: Proof.context -> bool -> morphism -> (string * morphism) list -> unit
+  val pretty_locale: theory -> bool -> string -> Pretty.T list
   val pretty_locale_deps: theory -> {name: string, parents: string list, body: Pretty.T} list
 end;
 
@@ -699,13 +700,12 @@
       activate_all name thy cons_elem (K (Morphism.transfer_morphism thy)) (empty_idents, [])
       |> snd |> rev;
   in
-    Pretty.block
-      (Pretty.keyword1 "locale" :: Pretty.brk 1 :: pretty_name locale_ctxt name ::
-        maps (fn elem => [Pretty.fbrk, Pretty.chunks (Element.pretty_ctxt locale_ctxt elem)]) elems)
+    Pretty.keyword1 "locale" :: Pretty.brk 1 :: pretty_name locale_ctxt name ::
+      maps (fn elem => [Pretty.fbrk, Pretty.chunks (Element.pretty_ctxt locale_ctxt elem)]) elems
   end;
 
 fun print_locale thy show_facts raw_name =
-  Pretty.writeln (pretty_locale thy show_facts (check thy raw_name));
+  Pretty.writeln (Pretty.block (pretty_locale thy show_facts (check thy raw_name)));
 
 fun print_registrations ctxt raw_name =
   let
@@ -732,7 +732,7 @@
     fun make_node name =
      {name = name,
       parents = map (fst o fst) (dependencies_of thy name),
-      body = pretty_locale thy false name};
+      body = Pretty.block (pretty_locale thy false name)};
     val names = sort_strings (Name_Space.fold_table (cons o #1) (Locales.get thy) []);
   in map make_node names end;
 

--- a/src/Pure/Isar/named_target.ML	Fri Aug 04 08:12:37 2017 +0200
+++ b/src/Pure/Isar/named_target.ML	Fri Aug 04 08:12:37 2017 +0200
@@ -25,41 +25,47 @@
 
 (* context data *)
 
+datatype target = Theory | Locale of string | Class of string;
+
+fun ident_of_target Theory = ""
+  | ident_of_target (Locale locale) = locale
+  | ident_of_target (Class class) = class;
+
+fun target_is_theory (SOME Theory) = true
+  | target_is_theory _ = false;
+
+fun locale_of_target (SOME (Locale locale)) = SOME locale
+  | locale_of_target (SOME (Class locale)) = SOME locale
+  | locale_of_target _ = NONE;
+
+fun class_of_target (SOME (Class class)) = SOME class
+  | class_of_target _ = NONE;
+
 structure Data = Proof_Data
 (
-  type T = (string * bool) option;
+  type T = target option;
   fun init _ = NONE;
 );
 
-val get_bottom_data = Data.get;
+val get_bottom_target = Data.get;
 
-fun get_data lthy =
+fun get_target lthy =
   if Local_Theory.level lthy = 1
-  then get_bottom_data lthy
+  then get_bottom_target lthy
   else NONE;
 
-fun is_theory lthy =
-  (case get_data lthy of
-    SOME ("", _) => true
-  | _ => false);
-
-fun target_of lthy =
-  (case get_data lthy of
+fun ident_of lthy =
+  case get_target lthy of
     NONE => error "Not in a named target"
-  | SOME (target, _) => target);
+  | SOME target => ident_of_target target;
 
-fun locale_name_of NONE = NONE
-  | locale_name_of (SOME ("", _)) = NONE
-  | locale_name_of (SOME (locale, _)) = SOME locale;
+val is_theory = target_is_theory o get_target;
 
-val locale_of = locale_name_of o get_data;
+val locale_of = locale_of_target o get_target;
 
-val bottom_locale_of = locale_name_of o get_bottom_data;
+val bottom_locale_of = locale_of_target o get_bottom_target;
 
-fun class_of lthy =
-  (case get_data lthy of
-    SOME (class, true) => SOME class
-  | _ => NONE);
+val class_of = class_of_target o get_target;
 
 
 (* operations *)
@@ -74,87 +80,73 @@
   #-> (fn (lhs, def) => Class.const class ((b, mx), lhs) params
     #> pair (lhs, def));
 
-fun foundation ("", _) = Generic_Target.theory_target_foundation
-  | foundation (locale, false) = locale_foundation locale
-  | foundation (class, true) = class_foundation class;
+fun foundation Theory = Generic_Target.theory_target_foundation
+  | foundation (Locale locale) = locale_foundation locale
+  | foundation (Class class) = class_foundation class;
 
-fun notes ("", _) = Generic_Target.theory_target_notes
-  | notes (locale, _) = Generic_Target.locale_target_notes locale;
+fun notes Theory = Generic_Target.theory_target_notes
+  | notes (Locale locale) = Generic_Target.locale_target_notes locale
+  | notes (Class class) = Generic_Target.locale_target_notes class;
 
-fun abbrev ("", _) = Generic_Target.theory_abbrev
-  | abbrev (locale, false) = Generic_Target.locale_abbrev locale
-  | abbrev (class, true) = Class.abbrev class;
+fun abbrev Theory = Generic_Target.theory_abbrev
+  | abbrev (Locale locale) = Generic_Target.locale_abbrev locale
+  | abbrev (Class class) = Class.abbrev class;
 
-fun declaration ("", _) _ decl = Generic_Target.theory_declaration decl
-  | declaration (locale, _) flags decl = Generic_Target.locale_declaration locale flags decl;
+fun declaration Theory _ decl = Generic_Target.theory_declaration decl
+  | declaration (Locale locale) flags decl = Generic_Target.locale_declaration locale flags decl
+  | declaration (Class class) flags decl = Generic_Target.locale_declaration class flags decl;
 
-fun theory_registration ("", _) = Generic_Target.theory_registration
+fun theory_registration Theory = Generic_Target.theory_registration
   | theory_registration _ = (fn _ => error "Not possible in theory target");
 
-fun locale_dependency ("", false) = (fn _ => error "Not possible in locale target")
-  | locale_dependency ("", true) = (fn _ => error "Not possible in class target")
-  | locale_dependency (locale, _) = Generic_Target.locale_dependency locale;
+fun locale_dependency Theory = (fn _ => error "Not possible in theory target")
+  | locale_dependency (Locale locale) = Generic_Target.locale_dependency locale
+  | locale_dependency (Class class) = Generic_Target.locale_dependency class;
 
-fun pretty (target, is_class) ctxt =
-  if target = "" then
-    [Pretty.block [Pretty.keyword1 "theory", Pretty.brk 1,
-      Pretty.str (Context.theory_name (Proof_Context.theory_of ctxt))]]
-  else if is_class then Class.pretty_specification (Proof_Context.theory_of ctxt) target
-  else
-    (* FIXME pretty locale content *)
-    let
-      val target_name = [Pretty.keyword1 "locale", Pretty.brk 1, Locale.pretty_name ctxt target];
-      val fixes =
-        map (fn (x, T) => (Binding.name x, SOME T, NoSyn))
-          (#1 (Proof_Context.inferred_fixes ctxt));
-      val assumes =
-        map (fn A => (Binding.empty_atts, [(Thm.term_of A, [])]))
-          (Assumption.all_assms_of ctxt);
-      val elems =
-        (if null fixes then [] else [Element.Fixes fixes]) @
-        (if null assumes then [] else [Element.Assumes assumes]);
-    in
-      if null elems then [Pretty.block target_name]
-      else [Pretty.block (Pretty.fbreaks (Pretty.block (target_name @ [Pretty.str " ="]) ::
-        map (Pretty.chunks o Element.pretty_ctxt ctxt) elems))]
-    end;
+fun pretty Theory ctxt =
+      [Pretty.block [Pretty.keyword1 "theory", Pretty.brk 1,
+        Pretty.str (Context.theory_name (Proof_Context.theory_of ctxt))]]
+  | pretty (Locale locale) ctxt = Locale.pretty_locale (Proof_Context.theory_of ctxt) false locale
+  | pretty (Class class) ctxt =
+      Class.pretty_specification (Proof_Context.theory_of ctxt) class;
 
 
 (* init *)
 
-fun make_name_data _ "" = ("", false)
-  | make_name_data thy target =
-      if Locale.defined thy target
-      then (target, Class.is_class thy target)
-      else error ("No such locale: " ^ quote target);
+fun make_target _ "" = Theory
+  | make_target thy ident =
+      if Locale.defined thy ident
+      then (if Class.is_class thy ident then Class else Locale) ident
+      else error ("No such locale: " ^ quote ident);
 
-fun init_context ("", _) = Proof_Context.init_global
-  | init_context (locale, false) = Locale.init locale
-  | init_context (class, true) = Class.init class;
+fun init_context Theory = Proof_Context.init_global
+  | init_context (Locale locale) = Locale.init locale
+  | init_context (Class class) = Class.init class;
 
-fun init before_exit target thy =
+fun init before_exit ident thy =
   let
-    val name_data = make_name_data thy target;
+    val target = make_target thy ident;
     val background_naming =
-      Sign.naming_of thy |> Name_Space.mandatory_path (Long_Name.base_name target);
+      Sign.naming_of thy |> Name_Space.mandatory_path (Long_Name.base_name ident);
   in
     thy
     |> Sign.change_begin
-    |> init_context name_data
-    |> is_none before_exit ? Data.put (SOME name_data)
+    |> init_context target
+    |> is_none before_exit ? Data.put (SOME target)
     |> Local_Theory.init background_naming
-       {define = Generic_Target.define (foundation name_data),
-        notes = Generic_Target.notes (notes name_data),
-        abbrev = abbrev name_data,
-        declaration = declaration name_data,
-        theory_registration = theory_registration name_data,
-        locale_dependency = locale_dependency name_data,
-        pretty = pretty name_data,
+       {define = Generic_Target.define (foundation target),
+        notes = Generic_Target.notes (notes target),
+        abbrev = abbrev target,
+        declaration = declaration target,
+        theory_registration = theory_registration target,
+        locale_dependency = locale_dependency target,
+        pretty = pretty target,
         exit = the_default I before_exit
           #> Local_Theory.target_of #> Sign.change_end_local}
   end;
 
 val theory_init = init NONE "";
+
 fun theory_map f = theory_init #> f #> Local_Theory.exit_global;
 
 
@@ -172,7 +164,7 @@
   | switch NONE (Context.Proof lthy) =
       (Context.Proof o Local_Theory.reset, lthy)
   | switch (SOME name) (Context.Proof lthy) =
-      (Context.Proof o init NONE (target_of lthy) o exit,
+      (Context.Proof o init NONE (ident_of lthy) o exit,
         (begin name o exit o Local_Theory.assert_nonbrittle) lthy);
 
 end;