src/Pure/Isar/isar_cmd.ML
changeset 58875 ab1c65b015c3
parent 58868 c5e1cce7ace3
child 58928 23d0ffd48006
     1.1 --- a/src/Pure/Isar/isar_cmd.ML	Sun Nov 02 16:54:06 2014 +0100
     1.2 +++ b/src/Pure/Isar/isar_cmd.ML	Sun Nov 02 16:59:40 2014 +0100
     1.3 @@ -51,6 +51,7 @@
     1.4    val local_theory_markup: (xstring * Position.T) option * Symbol_Pos.source ->
     1.5      Toplevel.transition -> Toplevel.transition
     1.6    val proof_markup: Symbol_Pos.source -> Toplevel.transition -> Toplevel.transition
     1.7 +  val header_markup: Symbol_Pos.source -> Toplevel.transition -> Toplevel.transition
     1.8    val heading_markup: (xstring * Position.T) option * Symbol_Pos.source ->
     1.9      Toplevel.transition -> Toplevel.transition
    1.10  end;
    1.11 @@ -385,12 +386,16 @@
    1.12    | reject_target (SOME (_, pos)) =
    1.13        error ("Illegal target specification -- not a theory context" ^ Position.here pos);
    1.14  
    1.15 -fun heading_markup (loc, txt) =
    1.16 +fun header_markup txt =
    1.17    Toplevel.keep (fn state =>
    1.18      if Toplevel.is_toplevel state then
    1.19       (legacy_feature "Obsolete 'header' command -- use 'chapter', 'section' etc. instead";
    1.20 -      reject_target loc;
    1.21        Thy_Output.check_text txt state)
    1.22 +    else raise Toplevel.UNDEF);
    1.23 +
    1.24 +fun heading_markup (loc, txt) =
    1.25 +  Toplevel.keep (fn state =>
    1.26 +    if Toplevel.is_toplevel state then (reject_target loc; Thy_Output.check_text txt state)
    1.27      else raise Toplevel.UNDEF) o
    1.28    local_theory_markup (loc, txt) o
    1.29    Toplevel.present_proof (fn state => (reject_target loc; Thy_Output.check_text txt state));