src/Pure/Interface/proof_general.ML
author wenzelm
Tue, 24 Aug 1999 11:43:30 +0200
changeset 7330 109b1ef4686a
parent 7289 3b1b301467cd
child 7407 fc8cad55af74
permissions -rw-r--r--
print_mode activated again;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
6699
1471f2bd74a0 Configuration for ProofGeneral of LFCS Edinburgh.
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/Interface/proof_general.ML
1471f2bd74a0 Configuration for ProofGeneral of LFCS Edinburgh.
wenzelm
parents:
diff changeset
     2
    ID:         $Id$
1471f2bd74a0 Configuration for ProofGeneral of LFCS Edinburgh.
wenzelm
parents:
diff changeset
     3
    Author:     Markus Wenzel, TU Muenchen
1471f2bd74a0 Configuration for ProofGeneral of LFCS Edinburgh.
wenzelm
parents:
diff changeset
     4
7266
28d95a7a265a isa_action: don't lock pretend_used files;
wenzelm
parents: 7235
diff changeset
     5
Configuration for Proof General of LFCS Edinburgh.
6699
1471f2bd74a0 Configuration for ProofGeneral of LFCS Edinburgh.
wenzelm
parents:
diff changeset
     6
*)
1471f2bd74a0 Configuration for ProofGeneral of LFCS Edinburgh.
wenzelm
parents:
diff changeset
     7
1471f2bd74a0 Configuration for ProofGeneral of LFCS Edinburgh.
wenzelm
parents:
diff changeset
     8
signature PROOF_GENERAL =
1471f2bd74a0 Configuration for ProofGeneral of LFCS Edinburgh.
wenzelm
parents:
diff changeset
     9
sig
6947
a233bc746c75 write_keywords: default file name;
wenzelm
parents: 6861
diff changeset
    10
  val write_keywords: unit -> unit
6699
1471f2bd74a0 Configuration for ProofGeneral of LFCS Edinburgh.
wenzelm
parents:
diff changeset
    11
  val setup: (theory -> theory) list
7193
cc7a89d233f7 proper ProofGeneral/isa setup;
wenzelm
parents: 7100
diff changeset
    12
  val help: unit -> unit
cc7a89d233f7 proper ProofGeneral/isa setup;
wenzelm
parents: 7100
diff changeset
    13
  val show_context: unit -> theory
cc7a89d233f7 proper ProofGeneral/isa setup;
wenzelm
parents: 7100
diff changeset
    14
  val kill_goal: unit -> unit
cc7a89d233f7 proper ProofGeneral/isa setup;
wenzelm
parents: 7100
diff changeset
    15
  val repeat_undo: int -> unit
7235
3c3defaad8ae Goals.reset_goals;
wenzelm
parents: 7210
diff changeset
    16
  val isa_restart: unit -> unit
6699
1471f2bd74a0 Configuration for ProofGeneral of LFCS Edinburgh.
wenzelm
parents:
diff changeset
    17
  val init: bool -> unit
1471f2bd74a0 Configuration for ProofGeneral of LFCS Edinburgh.
wenzelm
parents:
diff changeset
    18
end;
1471f2bd74a0 Configuration for ProofGeneral of LFCS Edinburgh.
wenzelm
parents:
diff changeset
    19
1471f2bd74a0 Configuration for ProofGeneral of LFCS Edinburgh.
wenzelm
parents:
diff changeset
    20
structure ProofGeneral: PROOF_GENERAL =
1471f2bd74a0 Configuration for ProofGeneral of LFCS Edinburgh.
wenzelm
parents:
diff changeset
    21
struct
1471f2bd74a0 Configuration for ProofGeneral of LFCS Edinburgh.
wenzelm
parents:
diff changeset
    22
1471f2bd74a0 Configuration for ProofGeneral of LFCS Edinburgh.
wenzelm
parents:
diff changeset
    23
6720
353bd9b74b1f write_keywords generates outer syntax keyword classification in elisp;
wenzelm
parents: 6699
diff changeset
    24
(** generate keyword classification file **)
353bd9b74b1f write_keywords generates outer syntax keyword classification in elisp;
wenzelm
parents: 6699
diff changeset
    25
353bd9b74b1f write_keywords generates outer syntax keyword classification in elisp;
wenzelm
parents: 6699
diff changeset
    26
