18 val integer: string -> int |
18 val integer: string -> int |
19 val args: (Proof.context * Args.T list -> 'a * (Proof.context * Args.T list)) -> |
19 val args: (Proof.context * Args.T list -> 'a * (Proof.context * Args.T list)) -> |
20 (Args.src -> Proof.context -> 'a -> string) -> Args.src -> Toplevel.state -> string |
20 (Args.src -> Proof.context -> 'a -> string) -> Args.src -> Toplevel.state -> string |
21 datatype markup = Markup | MarkupEnv | Verbatim |
21 datatype markup = Markup | MarkupEnv | Verbatim |
22 val interest_level: int ref |
22 val interest_level: int ref |
|
23 val hide_commands: bool ref |
|
24 val add_hidden_commands: string list -> unit |
23 val modes: string list ref |
25 val modes: string list ref |
24 val eval_antiquote: Scan.lexicon -> Toplevel.state -> string * Position.T -> string |
26 val eval_antiquote: Scan.lexicon -> Toplevel.state -> string * Position.T -> string |
25 val parse_thy: (markup -> OuterLex.token list -> OuterLex.token * OuterLex.token list) -> |
27 val parse_thy: (markup -> OuterLex.token list -> OuterLex.token * OuterLex.token list) -> |
26 Scan.lexicon -> Toplevel.transition list -> (OuterLex.token, 'a) Source.source -> |
28 Scan.lexicon -> Toplevel.transition list -> (OuterLex.token, 'a) Source.source -> |
27 (Toplevel.transition * (Toplevel.state -> Buffer.T -> Buffer.T)) list * Buffer.T |
29 (Toplevel.transition * (Toplevel.state -> Toplevel.state -> Buffer.T -> Buffer.T)) list * Buffer.T |
28 val output_with: (Proof.context -> 'a -> Pretty.T) -> Args.src -> |
30 val output_with: (Proof.context -> 'a -> Pretty.T) -> Args.src -> |
29 Proof.context -> 'a -> string |
31 Proof.context -> 'a -> string |
30 end; |
32 end; |
31 |
33 |
32 structure IsarOutput: ISAR_OUTPUT = |
34 structure IsarOutput: ISAR_OUTPUT = |
181 |
183 |
182 (* present_tokens *) |
184 (* present_tokens *) |
183 |
185 |
184 val interest_level = ref 0; |
186 val interest_level = ref 0; |
185 |
187 |
186 fun present_tokens lex (flag, toks) state = |
188 val hide_commands = ref false; |
|
189 val hidden_commands = ref ([] : string list); |
|
190 |
|
191 fun add_hidden_commands cmds = (hidden_commands := !hidden_commands @ cmds); |
|
192 |
|
193 fun is_proof state = (case Toplevel.node_of state of |
|
194 Toplevel.Theory _ => false | _ => true) handle Toplevel.UNDEF => false; |
|
195 |
|
196 fun is_newline (Latex.Basic tk, _) = T.is_newline tk |
|
197 | is_newline _ = false; |
|
198 |
|
199 fun is_hidden (Latex.Basic tk, _) = |
|
200 T.is_kind T.Command tk andalso T.val_of tk mem !hidden_commands |
|
201 | is_hidden _ = false; |
|
202 |
|
203 fun present_tokens lex (flag, toks) state' state = |
187 Buffer.add (case flag of None => "" | Some b => Latex.flag_markup b) o |
204 Buffer.add (case flag of None => "" | Some b => Latex.flag_markup b) o |
188 (toks |
205 ((if !hide_commands andalso exists (is_hidden o fst) toks then[] |
189 |> mapfilter (fn (tk, i) => if i > ! interest_level then None else Some tk) |
206 else mapfilter (fn (tk, i) => |
|
207 if i > ! interest_level then None |
|
208 else if !hide_commands andalso is_proof state' then |
|
209 if not (is_proof state) andalso is_newline tk then Some tk |
|
210 else None |
|
211 else Some tk) toks) |
190 |> map (apsnd (eval_antiquote lex state)) |
212 |> map (apsnd (eval_antiquote lex state)) |
191 |> Latex.output_tokens |
213 |> Latex.output_tokens |
192 |> Buffer.add); |
214 |> Buffer.add); |
193 |
215 |
194 |
216 |