# HG changeset patch # User haftmann # Date 1501827157 -7200 # Node ID 30c1639a343ae185df220d43cd5f24ff25fa85e0 # Parent 489667636064afcc48021cf45cb15b775c188c48 prefer explicit datatype over implicit sum; given up separate implementation to pretty-print locale specifications diff -r 489667636064 -r 30c1639a343a src/Pure/Isar/locale.ML --- 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; diff -r 489667636064 -r 30c1639a343a src/Pure/Isar/named_target.ML --- 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;