local
353bd9b74b1f write_keywords generates outer syntax keyword classification in elisp;
wenzelm
parents: 6699
diff changeset
    27
353bd9b74b1f write_keywords generates outer syntax keyword classification in elisp;
wenzelm
parents: 6699
diff changeset
    28
val regexp_meta = explode ".*+?[]^$";
353bd9b74b1f write_keywords generates outer syntax keyword classification in elisp;
wenzelm
parents: 6699
diff changeset
    29
val regexp_quote = implode o map (fn c => if c mem regexp_meta then "\\\\" ^ c else c) o explode;
353bd9b74b1f write_keywords generates outer syntax keyword classification in elisp;
wenzelm
parents: 6699
diff changeset
    30
353bd9b74b1f write_keywords generates outer syntax keyword classification in elisp;
wenzelm
parents: 6699
diff changeset
    31
fun defconst name strs =
353bd9b74b1f write_keywords generates outer syntax keyword classification in elisp;
wenzelm
parents: 6699
diff changeset
    32
  "\n(defconst isar-keywords-" ^ name ^
353bd9b74b1f write_keywords generates outer syntax keyword classification in elisp;
wenzelm
parents: 6699
diff changeset
    33
  "\n  '(" ^ space_implode "\n    " (map (quote o regexp_quote) strs) ^ "))\n";
353bd9b74b1f write_keywords generates outer syntax keyword classification in elisp;
wenzelm
parents: 6699
diff changeset
    34
353bd9b74b1f write_keywords generates outer syntax keyword classification in elisp;
wenzelm
parents: 6699
diff changeset
    35
fun make_elisp_commands commands kind =
7027
ca0fbe679bbb adapted to dest_keywords, dest_parsers;
wenzelm
parents: 6947
diff changeset
    36
  defconst kind (mapfilter (fn (c, _, k, _) => if k = kind then Some c else None) commands);
6720
353bd9b74b1f write_keywords generates outer syntax keyword classification in elisp;
wenzelm
parents: 6699
diff changeset
    37
353bd9b74b1f write_keywords generates outer syntax keyword classification in elisp;
wenzelm
parents: 6699
diff changeset
    38
fun make_elisp_syntax (keywords, commands) =
353bd9b74b1f write_keywords generates outer syntax keyword classification in elisp;
wenzelm
parents: 6699
diff changeset
    39
  ";;\n\
353bd9b74b1f write_keywords generates outer syntax keyword classification in elisp;
wenzelm
parents: 6699
diff changeset
    40
  \;; Keyword classification tables for Isabelle/Isar.\n\
353bd9b74b1f write_keywords generates outer syntax keyword classification in elisp;
wenzelm
parents: 6699
diff changeset
    41
  \;; This file generated by Isabelle -- DO NOT EDIT!\n\
353bd9b74b1f write_keywords generates outer syntax keyword classification in elisp;
wenzelm
parents: 6699
diff changeset
    42
  \;;\n\
6724
b5007e5e8a1b fixed cvs Id;
wenzelm
parents: 6720
diff changeset
    43
  \;; $" ^ "Id$\n\
6720
353bd9b74b1f write_keywords generates outer syntax keyword classification in elisp;
wenzelm
parents: 6699
diff changeset
    44
  \;;\n" ^
7027
ca0fbe679bbb adapted to dest_keywords, dest_parsers;
wenzelm
parents: 6947
diff changeset
    45
  defconst "minor" (filter Syntax.is_identifier keywords) ^
6720
353bd9b74b1f write_keywords generates outer syntax keyword classification in elisp;
wenzelm
parents: 6699
diff changeset
    46
  implode (map (make_elisp_commands commands) OuterSyntax.Keyword.kinds) ^
353bd9b74b1f write_keywords generates outer syntax keyword classification in elisp;
wenzelm
parents: 6699
diff changeset
    47
  "\n(provide 'isar-keywords)\n";
353bd9b74b1f write_keywords generates outer syntax keyword classification in elisp;
wenzelm
parents: 6699
diff changeset
    48
6947
a233bc746c75 write_keywords: default file name;
wenzelm
parents: 6861
diff changeset
    49
val keywords_file = "isar-keywords.el";
a233bc746c75 write_keywords: default file name;
wenzelm
parents: 6861
diff changeset
    50
6720
353bd9b74b1f write_keywords generates outer syntax keyword classification in elisp;
wenzelm
parents: 6699
diff changeset
    51
