# HG changeset patch # User wenzelm # Date 1140035707 -3600 # Node ID 9201b2bb36c2374011c0cac980f9ac973a6a17ac # Parent 6ac9dfe98e543c08d3fccf9514215479fa0b3001 simplified presentation commands; diff -r 6ac9dfe98e54 -r 9201b2bb36c2 src/Pure/Isar/isar_cmd.ML --- a/src/Pure/Isar/isar_cmd.ML Wed Feb 15 21:35:06 2006 +0100 +++ b/src/Pure/Isar/isar_cmd.ML Wed Feb 15 21:35:07 2006 +0100 @@ -354,42 +354,30 @@ fun add_header s = Toplevel.keep' (fn int => fn state => (Toplevel.assert (Toplevel.is_toplevel state); - if int then OuterSyntax.check_text s state else ())); + if int then OuterSyntax.check_text s NONE else ())); local -fun enter_locale NONE = Toplevel.theory I - | enter_locale (SOME loc) = Toplevel.theory_context (fn thy => - (#2 (Locale.init (Locale.intern thy loc) thy), thy)); +fun present _ txt true node = OuterSyntax.check_text txt (SOME node) + | present f (s, _) false node = + Context.setmp (try (Toplevel.cases_node I Proof.theory_of) node) f s; -fun present_text proof present loc (s, pos) = Toplevel.keep' (fn int => fn state => - (Toplevel.assert (can Toplevel.proof_of state = proof); - if int then - state - |> Toplevel.copy - |> Toplevel.no_body_context - |> Toplevel.command - (Toplevel.empty |> Toplevel.position pos |> enter_locale loc |> Toplevel.keep (K ())) - |> OuterSyntax.check_text (s, pos) - else Context.setmp (SOME (Toplevel.theory_of state)) present s; - raise Toplevel.UNDEF)); - -fun theory f (loc, txt) = enter_locale loc o present_text false f loc txt; -fun proof f txt = Toplevel.print o Toplevel.proof I o present_text true f NONE txt; +fun present_local_theory f (loc, txt) = Toplevel.present_local_theory loc (present f txt); +fun present_proof f txt = Toplevel.print o Toplevel.present_proof (present f txt); in -val add_chapter = theory Present.section; -val add_section = theory Present.section; -val add_subsection = theory Present.subsection; -val add_subsubsection = theory Present.subsubsection; -val add_text = theory (K ()); -fun add_text_raw txt = theory (K ()) (NONE, txt); -val add_txt = proof (K ()); -val add_txt_raw = add_txt; -val add_sect = add_txt; -val add_subsect = add_txt; -val add_subsubsect = add_txt; +val add_chapter = present_local_theory Present.section; +val add_section = present_local_theory Present.section; +val add_subsection = present_local_theory Present.subsection; +val add_subsubsection = present_local_theory Present.subsubsection; +val add_text = present_local_theory (K ()); +fun add_text_raw txt = present_local_theory (K ()) (NONE, txt); +val add_txt = present_proof (K ()); +val add_txt_raw = add_txt; +val add_sect = add_txt; +val add_subsect = add_txt; +val add_subsubsect = add_txt; end;