Markup.output;
authorwenzelm
Tue Jul 10 16:45:04 2007 +0200 (2007-07-10)
changeset 237011716f19e7d25
parent 23700 fb1102e98cd4
child 23702 58ca991e0702
Markup.output;
removed no_state markup -- produce empty state;
src/Pure/Isar/toplevel.ML
     1.1 --- a/src/Pure/Isar/toplevel.ML	Tue Jul 10 16:45:03 2007 +0200
     1.2 +++ b/src/Pure/Isar/toplevel.ML	Tue Jul 10 16:45:04 2007 +0200
     1.3 @@ -213,16 +213,14 @@
     1.4    |> Pretty.chunks |> Pretty.writeln;
     1.5  
     1.6  fun print_state prf_only state =
     1.7 -  let val prts =
     1.8 -    (case try node_of state of
     1.9 -      NONE => []
    1.10 -    | SOME (Theory (gthy, _)) => if prf_only then [] else pretty_context gthy
    1.11 -    | SOME (Proof (prf, _)) =>
    1.12 -        Proof.pretty_state (ProofHistory.position prf) (ProofHistory.current prf)
    1.13 -    | SOME (SkipProof (h, _)) =>
    1.14 -        [Pretty.str ("skipped proof: depth " ^ string_of_int (History.current h))])
    1.15 -  in Pretty.markup_chunks (if null prts then Markup.no_state else Markup.state) prts end
    1.16 -  |> Pretty.writeln;
    1.17 +  (case try node_of state of
    1.18 +    NONE => []
    1.19 +  | SOME (Theory (gthy, _)) => if prf_only then [] else pretty_context gthy
    1.20 +  | SOME (Proof (prf, _)) =>
    1.21 +      Proof.pretty_state (ProofHistory.position prf) (ProofHistory.current prf)
    1.22 +  | SOME (SkipProof (h, _)) =>
    1.23 +      [Pretty.str ("skipped proof: depth " ^ string_of_int (History.current h))])
    1.24 +  |> Pretty.markup_chunks Markup.state |> Pretty.writeln;
    1.25  
    1.26  
    1.27  
    1.28 @@ -754,7 +752,7 @@
    1.29  
    1.30  fun raw_loop src =
    1.31    let val prompt =
    1.32 -    Output.escape (Source.default_prompt |> (Pretty.mode_markup Markup.prompt |-> enclose))
    1.33 +    Output.escape ((Markup.output Markup.prompt |-> enclose) Source.default_prompt)
    1.34    in
    1.35      (case get_interrupt (Source.set_prompt prompt src) of
    1.36        NONE => (writeln "\nInterrupt."; raw_loop src)