in
353bd9b74b1f write_keywords generates outer syntax keyword classification in elisp;
wenzelm
parents: 6699
diff changeset
    52
6947
a233bc746c75 write_keywords: default file name;
wenzelm
parents: 6861
diff changeset
    53
fun write_keywords () =
7027
ca0fbe679bbb adapted to dest_keywords, dest_parsers;
wenzelm
parents: 6947
diff changeset
    54
  File.write (Path.unpack keywords_file)
ca0fbe679bbb adapted to dest_keywords, dest_parsers;
wenzelm
parents: 6947
diff changeset
    55
    (make_elisp_syntax (OuterSyntax.dest_keywords (), OuterSyntax.dest_parsers ()));
6720
353bd9b74b1f write_keywords generates outer syntax keyword classification in elisp;
wenzelm
parents: 6699
diff changeset
    56
353bd9b74b1f write_keywords generates outer syntax keyword classification in elisp;
wenzelm
parents: 6699
diff changeset
    57
end;
353bd9b74b1f write_keywords generates outer syntax keyword classification in elisp;
wenzelm
parents: 6699
diff changeset
    58
353bd9b74b1f write_keywords generates outer syntax keyword classification in elisp;
wenzelm
parents: 6699
diff changeset
    59
353bd9b74b1f write_keywords generates outer syntax keyword classification in elisp;
wenzelm
parents: 6699
diff changeset
    60
6699
1471f2bd74a0 Configuration for ProofGeneral of LFCS Edinburgh.
wenzelm
parents:
diff changeset
    61
(** compile-time theory setup **)
1471f2bd74a0 Configuration for ProofGeneral of LFCS Edinburgh.
wenzelm
parents:
diff changeset
    62
1471f2bd74a0 Configuration for ProofGeneral of LFCS Edinburgh.
wenzelm
parents:
diff changeset
    63
(* token translations *)
1471f2bd74a0 Configuration for ProofGeneral of LFCS Edinburgh.
wenzelm
parents:
diff changeset
    64
1471f2bd74a0 Configuration for ProofGeneral of LFCS Edinburgh.
wenzelm
parents:
diff changeset
    65
val proof_generalN = "ProofGeneral";
1471f2bd74a0 Configuration for ProofGeneral of LFCS Edinburgh.
wenzelm
parents:
diff changeset
    66
1471f2bd74a0 Configuration for ProofGeneral of LFCS Edinburgh.
wenzelm
parents:
diff changeset
    67
local
1471f2bd74a0 Configuration for ProofGeneral of LFCS Edinburgh.
wenzelm
parents:
diff changeset
    68
1471f2bd74a0 Configuration for ProofGeneral of LFCS Edinburgh.
wenzelm
parents:
diff changeset
    69
val end_tag = oct_char "350";
1471f2bd74a0 Configuration for ProofGeneral of LFCS Edinburgh.
wenzelm
parents:
diff changeset
    70
val tclass_tag = oct_char "351";
1471f2bd74a0 Configuration for ProofGeneral of LFCS Edinburgh.
wenzelm
parents:
diff changeset
    71
val tfree_tag = oct_char "352";
1471f2bd74a0 Configuration for ProofGeneral of LFCS Edinburgh.
wenzelm
parents:
diff changeset
    72
val tvar_tag = oct_char "353";
1471f2bd74a0 Configuration for ProofGeneral of LFCS Edinburgh.
wenzelm
parents:
diff changeset
    73
val free_tag = oct_char "354";
1471f2bd74a0 Configuration for ProofGeneral of LFCS Edinburgh.
wenzelm
parents:
diff changeset
    74
val bound_tag = oct_char "355";
1471f2bd74a0 Configuration for ProofGeneral of LFCS Edinburgh.
wenzelm
parents:
diff changeset
    75
val var_tag = oct_char "356";
1471f2bd74a0 Configuration for ProofGeneral of LFCS Edinburgh.
wenzelm
parents:
diff changeset
    76
1471f2bd74a0 Configuration for ProofGeneral of LFCS Edinburgh.
wenzelm
parents:
diff changeset
    77
fun tagit p x = (p ^ x ^ end_tag, real (size x));
1471f2bd74a0 Configuration for ProofGeneral of LFCS Edinburgh.
wenzelm
parents:
diff changeset
    78
