clarified legacy command;
authorwenzelm
Sun Nov 02 16:59:40 2014 +0100 (2014-11-02 ago)
changeset 58875ab1c65b015c3
parent 58874 7172c7ffb047
child 58876 1888e3cb8048
clarified legacy command;
src/Pure/Isar/isar_cmd.ML
src/Pure/Isar/isar_syn.ML
     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));
     2.1 --- a/src/Pure/Isar/isar_syn.ML	Sun Nov 02 16:54:06 2014 +0100
     2.2 +++ b/src/Pure/Isar/isar_syn.ML	Sun Nov 02 16:59:40 2014 +0100
     2.3 @@ -12,7 +12,7 @@
     2.4  val _ =
     2.5    Outer_Syntax.markup_command Thy_Output.Markup
     2.6      @{command_spec "header"} "theory header"
     2.7 -    (Parse.document_source >> (fn s => Isar_Cmd.heading_markup (NONE, s)));
     2.8 +    (Parse.document_source >> Isar_Cmd.header_markup);
     2.9  
    2.10  val _ =
    2.11    Outer_Syntax.markup_command Thy_Output.Markup