blob: 8cf11f2f186b40a32b85c30a97558ae6eccf1ed1 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
|
(*
Isabelle/Isar configuration for Proof General.
Author: David Aspinall <da@dcs.ed.ac.uk>
Contact: Isabelle maintainer <isabelle@dcs.ed.ac.uk>
ProofGeneral.ML,v 2.16 1998/11/03 16:29:30 da Exp
MMW: I have temporarily removed the theory loader patches, since it
kept crashing on me.
*)
(** configure output channels to decorate output **)
(*messages*)
writeln_fn :=
(std_output o suffix "\n" o enclose (oct_char "360") (oct_char "361"));
warning_fn :=
(std_output o suffix "\n" o enclose (oct_char "362") (oct_char "363") o prefix_lines "### ");
error_fn :=
(std_output o suffix "\n" o enclose (oct_char "364") (oct_char "365") o prefix_lines "*** ");
(*prompts*)
Source.decorate_prompt_fn := (fn s => s ^ oct_char "372");
(*theory / proof state*)
current_goals_markers :=
let
val begin_state = oct_char "366";
val end_state= oct_char "367";
val begin_goal = oct_char "370";
in (begin_state, end_state, begin_goal) end;
Toplevel.print_state_fn :=
(Library.setmp writeln_fn (std_output o suffix "\n") Toplevel.print_state_default);
print_mode := ["ProofGeneral"];
Isar.main();
|