1471f2bd74a0 Configuration for ProofGeneral of LFCS Edinburgh.
wenzelm
parents:
diff changeset
    79
in
1471f2bd74a0 Configuration for ProofGeneral of LFCS Edinburgh.
wenzelm
parents:
diff changeset
    80
1471f2bd74a0 Configuration for ProofGeneral of LFCS Edinburgh.
wenzelm
parents:
diff changeset
    81
val proof_general_trans =
1471f2bd74a0 Configuration for ProofGeneral of LFCS Edinburgh.
wenzelm
parents:
diff changeset
    82
 Syntax.tokentrans_mode proof_generalN
1471f2bd74a0 Configuration for ProofGeneral of LFCS Edinburgh.
wenzelm
parents:
diff changeset
    83
  [("class", tagit tclass_tag),
1471f2bd74a0 Configuration for ProofGeneral of LFCS Edinburgh.
wenzelm
parents:
diff changeset
    84
   ("tfree", tagit tfree_tag),
1471f2bd74a0 Configuration for ProofGeneral of LFCS Edinburgh.
wenzelm
parents:
diff changeset
    85
   ("tvar", tagit tvar_tag),
1471f2bd74a0 Configuration for ProofGeneral of LFCS Edinburgh.
wenzelm
parents:
diff changeset
    86
   ("free", tagit free_tag),
1471f2bd74a0 Configuration for ProofGeneral of LFCS Edinburgh.
wenzelm
parents:
diff changeset
    87
   ("bound", tagit bound_tag),
1471f2bd74a0 Configuration for ProofGeneral of LFCS Edinburgh.
wenzelm
parents:
diff changeset
    88
   ("var", tagit var_tag)];
1471f2bd74a0 Configuration for ProofGeneral of LFCS Edinburgh.
wenzelm
parents:
diff changeset
    89
1471f2bd74a0 Configuration for ProofGeneral of LFCS Edinburgh.
wenzelm
parents:
diff changeset
    90
end;
1471f2bd74a0 Configuration for ProofGeneral of LFCS Edinburgh.
wenzelm
parents:
diff changeset
    91
1471f2bd74a0 Configuration for ProofGeneral of LFCS Edinburgh.
wenzelm
parents:
diff changeset
    92
1471f2bd74a0 Configuration for ProofGeneral of LFCS Edinburgh.
wenzelm
parents:
diff changeset
    93
(* setup *)
1471f2bd74a0 Configuration for ProofGeneral of LFCS Edinburgh.
wenzelm
parents:
diff changeset
    94
1471f2bd74a0 Configuration for ProofGeneral of LFCS Edinburgh.
wenzelm
parents:
diff changeset
    95
val setup = [Theory.add_tokentrfuns proof_general_trans];
1471f2bd74a0 Configuration for ProofGeneral of LFCS Edinburgh.
wenzelm
parents:
diff changeset
    96
1471f2bd74a0 Configuration for ProofGeneral of LFCS Edinburgh.
wenzelm
parents:
diff changeset
    97
1471f2bd74a0 Configuration for ProofGeneral of LFCS Edinburgh.
wenzelm
parents:
diff changeset
    98
7193
cc7a89d233f7 proper ProofGeneral/isa setup;
wenzelm
parents: 7100
diff changeset
    99
(** run-time operations **)
6699
1471f2bd74a0 Configuration for ProofGeneral of LFCS Edinburgh.
wenzelm
parents:
diff changeset
   100
1471f2bd74a0 Configuration for ProofGeneral of LFCS Edinburgh.
wenzelm
parents:
diff changeset
   101
(* messages *)
1471f2bd74a0 Configuration for ProofGeneral of LFCS Edinburgh.
wenzelm
parents:
diff changeset
   102
7193
cc7a89d233f7 proper ProofGeneral/isa setup;
wenzelm
parents: 7100
diff changeset
   103
val plain_output = std_output o suffix "\n";
7195
a38dc0c6b244 made SML happy;
wenzelm
parents: 7193
diff changeset
   104
fun plain_writeln x = Library.setmp writeln_fn plain_output x;
7193
cc7a89d233f7 proper ProofGeneral/isa setup;
wenzelm
parents: 7100
diff changeset
   105
cc7a89d233f7 proper ProofGeneral/isa setup;
wenzelm
parents: 7100
diff changeset
   106
