src/Pure/Isar/isar_cmd.ML
changeset 58868 c5e1cce7ace3
parent 58201 5bf56c758e02
child 58875 ab1c65b015c3
     1.1 --- a/src/Pure/Isar/isar_cmd.ML	Sun Nov 02 13:26:20 2014 +0100
     1.2 +++ b/src/Pure/Isar/isar_cmd.ML	Sun Nov 02 15:27:37 2014 +0100
     1.3 @@ -48,10 +48,11 @@
     1.4    val print_term: (string list * string) -> Toplevel.transition -> Toplevel.transition
     1.5    val print_type: (string list * (string * string option)) ->
     1.6      Toplevel.transition -> Toplevel.transition
     1.7 -  val header_markup: Symbol_Pos.source -> Toplevel.transition -> Toplevel.transition
     1.8 -  val local_theory_markup: (xstring * Position.T) option * (Symbol_Pos.source) ->
     1.9 +  val local_theory_markup: (xstring * Position.T) option * Symbol_Pos.source ->
    1.10      Toplevel.transition -> Toplevel.transition
    1.11    val proof_markup: Symbol_Pos.source -> Toplevel.transition -> Toplevel.transition
    1.12 +  val heading_markup: (xstring * Position.T) option * Symbol_Pos.source ->
    1.13 +    Toplevel.transition -> Toplevel.transition
    1.14  end;
    1.15  
    1.16  structure Isar_Cmd: ISAR_CMD =
    1.17 @@ -377,11 +378,21 @@
    1.18  
    1.19  (* markup commands *)
    1.20  
    1.21 -fun header_markup txt = Toplevel.keep (fn state =>
    1.22 -  if Toplevel.is_toplevel state then Thy_Output.check_text txt state
    1.23 -  else raise Toplevel.UNDEF);
    1.24 -
    1.25  fun local_theory_markup (loc, txt) = Toplevel.present_local_theory loc (Thy_Output.check_text txt);
    1.26  val proof_markup = Toplevel.present_proof o Thy_Output.check_text;
    1.27  
    1.28 +fun reject_target NONE = ()
    1.29 +  | reject_target (SOME (_, pos)) =
    1.30 +      error ("Illegal target specification -- not a theory context" ^ Position.here pos);
    1.31 +
    1.32 +fun heading_markup (loc, txt) =
    1.33 +  Toplevel.keep (fn state =>
    1.34 +    if Toplevel.is_toplevel state then
    1.35 +     (legacy_feature "Obsolete 'header' command -- use 'chapter', 'section' etc. instead";
    1.36 +      reject_target loc;
    1.37 +      Thy_Output.check_text txt state)
    1.38 +    else raise Toplevel.UNDEF) o
    1.39 +  local_theory_markup (loc, txt) o
    1.40 +  Toplevel.present_proof (fn state => (reject_target loc; Thy_Output.check_text txt state));
    1.41 +
    1.42  end;