src/Pure/Isar/isar_cmd.ML
changeset 58928 23d0ffd48006
parent 58875 ab1c65b015c3
child 58978 e42da880c61e
     1.1 --- a/src/Pure/Isar/isar_cmd.ML	Fri Nov 07 16:22:25 2014 +0100
     1.2 +++ b/src/Pure/Isar/isar_cmd.ML	Fri Nov 07 16:36:55 2014 +0100
     1.3 @@ -48,12 +48,6 @@
     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 local_theory_markup: (xstring * Position.T) option * Symbol_Pos.source ->
     1.8 -    Toplevel.transition -> Toplevel.transition
     1.9 -  val proof_markup: Symbol_Pos.source -> Toplevel.transition -> Toplevel.transition
    1.10 -  val header_markup: Symbol_Pos.source -> Toplevel.transition -> Toplevel.transition
    1.11 -  val heading_markup: (xstring * Position.T) option * Symbol_Pos.source ->
    1.12 -    Toplevel.transition -> Toplevel.transition
    1.13  end;
    1.14  
    1.15  structure Isar_Cmd: ISAR_CMD =
    1.16 @@ -376,28 +370,4 @@
    1.17  
    1.18  end;
    1.19  
    1.20 -
    1.21 -(* markup commands *)
    1.22 -
    1.23 -fun local_theory_markup (loc, txt) = Toplevel.present_local_theory loc (Thy_Output.check_text txt);
    1.24 -val proof_markup = Toplevel.present_proof o Thy_Output.check_text;
    1.25 -
    1.26 -fun reject_target NONE = ()
    1.27 -  | reject_target (SOME (_, pos)) =
    1.28 -      error ("Illegal target specification -- not a theory context" ^ Position.here pos);
    1.29 -
    1.30 -fun header_markup txt =
    1.31 -  Toplevel.keep (fn state =>
    1.32 -    if Toplevel.is_toplevel state then
    1.33 -     (legacy_feature "Obsolete 'header' command -- use 'chapter', 'section' etc. instead";
    1.34 -      Thy_Output.check_text txt state)
    1.35 -    else raise Toplevel.UNDEF);
    1.36 -
    1.37 -fun heading_markup (loc, txt) =
    1.38 -  Toplevel.keep (fn state =>
    1.39 -    if Toplevel.is_toplevel state then (reject_target loc; Thy_Output.check_text txt state)
    1.40 -    else raise Toplevel.UNDEF) o
    1.41 -  local_theory_markup (loc, txt) o
    1.42 -  Toplevel.present_proof (fn state => (reject_target loc; Thy_Output.check_text txt state));
    1.43 -
    1.44  end;