fun decorate_lines bg en "" = plain_output o enclose bg en
cc7a89d233f7 proper ProofGeneral/isa setup;
wenzelm
parents: 7100
diff changeset
   107
  | decorate_lines bg en prfx = plain_output o enclose bg en o prefix_lines prfx;
6699
1471f2bd74a0 Configuration for ProofGeneral of LFCS Edinburgh.
wenzelm
parents:
diff changeset
   108
1471f2bd74a0 Configuration for ProofGeneral of LFCS Edinburgh.
wenzelm
parents:
diff changeset
   109
fun setup_messages () =
1471f2bd74a0 Configuration for ProofGeneral of LFCS Edinburgh.
wenzelm
parents:
diff changeset
   110
 (writeln_fn := (decorate_lines (oct_char "360") (oct_char "361") "");
1471f2bd74a0 Configuration for ProofGeneral of LFCS Edinburgh.
wenzelm
parents:
diff changeset
   111
  warning_fn := (decorate_lines (oct_char "362") (oct_char "363") "### ");
1471f2bd74a0 Configuration for ProofGeneral of LFCS Edinburgh.
wenzelm
parents:
diff changeset
   112
  error_fn := (decorate_lines (oct_char "364") (oct_char "365") "*** "));
1471f2bd74a0 Configuration for ProofGeneral of LFCS Edinburgh.
wenzelm
parents:
diff changeset
   113
1471f2bd74a0 Configuration for ProofGeneral of LFCS Edinburgh.
wenzelm
parents:
diff changeset
   114
1471f2bd74a0 Configuration for ProofGeneral of LFCS Edinburgh.
wenzelm
parents:
diff changeset
   115
(* theory / proof state *)
1471f2bd74a0 Configuration for ProofGeneral of LFCS Edinburgh.
wenzelm
parents:
diff changeset
   116
7193
cc7a89d233f7 proper ProofGeneral/isa setup;
wenzelm
parents: 7100
diff changeset
   117
fun print_current_goals n max th = plain_writeln (Goals.print_current_goals_default n max) th;
cc7a89d233f7 proper ProofGeneral/isa setup;
wenzelm
parents: 7100
diff changeset
   118
cc7a89d233f7 proper ProofGeneral/isa setup;
wenzelm
parents: 7100
diff changeset
   119
fun setup_state isar =
6699
1471f2bd74a0 Configuration for ProofGeneral of LFCS Edinburgh.
wenzelm
parents:
diff changeset
   120
  (current_goals_markers :=
1471f2bd74a0 Configuration for ProofGeneral of LFCS Edinburgh.
wenzelm
parents:
diff changeset
   121
    let
1471f2bd74a0 Configuration for ProofGeneral of LFCS Edinburgh.
wenzelm
parents:
diff changeset
   122
      val begin_state = oct_char "366";
1471f2bd74a0 Configuration for ProofGeneral of LFCS Edinburgh.
wenzelm
parents:
diff changeset
   123
      val end_state= oct_char "367";
1471f2bd74a0 Configuration for ProofGeneral of LFCS Edinburgh.
wenzelm
parents:
diff changeset
   124
      val begin_goal = oct_char "370";
1471f2bd74a0 Configuration for ProofGeneral of LFCS Edinburgh.
wenzelm
parents:
diff changeset
   125
    in (begin_state, end_state, begin_goal) end;
7193
cc7a89d233f7 proper ProofGeneral/isa setup;
wenzelm
parents: 7100
diff changeset
   126
  if isar then
cc7a89d233f7 proper ProofGeneral/isa setup;
wenzelm
parents: 7100
diff changeset
   127
   (Toplevel.print_state_fn := plain_writeln Toplevel.print_state_default;
cc7a89d233f7 proper ProofGeneral/isa setup;
wenzelm
parents: 7100
diff changeset
   128
    Toplevel.prompt_state_fn := (suffix (oct_char "372") o Toplevel.prompt_state_default))
cc7a89d233f7 proper ProofGeneral/isa setup;
wenzelm
parents: 7100
diff changeset
   129
  else Goals.print_current_goals_fn := print_current_goals);
6699
1471f2bd74a0 Configuration for ProofGeneral of LFCS Edinburgh.
wenzelm
parents:
diff changeset
   130
1471f2bd74a0 Configuration for ProofGeneral of LFCS Edinburgh.
wenzelm
parents:
diff changeset
   131
