Implemented hiding of proofs and other commands.
1.1 --- a/src/Pure/Isar/isar_output.ML Sat Jan 08 09:30:16 2005 +0100
1.2 +++ b/src/Pure/Isar/isar_output.ML Tue Jan 11 14:08:07 2005 +0100
1.3 @@ -20,11 +20,13 @@
1.4 (Args.src -> Proof.context -> 'a -> string) -> Args.src -> Toplevel.state -> string
1.5 datatype markup = Markup | MarkupEnv | Verbatim
1.6 val interest_level: int ref
1.7 + val hide_commands: bool ref
1.8 + val add_hidden_commands: string list -> unit
1.9 val modes: string list ref
1.10 val eval_antiquote: Scan.lexicon -> Toplevel.state -> string * Position.T -> string
1.11 val parse_thy: (markup -> OuterLex.token list -> OuterLex.token * OuterLex.token list) ->
1.12 Scan.lexicon -> Toplevel.transition list -> (OuterLex.token, 'a) Source.source ->
1.13 - (Toplevel.transition * (Toplevel.state -> Buffer.T -> Buffer.T)) list * Buffer.T
1.14 + (Toplevel.transition * (Toplevel.state -> Toplevel.state -> Buffer.T -> Buffer.T)) list * Buffer.T
1.15 val output_with: (Proof.context -> 'a -> Pretty.T) -> Args.src ->
1.16 Proof.context -> 'a -> string
1.17 end;
1.18 @@ -183,10 +185,30 @@
1.19
1.20 val interest_level = ref 0;
1.21
1.22 -fun present_tokens lex (flag, toks) state =
1.23 +val hide_commands = ref false;
1.24 +val hidden_commands = ref ([] : string list);
1.25 +
1.26 +fun add_hidden_commands cmds = (hidden_commands := !hidden_commands @ cmds);
1.27 +
1.28 +fun is_proof state = (case Toplevel.node_of state of
1.29 + Toplevel.Theory _ => false | _ => true) handle Toplevel.UNDEF => false;
1.30 +
1.31 +fun is_newline (Latex.Basic tk, _) = T.is_newline tk
1.32 + | is_newline _ = false;
1.33 +
1.34 +fun is_hidden (Latex.Basic tk, _) =
1.35 + T.is_kind T.Command tk andalso T.val_of tk mem !hidden_commands
1.36 + | is_hidden _ = false;
1.37 +
1.38 +fun present_tokens lex (flag, toks) state' state =
1.39 Buffer.add (case flag of None => "" | Some b => Latex.flag_markup b) o
1.40 - (toks
1.41 - |> mapfilter (fn (tk, i) => if i > ! interest_level then None else Some tk)
1.42 + ((if !hide_commands andalso exists (is_hidden o fst) toks then[]
1.43 + else mapfilter (fn (tk, i) =>
1.44 + if i > ! interest_level then None
1.45 + else if !hide_commands andalso is_proof state' then
1.46 + if not (is_proof state) andalso is_newline tk then Some tk
1.47 + else None
1.48 + else Some tk) toks)
1.49 |> map (apsnd (eval_antiquote lex state))
1.50 |> Latex.output_tokens
1.51 |> Buffer.add);