7100
4f777a0e1c8b setup_thy_loader;
wenzelm
parents: 7027
diff changeset
   132
(* theory loader actions *)
4f777a0e1c8b setup_thy_loader;
wenzelm
parents: 7027
diff changeset
   133
4f777a0e1c8b setup_thy_loader;
wenzelm
parents: 7027
diff changeset
   134
local
4f777a0e1c8b setup_thy_loader;
wenzelm
parents: 7027
diff changeset
   135
4f777a0e1c8b setup_thy_loader;
wenzelm
parents: 7027
diff changeset
   136
fun tell_pg msg name = writeln ("Proof General, " ^ msg ^ " " ^ quote name);
4f777a0e1c8b setup_thy_loader;
wenzelm
parents: 7027
diff changeset
   137
7193
cc7a89d233f7 proper ProofGeneral/isa setup;
wenzelm
parents: 7100
diff changeset
   138
fun isa_action action name =
7266
28d95a7a265a isa_action: don't lock pretend_used files;
wenzelm
parents: 7235
diff changeset
   139
  let
28d95a7a265a isa_action: don't lock pretend_used files;
wenzelm
parents: 7235
diff changeset
   140
    val update = (action = ThyInfo.Update);
28d95a7a265a isa_action: don't lock pretend_used files;
wenzelm
parents: 7235
diff changeset
   141
    fun loaded ((path, _), really) =
28d95a7a265a isa_action: don't lock pretend_used files;
wenzelm
parents: 7235
diff changeset
   142
      if update andalso not really then None
28d95a7a265a isa_action: don't lock pretend_used files;
wenzelm
parents: 7235
diff changeset
   143
      else Some (File.sysify_path path);
28d95a7a265a isa_action: don't lock pretend_used files;
wenzelm
parents: 7235
diff changeset
   144
    val files = mapfilter loaded (ThyInfo.loaded_files name);
28d95a7a265a isa_action: don't lock pretend_used files;
wenzelm
parents: 7235
diff changeset
   145
  in
28d95a7a265a isa_action: don't lock pretend_used files;
wenzelm
parents: 7235
diff changeset
   146
    if update then seq (tell_pg "this file is loaded:") files
7193
cc7a89d233f7 proper ProofGeneral/isa setup;
wenzelm
parents: 7100
diff changeset
   147
    else seq (tell_pg "you can unlock the file") files
cc7a89d233f7 proper ProofGeneral/isa setup;
wenzelm
parents: 7100
diff changeset
   148
  end;
cc7a89d233f7 proper ProofGeneral/isa setup;
wenzelm
parents: 7100
diff changeset
   149
cc7a89d233f7 proper ProofGeneral/isa setup;
wenzelm
parents: 7100
diff changeset
   150
fun isar_action action name =
cc7a89d233f7 proper ProofGeneral/isa setup;
wenzelm
parents: 7100
diff changeset
   151
  if action = ThyInfo.Update then tell_pg "this theory is loaded:" name
cc7a89d233f7 proper ProofGeneral/isa setup;
wenzelm
parents: 7100
diff changeset
   152
  else tell_pg "you can unlock the theory" name;
7100
4f777a0e1c8b setup_thy_loader;
wenzelm
parents: 7027
diff changeset
   153
4f777a0e1c8b setup_thy_loader;
wenzelm
parents: 7027
diff changeset
   154
in
7193
cc7a89d233f7 proper ProofGeneral/isa setup;
wenzelm
parents: 7100
diff changeset
   155
  fun setup_thy_loader isar = ThyInfo.add_hook (if isar then isar_action else isa_action);
7100
4f777a0e1c8b setup_thy_loader;
wenzelm
parents: 7027
diff changeset
   156
end;
4f777a0e1c8b setup_thy_loader;
wenzelm
parents: 7027
diff changeset
   157
4f777a0e1c8b setup_thy_loader;
wenzelm
parents: 7027
diff changeset
   158
7193
cc7a89d233f7 proper ProofGeneral/isa setup;
wenzelm
parents: 7100
diff changeset
   159
(* some top-level commands for ProofGeneral/isa *)
cc7a89d233f7 proper ProofGeneral/isa setup;
wenzelm
parents: 7100
diff changeset
   160
cc7a89d233f7 proper ProofGeneral/isa setup;
wenzelm
parents: 7100
diff changeset
   161
val help = writeln o Session.welcome;
cc7a89d233f7 proper ProofGeneral/isa setup;
wenzelm
parents: 7100
diff changeset
   162
val show_context = Context.the_context;
cc7a89d233f7 proper ProofGeneral/isa setup;
wenzelm
parents: 7100
diff changeset
   163
cc7a89d233f7 proper ProofGeneral/isa setup;
wenzelm
parents: 7100
diff changeset
   164
fun kill_goal () =
7266
28d95a7a265a isa_action: don't lock pretend_used files;
wenzelm
parents: 7235
diff changeset
   165
  (Goals.reset_goals (); writeln "Proof General, please clear the goals buffer.");
7193
cc7a89d233f7 proper ProofGeneral/isa setup;
wenzelm
parents: 7100
diff changeset
   166
cc7a89d233f7 proper ProofGeneral/isa setup;
wenzelm
parents: 7100
diff changeset
   167
fun repeat_undo 0 = ()
cc7a89d233f7 proper ProofGeneral/isa setup;
wenzelm
parents: 7100
diff changeset
   168
  | repeat_undo n = (undo(); repeat_undo (n - 1));
cc7a89d233f7 proper ProofGeneral/isa setup;
wenzelm
parents: 7100
diff changeset
   169
cc7a89d233f7 proper ProofGeneral/isa setup;
wenzelm
parents: 7100
diff changeset
   170
fun isa_restart () =
7210
ae9a645e8728 tuned prompts;
wenzelm
parents: 7195
diff changeset
   171
 (ml_prompts ("> " ^ oct_char "372") ("- " ^ oct_char "373");
7193
cc7a89d233f7 proper ProofGeneral/isa setup;
wenzelm
parents: 7100
diff changeset
   172
  ThyInfo.touch_all_thys ();
cc7a89d233f7 proper ProofGeneral/isa setup;
wenzelm
parents: 7100
diff changeset
   173
  kill_goal ();
7266
28d95a7a265a isa_action: don't lock pretend_used files;
wenzelm
parents: 7235
diff changeset
   174
  writeln "Proof General, please clear the response buffer.";
7193
cc7a89d233f7 proper ProofGeneral/isa setup;
wenzelm
parents: 7100
diff changeset
   175
  writeln "Isabelle Proof General: Isabelle process ready!");
cc7a89d233f7 proper ProofGeneral/isa setup;
wenzelm
parents: 7100
diff changeset
   176
cc7a89d233f7 proper ProofGeneral/isa setup;
wenzelm
parents: 7100
diff changeset
   177
6699
1471f2bd74a0 Configuration for ProofGeneral of LFCS Edinburgh.
wenzelm
parents:
diff changeset
   178
(* init *)
1471f2bd74a0 Configuration for ProofGeneral of LFCS Edinburgh.
wenzelm
parents:
diff changeset
   179
1471f2bd74a0 Configuration for ProofGeneral of LFCS Edinburgh.
wenzelm
parents:
diff changeset
   180
fun init isar =
1471f2bd74a0 Configuration for ProofGeneral of LFCS Edinburgh.
wenzelm
parents:
diff changeset
   181
 (setup_messages ();
7193
cc7a89d233f7 proper ProofGeneral/isa setup;
wenzelm
parents: 7100
diff changeset
   182
  setup_state isar;
cc7a89d233f7 proper ProofGeneral/isa setup;
wenzelm
parents: 7100
diff changeset
   183
  setup_thy_loader isar;
7330
109b1ef4686a print_mode activated again;
wenzelm
parents: 7289
diff changeset
   184
  print_mode := [proof_generalN];
6699
1471f2bd74a0 Configuration for ProofGeneral of LFCS Edinburgh.
wenzelm
parents:
diff changeset
   185
  set quick_and_dirty;
7193
cc7a89d233f7 proper ProofGeneral/isa setup;
wenzelm
parents: 7100
diff changeset
   186
  if isar then Isar.sync_main () else isa_restart ());
6699
1471f2bd74a0 Configuration for ProofGeneral of LFCS Edinburgh.
wenzelm
parents:
diff changeset
   187
1471f2bd74a0 Configuration for ProofGeneral of LFCS Edinburgh.
wenzelm
parents:
diff changeset
   188
1471f2bd74a0 Configuration for ProofGeneral of LFCS Edinburgh.
wenzelm
parents:
diff changeset
   189
end;