src/Pure/proof_general.ML
author aspinall
Mon, 16 Aug 2004 18:05:41 +0200
changeset 15134 d3fa5e1d6e4d
parent 15010 72fbe711e414
child 15145 07360eef9f4f
permissions -rw-r--r--
Experimental version supporting PGIP, merged with main branch with help from Makarius.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
12780
6b41c750451c tuned title;
wenzelm
parents: 12778
diff changeset
     1
(*  Title:      Pure/proof_general.ML
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
     2
    ID:         $Id$
14675
08b9c690f9cf removed obsolete 'undo';
wenzelm
parents: 14568
diff changeset
     3
    Author:     David Aspinall and Markus Wenzel
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
     4
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
     5
Isabelle configuration for Proof General (see http://proofgeneral.inf.ed.ac.uk)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
     6
Includes support for PGIP control language for Isabelle/Isar.
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
     7
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
     8
===========================================================================
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
     9
NOTE: With this version you will lose support for the Isabelle
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    10
preferences menu in the currently released version of Proof General (3.5).
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    11
No other changes should be visible in the Emacs interface.
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    12
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    13
If the loss of preferences is a serious problem, please use a "sticky"
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    14
check-out of the previous version of this file, version 1.27.
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    15
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    16
A version of Proof General which supports the new PGIP format for
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    17
preferences will be available shortly.  
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    18
===========================================================================
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    19
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    20
STATUS: this version is an interim experimental version that was
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    21
used from 07.2003-08.2004 for the development of PGIP 1.X.  This will
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    22
soon be replaced by a version for PGIP 2.X.
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    23
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    24
*)
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    25
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    26
signature PROOF_GENERAL =
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    27
sig
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    28
  val setup: (theory -> theory) list
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    29
  val update_thy_only: string -> unit
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    30
  val try_update_thy_only: string -> unit
13391
553e7b62680f fixed inform_file_retracted: remove_thy;
wenzelm
parents: 13284
diff changeset
    31
  val inform_file_retracted: string -> unit
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    32
  val inform_file_processed: string -> unit
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    33
  val preferences: 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    34
      (string * 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    35
	(string * 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    36
	 (string * 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    37
	  (string * (string * (unit -> string)) * 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    38
	   (string -> unit)))) list) list ref
13728
8004e56204fd Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents: 13646
diff changeset
    39
  val process_pgip: string -> unit
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    40
  val thms_containing: string list -> unit
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    41
  val help: unit -> unit
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    42
  val show_context: unit -> theory
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    43
  val kill_goal: unit -> unit
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    44
  val repeat_undo: int -> unit
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    45
  val isa_restart: unit -> unit
12833
9f3226cfe021 full_proofs;
wenzelm
parents: 12780
diff changeset
    46
  val full_proofs: bool -> unit
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    47
  val isarcmd: string -> unit
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    48
  val init: bool -> unit
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    49
  val init_pgip: bool -> unit
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    50
  val write_keywords: string -> unit
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    51
end;
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    52
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    53
structure ProofGeneral : PROOF_GENERAL =
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    54
struct
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    55
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    56
(* PGIP messaging mode (independent of PGML output) *)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    57
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    58
val pgip_active = ref false;
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    59
val pgip_emacs_compatibility_flag = ref false;
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    60
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    61
fun pgip () = (!pgip_active);
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    62
fun pgip_emacs_compatibility () = (!pgip_emacs_compatibility_flag);
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    63
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    64
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    65
(* print modes *)
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    66
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    67
val proof_generalN = "ProofGeneral"; (* token markup (colouring vars, etc.) *)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    68
val xsymbolsN = Symbol.xsymbolsN;    (* XSymbols symbols *)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    69
val pgmlN = "PGML";		     (* XML escapes and PGML symbol elements *)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    70
val pgmlatomsN = "PGMLatoms";	     (* variable kind decorations *)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    71
val thm_depsN = "thm_deps";	     (* meta-information about theorem deps *)
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    72
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    73
fun pgml () = pgmlN mem_string ! print_mode;
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    74
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    75
(* text output: print modes for xsymbol and PGML *)
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    76
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    77
local
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    78
14827
d973e7f820cb Output.add_mode; Output.timing;
wenzelm
parents: 14725
diff changeset
    79
fun xsym_output "\\" = "\\\\"
d973e7f820cb Output.add_mode; Output.timing;
wenzelm
parents: 14725
diff changeset
    80
  | xsym_output s = if Symbol.is_raw s then Symbol.decode_raw s else s;
d973e7f820cb Output.add_mode; Output.timing;
wenzelm
parents: 14725
diff changeset
    81
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    82
fun xsymbols_output s =
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    83
  if xsymbolsN mem_string ! print_mode andalso exists_string (equal "\\") s then
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    84
    let val syms = Symbol.explode s
14827
d973e7f820cb Output.add_mode; Output.timing;
wenzelm
parents: 14725
diff changeset
    85
    in (implode (map xsym_output syms), real (Symbol.length syms)) end
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    86
  else Symbol.default_output s;
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    87
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    88
fun pgml_sym s =
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    89
  (case Symbol.decode s of
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    90
    Symbol.Char "\\" => "\\\\"
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    91
  | Symbol.Char s => XML.text s
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    92
  | Symbol.Sym s => XML.element "sym" [("name", s)] []
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    93
  | Symbol.Ctrl s => XML.element "ctrl" [("name", s)] []
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    94
  | Symbol.Raw s => s);
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    95
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    96
fun pgml_output str =
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    97
  let val syms = Symbol.explode str
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    98
  in (implode (map pgml_sym syms), real (Symbol.length syms)) end;
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    99
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   100
in 
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   101
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   102
fun setup_xsymbols_output () = 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   103
    Output.add_mode 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   104
	xsymbolsN 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   105
	(xsymbols_output, Symbol.default_indent, Symbol.encode_raw);
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   106
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   107
fun setup_pgml_output () = 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   108
    Output.add_mode 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   109
	pgmlN
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   110
	(pgml_output, Symbol.default_indent, Symbol.encode_raw);
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   111
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   112
end;
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   113
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   114
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   115
(* token translations *)
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   116
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   117
local
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   118
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   119
val end_tag = oct_char "350";
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   120
val class_tag = ("class", oct_char "351");
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   121
val tfree_tag = ("tfree", oct_char "352");
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   122
val tvar_tag = ("tvar", oct_char "353");
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   123
val free_tag = ("free", oct_char "354");
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   124
val bound_tag = ("bound", oct_char "355");
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   125
val var_tag = ("var", oct_char "356");
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   126
val skolem_tag = ("skolem", oct_char "357");
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   127
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   128
fun xml_atom kind x = XML.element "atom" [("kind", kind)] [XML.text x];
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   129
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   130
fun tagit (kind, bg_tag) x =
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   131
    (if Output.has_mode pgmlatomsN then 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   132
	 xml_atom kind x
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   133
     else bg_tag ^ x ^ end_tag, 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   134
     real (Symbol.length (Symbol.explode x)));
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   135
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   136
fun free_or_skolem x =
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   137
  (case try Syntax.dest_skolem x of
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   138
    None => tagit free_tag x
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   139
  | Some x' => tagit skolem_tag x');
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   140
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   141
fun var_or_skolem s =
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   142
  (case Syntax.read_var s of
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   143
    Var ((x, i), _) =>
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   144
      (case try Syntax.dest_skolem x of
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   145
        None => tagit var_tag s
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   146
      | Some x' => tagit skolem_tag (Syntax.string_of_vname (x', i)))
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   147
  | _ => tagit var_tag s);
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   148
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   149
val proof_general_trans =
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   150
 Syntax.tokentrans_mode proof_generalN
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   151
  [("class", tagit class_tag),
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   152
   ("tfree", tagit tfree_tag),
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   153
   ("tvar", tagit tvar_tag),
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   154
   ("free", free_or_skolem),
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   155
   ("bound", tagit bound_tag),
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   156
   ("var", var_or_skolem)];
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   157
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   158
in val setup = [Theory.add_tokentrfuns proof_general_trans] end;
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   159
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   160
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   161
(* assembling PGIP packets *)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   162
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   163
val pgip_refseq = ref None : string option ref
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   164
val pgip_refid = ref None : string option ref
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   165
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   166
local
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   167
    val myseq_no = ref 1;      (* PGIP packet counter *)
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   168
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   169
    val pgip_class  = "pg"
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   170
    val pgip_origin = "Isabelle/Isar"
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   171
    val pgip_id = (getenv "HOSTNAME") ^ "/" ^ (getenv "USER") ^ "/" ^ 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   172
		   (Time.toString(Time.now()))
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   173
	          (* FIXME: PPID is empty for me: any way to get process ID? *)
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   174
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   175
    fun assemble_pgips pgips = 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   176
	XML.element 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   177
	     "pgip" 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   178
	     ([("class",  pgip_class),
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   179
	       ("origin", pgip_origin),
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   180
	       ("id",     pgip_id)] @
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   181
	      (if_none (apsome (single o (pair "refseq")) (!pgip_refseq)) []) @
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   182
	      (if_none (apsome (single o (pair "refid")) (!pgip_refid)) []) @
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   183
	      [("seq",  string_of_int (Library.inc myseq_no))])
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   184
	     pgips
13526
9269275e5da6 result dependency output;
wenzelm
parents: 13391
diff changeset
   185
in
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   186
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   187
 fun decorated_output bg en prfx = 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   188
    writeln_default o enclose bg en o prefix_lines prfx;
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   189
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   190
 (* FIXME: see Rev 1.48 [PG CVS] for cleaner version of this which can be used
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   191
    for PG 4.0 which processes PGIP without needing special chars. *)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   192
 fun issue_pgips ps = 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   193
     if pgip_emacs_compatibility() then
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   194
	 decorated_output (* add urgent message annotation *)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   195
	     (oct_char "360") (oct_char "361") "" 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   196
	     (assemble_pgips ps)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   197
     else 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   198
	 writeln_default (assemble_pgips ps)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   199
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   200
 fun assemble_pgip resp attrs s = assemble_pgips [XML.element resp attrs [s]]
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   201
				  
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   202
 fun assemble_pgipe resp attrs = assemble_pgips [XML.element resp attrs []]
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   203
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   204
 fun issue_pgip resp attrs = writeln_default o (assemble_pgip resp attrs)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   205
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   206
(*  FIXME: temporarily to support PG 3.4.  *)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   207
 fun issue_pgip_maybe_decorated bg en resp attrs s = 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   208
     if pgip_emacs_compatibility() then
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   209
      (*  in PGIP mode, but using escape characters as well.  *)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   210
	writeln_default (enclose bg en (assemble_pgip resp attrs s))
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   211
     else 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   212
	issue_pgip resp attrs s
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   213
	
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   214
 fun issue_pgipe resp attrs = writeln_default (assemble_pgipe resp attrs)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   215
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   216
end
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   217
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   218
(* messages and notification *)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   219
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   220
fun message resp attrs bg en prfx s =
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   221
  if pgip() then 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   222
      issue_pgip_maybe_decorated bg en resp attrs (prefix_lines prfx s)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   223
  else 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   224
      decorated_output bg en prfx s;
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   225
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   226
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   227
local
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   228
    val display_area = ("area", "display")
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   229
    val message_area = ("area", "message")
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   230
    val tracing_category = ("category", "tracing")
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   231
    val urgent_indication = ("urgent", "y")
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   232
    val nonfatal = ("fatality", "nonfatal")
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   233
    val fatal = ("fatality", "fatal")
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   234
    val panic = ("fatality", "panic")
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   235
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   236
    val thyname_attr = pair "thyname"
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   237
    val url_attr = pair "url"
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   238
    fun localfile_url_attr path = url_attr ("file:///" ^ path)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   239
in			   
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   240
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   241
fun setup_messages () =
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   242
 (writeln_fn  := message "normalresponse" [message_area] "" "" "";
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   243
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   244
  priority_fn := message "normalresponse" [message_area, urgent_indication]
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   245
			 (oct_char "360") (oct_char "361") "";
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   246
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   247
  tracing_fn := message "normalresponse"  [message_area, tracing_category]
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   248
			(oct_char "360" ^ oct_char "375") (oct_char "361") "";
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   249
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   250
  warning_fn := message "errorresponse"    [nonfatal]
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   251
			(oct_char "362") (oct_char "363") "### ";
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   252
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   253
  error_fn := message "errorresponse" [fatal]
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   254
		      (oct_char "364") (oct_char "365") "*** ";
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   255
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   256
  panic_fn := message "errorresponse" [panic]
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   257
		      (oct_char "364") (oct_char "365") "!!! ")
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   258
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   259
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   260
(* accumulate printed output in a single PGIP response *)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   261
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   262
fun with_displaywrap (elt,attrs) dispfn =
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   263
    let 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   264
	val lines = ref ([] : string list);
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   265
	fun wlgrablines s = (lines:= (s :: (!lines)))
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   266
    in 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   267
	(setmp writeln_fn wlgrablines dispfn ();
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   268
	 (* FIXME: cat_lines here inefficient, should use stream output *)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   269
         issue_pgip elt attrs (cat_lines (!lines)))
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   270
    end
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   271
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   272
val emacs_notify = decorated_output (oct_char "360") (oct_char "361") "";
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   273
    
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   274
fun tell_clear_goals () = 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   275
    if pgip() then
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   276
	issue_pgipe "cleardisplay" [display_area]
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   277
    else 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   278
	emacs_notify "Proof General, please clear the goals buffer.";
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   279
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   280
fun tell_clear_response () = 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   281
    if pgip() then
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   282
	issue_pgipe "cleardisplay" [message_area]
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   283
    else 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   284
	emacs_notify "Proof General, please clear the response buffer.";
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   285
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   286
fun tell_file_loaded path = 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   287
    if pgip() then
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   288
	issue_pgipe "informtheoryloaded"  (* FIXME: get thy name from info here? *)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   289
		    [thyname_attr        (XML.text (File.sysify_path path)),
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   290
		     localfile_url_attr  (XML.text (File.sysify_path path))]
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   291
    else 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   292
	emacs_notify ("Proof General, this file is loaded: " 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   293
		      ^ quote (File.sysify_path path));
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   294
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   295
fun tell_file_retracted path = 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   296
    if pgip() then
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   297
	issue_pgipe "informtheoryretracted"  (* FIXME: get thy name from info here? *)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   298
		    [thyname_attr        (XML.text (File.sysify_path path)),
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   299
		     localfile_url_attr  (XML.text (File.sysify_path path))]
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   300
    else 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   301
	emacs_notify ("Proof General, you can unlock the file " 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   302
		      ^ quote (File.sysify_path path));
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   303
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   304
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   305
(* theory / proof state output *)
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   306
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   307
local
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   308
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   309
    fun tmp_markers f =	setmp Display.current_goals_markers 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   310
			      (oct_char "366", oct_char "367", "") f ()
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   311
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   312
    fun statedisplay prts =
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   313
	issue_pgip "proofstate" []
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   314
		   (XML.element "pgml" []
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   315
				[XML.element "statedisplay" 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   316
					     [] 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   317
					     [Output.output (* FIXME: needed? *)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   318
						  (Pretty.output
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   319
						       (Pretty.chunks prts))]])
13545
fcdbd6cf5f9f improved tell_thm_deps;
wenzelm
parents: 13538
diff changeset
   320
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   321
    fun print_current_goals n m st =
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   322
	if pgml () then statedisplay (Display.pretty_current_goals n m st)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   323
	else tmp_markers (fn () => Display.print_current_goals_default n m st)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   324
	     
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   325
    fun print_state b st =
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   326
	if pgml () then statedisplay (Toplevel.pretty_state b st)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   327
	else tmp_markers (fn () => Toplevel.print_state_default b st)
13526
9269275e5da6 result dependency output;
wenzelm
parents: 13391
diff changeset
   328
in
9269275e5da6 result dependency output;
wenzelm
parents: 13391
diff changeset
   329
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   330
 fun setup_state () =
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   331
     (Display.print_current_goals_fn := print_current_goals;
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   332
      Toplevel.print_state_fn := print_state;
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   333
      (* FIXME: check next octal char won't appear in pgip? *)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   334
      Toplevel.prompt_state_fn := (suffix (oct_char "372") o  
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   335
				   Toplevel.prompt_state_default));
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   336
end
13728
8004e56204fd Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents: 13646
diff changeset
   337
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   338
end
13728
8004e56204fd Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents: 13646
diff changeset
   339
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   340
(* misc commands for ProofGeneral/isa *)
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   341
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   342
fun thms_containing ss =
13284
20c818c966e6 thms_containing: optional limit argument;
wenzelm
parents: 13273
diff changeset
   343
  ProofContext.print_thms_containing (ProofContext.init (the_context ())) None ss;
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   344
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   345
val welcome = priority o Session.welcome;
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   346
val help = welcome;
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   347
val show_context = Context.the_context;
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   348
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   349
fun kill_goal () = (Goals.reset_goals (); tell_clear_goals ());
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   350
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   351
fun no_print_goals f = setmp Display.print_current_goals_fn (fn _ => fn _ => fn _ => ()) f;
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   352
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   353
fun repeat_undo 0 = ()
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   354
  | repeat_undo 1 = undo ()
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   355
  | repeat_undo n = (no_print_goals undo (); repeat_undo (n - 1));
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   356
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   357
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   358
(* theory loader actions *)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   359
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   360
local
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   361
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   362
fun add_master_files name files =
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   363
  let val masters = [ThyLoad.thy_path name, ThyLoad.ml_path name]
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   364
  in masters @ gen_rems (op = o pairself Path.base) (files, masters) end;
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   365
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   366
fun trace_action action name =
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   367
  if action = ThyInfo.Update then
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   368
    seq tell_file_loaded (ThyInfo.loaded_files name)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   369
  else if action = ThyInfo.Outdate orelse action = ThyInfo.Remove then
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   370
    seq tell_file_retracted (add_master_files name (ThyInfo.loaded_files name))
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   371
  else ();
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   372
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   373
in
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   374
  fun setup_thy_loader () = ThyInfo.add_hook trace_action;
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   375
  fun sync_thy_loader () = seq (trace_action ThyInfo.Update) (ThyInfo.names ());
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   376
end;
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   377
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   378
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   379
(* prepare theory context *)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   380
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   381
val thy_name = Path.pack o #1 o Path.split_ext o Path.base o Path.unpack;
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   382
val update_thy_only = setmp MetaSimplifier.trace_simp 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   383
			    false ThyInfo.update_thy_only;
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   384
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   385
fun which_context () =
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   386
  (case Context.get_context () of
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   387
    Some thy => "  Using current (dynamic!) one: " ^
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   388
      (case try PureThy.get_name thy of Some name => quote name | None => "<unnamed>")
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   389
  | None => "");
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   390
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   391
fun try_update_thy_only file =
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   392
  ThyLoad.cond_add_path (Path.dir (Path.unpack file)) (fn () =>
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   393
    let val name = thy_name file in
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   394
      if is_some (ThyLoad.check_file (ThyLoad.thy_path name)) 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   395
      then update_thy_only name
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   396
      else warning ("Unkown theory context of ML file." ^ which_context ())
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   397
    end) ();
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   398
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   399
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   400
(* get informed about files *)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   401
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   402
val inform_file_retracted = 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   403
    ThyInfo.if_known_thy ThyInfo.remove_thy o thy_name;
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   404
val inform_file_processed = 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   405
    ThyInfo.if_known_thy ThyInfo.touch_child_thys o thy_name;
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   406
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   407
fun proper_inform_file_processed file state =
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   408
  let val name = thy_name file in
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   409
    if Toplevel.is_toplevel state andalso ThyInfo.known_thy name then
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   410
     (ThyInfo.touch_child_thys name;
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   411
      transform_error ThyInfo.pretend_use_thy_only name handle ERROR_MESSAGE msg =>
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   412
       (warning msg; warning ("Failed to register theory: " ^ quote name);
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   413
        tell_file_retracted (Path.base (Path.unpack file))))
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   414
    else raise Toplevel.UNDEF
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   415
  end;
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   416
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   417
fun vacuous_inform_file_processed file state =
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   418
 (warning ("No theory " ^ quote (thy_name file));
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   419
  tell_file_retracted (Path.base (Path.unpack file)));
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   420
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   421
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   422
(* restart top-level loop (keeps most state information) *)
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   423
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   424
local
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   425
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   426
fun restart isar =
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   427
 (if isar then tell_clear_goals () else kill_goal ();
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   428
  tell_clear_response ();
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   429
  welcome ());
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   430
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   431
in
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   432
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   433
fun isa_restart () = restart false;
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   434
fun isar_restart () = (sync_thy_loader (); restart true; raise Toplevel.RESTART);
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   435
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   436
end;
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   437
12833
9f3226cfe021 full_proofs;
wenzelm
parents: 12780
diff changeset
   438
fun full_proofs true = proofs := 2
9f3226cfe021 full_proofs;
wenzelm
parents: 12780
diff changeset
   439
  | full_proofs false = proofs := 1;
9f3226cfe021 full_proofs;
wenzelm
parents: 12780
diff changeset
   440
9f3226cfe021 full_proofs;
wenzelm
parents: 12780
diff changeset
   441
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   442
(* theorem dependency output *)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   443
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   444
local
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   445
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   446
val spaces_quote = space_implode " " o map quote;
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   447
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   448
fun thm_deps_message (thms, deps) = 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   449
    if pgip() then
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   450
	issue_pgips 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   451
	    [XML.element
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   452
		 "metainforesponse"  (* FIXME: get thy name from info here? *)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   453
		 [("infotype", "isabelle_theorem_dependencies")]
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   454
		 [XML.element "value" [("name", "thms")] [XML.text thms],
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   455
		  XML.element "value" [("name", "deps")] [XML.text deps]]]
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   456
    else emacs_notify 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   457
	     ("Proof General, theorem dependencies of " 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   458
	      ^ thms ^ " are " ^ deps)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   459
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   460
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   461
fun tell_thm_deps ths =
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   462
  conditional (thm_depsN mem_string ! print_mode) (fn () =>
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   463
    let
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   464
      val names = map Thm.name_of_thm ths \ "";
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   465
      val deps = Symtab.keys (foldl (uncurry Proofterm.thms_of_proof)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   466
				    (Symtab.empty, map Thm.proof_of ths)) \ "";
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   467
    in
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   468
      if null names orelse null deps then ()
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   469
      else thm_deps_message (spaces_quote names, spaces_quote deps)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   470
    end);
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   471
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   472
in
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   473
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   474
fun setup_present_hook () =
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   475
  Present.add_hook (fn _ => fn res => tell_thm_deps (flat (map #2 res)));
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   476
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   477
end;
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   478
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   479
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   480
(*** Preferences ***)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   481
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   482
local
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   483
val pgipnat        = XML.element "pgipint" [("min", "0")] [] 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   484
fun pgipnatmax max = XML.element "pgipint" [("min", "0"), 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   485
					    ("max", string_of_int max)] []
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   486
val pgipbool       = XML.element "pgipbool" [] []
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   487
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   488
fun withdefault f = (f(), f)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   489
in
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   490
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   491
fun nat_option r = (pgipnat,
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   492
  withdefault (fn () => string_of_int (!r)),
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   493
  (fn s => (case Syntax.read_nat s of
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   494
       None => error "nat_option: illegal value"
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   495
     | Some i => r := i)));
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   496
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   497
fun bool_option r = (pgipbool,
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   498
  withdefault (fn () => Bool.toString (!r)),
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   499
  (fn "false" => r := false | "true" => r := true
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   500
    | _ => error "bool_option: illegal value"));
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   501
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   502
val proof_option = (pgipbool,
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   503
  withdefault (fn () => Bool.toString (!proofs >= 2)),
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   504
  (fn "false" => proofs := 1 | "true" => proofs := 2
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   505
    | _ => error "proof_option: illegal value"));
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   506
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   507
val thm_deps_option = (pgipbool,
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   508
  withdefault (fn () => Bool.toString (Output.has_mode "thm_deps")),
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   509
  (fn "false" => print_mode := ((!print_mode) \ "thm_deps")
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   510
    | "true" => print_mode := ("thm_deps" ins (!print_mode))
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   511
    | _ => error "thm_deps_option: illegal value"));
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   512
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   513
local 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   514
    val pg_print_depth_val = ref 10
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   515
    fun pg_print_depth n = (print_depth n; pg_print_depth_val := n)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   516
in
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   517
val print_depth_option = (pgipnat,
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   518
  withdefault (fn () => string_of_int (!pg_print_depth_val)),
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   519
  (fn s => (case Syntax.read_nat s of
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   520
       None => error "print_depth_option: illegal value"
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   521
     | Some i => pg_print_depth i)))
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   522
end
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   523
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   524
val preferences = ref 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   525
  [("Display",
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   526
    [("show-types", 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   527
      ("Include types in display of Isabelle terms", 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   528
       bool_option show_types)),
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   529
     ("show-sorts", 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   530
      ("Include sorts in display of Isabelle terms", 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   531
       bool_option show_sorts)),
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   532
     ("show-consts", 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   533
      ("Show types of consts in Isabelle goal display",
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   534
       bool_option show_consts)),
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   535
     ("long-names", 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   536
      ("Show fully qualified names in Isabelle terms", bool_option long_names)),
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   537
     ("show-brackets", 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   538
      ("Show full bracketing in Isabelle terms",
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   539
       bool_option show_brackets)),
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   540
     ("show-main-goal", 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   541
      ("Show main goal in proof state display", bool_option Proof.show_main_goal)),
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   542
     ("eta-contract", 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   543
      ("Print terms eta-contracted",
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   544
       bool_option Syntax.eta_contract))]),
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   545
   ("Advanced Display",
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   546
    [("goals-limit", 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   547
      ("Setting for maximum number of goals printed",
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   548
       nat_option goals_limit)),
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   549
     ("prems-limit", 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   550
      ("Setting for maximum number of premises printed",
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   551
       nat_option ProofContext.prems_limit)),
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   552
     ("print-depth", 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   553
      ("Setting for the ML print depth",
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   554
       print_depth_option))]),
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   555
   ("Tracing",
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   556
    [("trace-simplifier", 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   557
      ("Trace simplification rules.",
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   558
       bool_option trace_simp)),
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   559
     ("trace-rules", ("Trace application of the standard rules",
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   560
		      bool_option trace_rules)),
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   561
     ("trace-unification", 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   562
      ("Output error diagnostics during unification",
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   563
       bool_option Pattern.trace_unify_fail)),
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   564
     ("global-timing", 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   565
      ("Whether to enable timing in Isabelle.",
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   566
       bool_option Output.timing))]),
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   567
   ("Proof", 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   568
    [("quick-and-dirty", 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   569
      ("Take a few (interactive-only) short cuts",
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   570
       bool_option quick_and_dirty)),
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   571
     ("full-proofs", 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   572
      ("Record full proof objects internally",
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   573
       proof_option)),
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   574
     ("theorem-dependencies", 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   575
       ("Track theorem dependencies within Proof General",
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   576
	thm_deps_option))])
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   577
   ];
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   578
end
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   579
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   580
(* Configuration: GUI config, proverinfo messages *)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   581
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   582
local
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   583
    val config_file = "~~/lib/ProofGeneral/pgip_isar.xml"
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   584
    val name_attr = pair "name"
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   585
    val version_attr = pair "version"
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   586
    val isabelle_www = "http://isabelle.in.tum.de/"
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   587
in
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   588
fun send_pgip_config () =
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   589
    let 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   590
	val path = Path.unpack config_file
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   591
	val exists = File.exists path
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   592
	val proverinfo = 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   593
	    XML.element "proverinfo"
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   594
              [("name",Session.name()), ("version", version),
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   595
	       ("url", isabelle_www)]
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   596
	    [XML.element "welcomemsg" [] [XML.text (Session.welcome())],
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   597
	     XML.element "helpdoc" 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   598
         (* NB: would be nice to generate/display docs from isatool
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   599
          doc, but that program may not be running on same machine;
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   600
          front end should be responsible for launching viewer, etc. *)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   601
		      [("name", "Isabelle/HOL Tutorial"),
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   602
		       ("descr", "A Gentle Introduction to Isabelle/HOL"), 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   603
		       ("url",  "http://isabelle.in.tum.de/dist/Isabelle2003/doc/tutorial.pdf")]
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   604
	      []]
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   605
    in
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   606
	if exists then
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   607
	    (issue_pgips [proverinfo]; issue_pgips [File.read path])
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   608
	else panic ("PGIP configuration file " ^ config_file ^ " not found")
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   609
    end;
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   610
end
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   611
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   612
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   613
(* PGIP identifier tables (prover objects). [incomplete] *)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   614
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   615
local
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   616
    val objtype_thy  = "theory"
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   617
    val objtype_thm  = "theorem"
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   618
    val objtype_term = "term"
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   619
    val objtype_type = "type"
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   620
		       
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   621
    fun xml_idtable ty ctx ids = 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   622
	let
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   623
            fun ctx_attr (Some c)= [("context", c)]
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   624
              | ctx_attr None    = []
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   625
	    fun xmlid x = XML.element "identifier" [] [XML.text x];
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   626
	in 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   627
	    XML.element "idtable" (("objtype", ty)::ctx_attr ctx)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   628
	                          (map xmlid ids)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   629
	end
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   630
in
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   631
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   632
fun setids t = issue_pgip "setids" [] t
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   633
fun addids t = issue_pgip "addids" [] t
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   634
fun delids t = issue_pgip "delids" [] t
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   635
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   636
fun delallids ty = setids (xml_idtable ty None [])
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   637
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   638
fun send_thy_idtable ctx thys = setids (xml_idtable objtype_thy ctx thys)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   639
fun clear_thy_idtable () = delallids objtype_thy
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   640
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   641
fun send_thm_idtable ctx thy = 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   642
    addids (xml_idtable objtype_thm ctx (map fst (PureThy.thms_of thy)));
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   643
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   644
fun clear_thm_idtable () = delallids objtype_thm
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   645
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   646
(* fun send_type_idtable thy = TODO, it's a bit low-level messy
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   647
   & maybe not so useful anyway *)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   648
	
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   649
end
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   650
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   651
(* Response to interface queries about known objects *)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   652
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   653
local
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   654
 val topthy = Toplevel.theory_of o Toplevel.get_state
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   655
 val pthm = print_thm oo get_thm
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   656
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   657
 fun idvalue tp nm = ("idvalue",[("objtype",tp),("name",nm)])
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   658
in
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   659
fun askids (None, Some "theory")  = send_thy_idtable None (ThyInfo.names())
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   660
  | askids (None, None) =  send_thy_idtable None (ThyInfo.names())
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   661
                           (* only theories known in top context *)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   662
  | askids (Some thy, Some "theory") = send_thy_idtable (Some thy) (ThyInfo.get_preds thy)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   663
  | askids (Some thy, Some "theorem") = send_thm_idtable (Some thy) (ThyInfo.get_theory thy)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   664
  | askids (Some thy, None) = (send_thy_idtable (Some thy) (ThyInfo.get_preds thy);
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   665
                               send_thm_idtable (Some thy) (ThyInfo.get_theory thy)) 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   666
(*  | askids (Some thy, "type") = send_type_idtable (Some thy) (ThyInfo.get_theory thy) *)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   667
  | askids (_, Nothing) = error "No objects of any type are available here."
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   668
  | askids (_, Some ot) = error ("No objects of type "^(quote ot)^" are available here.")
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   669
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   670
fun showid (_,        "theory", n) = 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   671
    with_displaywrap (idvalue "theory" n) (fn ()=>(print_theory (ThyInfo.get_theory n)))
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   672
  | showid (Some thy, "theorem", t) = 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   673
    with_displaywrap (idvalue "theorem" t) (fn ()=>(pthm (ThyInfo.get_theory thy) t))
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   674
  | showid (None,     "theorem", t) = 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   675
    with_displaywrap (idvalue "theorem" t) (fn ()=>pthm (topthy()) t)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   676
  | showid (_, ot, _) = error ("Cannot show objects of type "^ot)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   677
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   678
(* Return script command to set an identifier to some value *)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   679
(* TODO: support object preference setting here *)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   680
fun bindid (name, "thm", [XML.Elem ("objval",_,[XML.Text objval])]) = 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   681
    ("lemmas " ^ name ^ " = " ^ objval)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   682
  | bindid (name, ot, _) = error ("Cannot bind objects of type " ^ ot)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   683
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   684
end
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   685
	 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   686
(** Parsing proof scripts without execution **)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   687
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   688
local
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   689
    (* This is a temporary hack until we have decent parsing of proof scripts *)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   690
    fun xmle elt = XML.element elt [] []
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   691
    fun xmlc elt str = XML.element elt [] [XML.text str]
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   692
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   693
    fun make_opengoal args =
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   694
	(* For now, strictly only args like <lemma foo: "P->Q"> *)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   695
	let
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   696
	    val tstart = find_index_eq "\"" (explode args)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   697
	    val tend = find_index_eq "\"" (drop (tstart, (explode args)))
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   698
	    val nend = find_index_eq ":" (explode args)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   699
	    val uptonend = (rev (take (nend-1,explode args)))
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   700
	    val nstart = (length uptonend) - 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   701
			 (find_index (not o Symbol.is_letter) uptonend)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   702
	in 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   703
	    (XML.element 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   704
		"opengoal" 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   705
		[("thmname", String.substring(args,nstart,nend-nstart))]
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   706
		[XML.text (String.substring(args, tstart+1, tend))])
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   707
	end
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   708
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   709
    fun make_theory args =
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   710
	(* For now, strictly only args like <theory Foo=Main:> *)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   711
	let
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   712
	    val argstart = find_index_eq "=" (explode args)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   713
	    val argend = find_index_eq ":" (explode args)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   714
	    val (name1,arg1) = splitAt(argstart, explode args)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   715
	    val namecs = dropwhile (fn c => c mem [" ","\t","\n"]) (rev name1)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   716
	    val nameend = find_index (fn c=> not (Symbol.is_quasi_letter c)) namecs
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   717
	    val (namecs',_) = splitAt(nameend, namecs)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   718
	    val name = implode (rev namecs')
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   719
	    val (arg2, _) = splitAt(argend-argstart-1, tl arg1)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   720
            val arg = implode arg2
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   721
	in 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   722
	    XML.element "opentheory" [("thyname", name)] [XML.text arg]
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   723
	end
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   724
in
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   725
fun xmls_of_transition (name,toks,tr) = 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   726
   let 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   727
       val str = name ^ " " ^ (space_implode " " (map OuterLex.unparse toks))
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   728
   in
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   729
    case name of (* NB: see isar_syn.ML for names of standard commands *)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   730
         "done"       => [xmle "closegoal"]  
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   731
       | "sorry"      => [xmle "giveupgoal"]
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   732
       | "oops"       => [xmle "postponegoal"]
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   733
       | "by"         => [xmlc "proofstep" ("apply " ^ str),
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   734
			  xmle "closegoal"] (* FIXME: tactic proofs only just now *)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   735
       (* theories *)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   736
       | "theory"     => [make_theory str]
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   737
       (* goals *)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   738
       | "lemma"      => [make_opengoal str]
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   739
       | "theorem"    => [make_opengoal str]
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   740
       | "corollary"  => [make_opengoal str]
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   741
       (* literate text *)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   742
       | "text"       => [xmlc "litcomment" str]
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   743
       | "sect"       => [xmlc "litcomment" ("ion " ^ str)]
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   744
       | "subsect"    => [xmlc "litcomment" ("ion " ^ str)]
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   745
       | "subsubsect" => [xmlc "litcomment" ("ion " ^ str)]
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   746
       | "txt"	      => [xmlc "litcomment" str]
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   747
       | _ => [xmlc "proofstep" str]  (* default for anything else *)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   748
   end
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   749
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   750
(* FIXME: need to handle parse errors gracefully below, perhaps returning partial parse *)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   751
(* NB: comments are ignored by below; not good if we use this to reconstruct script *)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   752
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   753
fun xmls_of_str str =
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   754
   let fun parse_loop (nm_lex_trs,xmls) = 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   755
	   (case nm_lex_trs of
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   756
	      [] => xmls  
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   757
	    | (nm,toks,tr)::rest  => 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   758
	      let 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   759
		val xmls_tr = xmls_of_transition (nm,toks,tr)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   760
	      in  
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   761
	         parse_loop (rest, xmls @ xmls_tr)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   762
	      end)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   763
    in
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   764
	parse_loop (OuterSyntax.read str, [])
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   765
    end
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   766
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   767
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   768
fun parsescript str = 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   769
    issue_pgips [XML.element "parseresult" [] (xmls_of_str str)]
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   770
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   771
end
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   772
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   773
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   774
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   775
(**** PGIP:  Isabelle -> Interface ****)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   776
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   777
val isabelle_pgml_version_supported = "1.0"; 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   778
val isabelle_pgip_version_supported = "1.0"
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   779
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   780
fun usespgip () = 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   781
    issue_pgipe "usespgip" [("version", isabelle_pgip_version_supported)];
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   782
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   783
fun usespgml () = 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   784
    issue_pgipe "usespgml" [("version", isabelle_pgml_version_supported)];
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   785
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   786
fun hasprefs () = 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   787
    seq (fn (prefcat, prefs) =>
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   788
	    issue_pgips [XML.element "hasprefs" [("prefcategory",prefcat)]
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   789
		 (map (fn (name, (descr, (ty, (default,_),_))) => 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   790
		       XML.element "haspref" [("name", name), 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   791
					      ("descr", descr), 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   792
					      ("default", default)]
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   793
		       [ty]) prefs)]) (!preferences);
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   794
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   795
fun allprefs () = foldl (op @) ([], map snd (!preferences))
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   796
	
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   797
fun setpref name value = 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   798
    (case assoc (allprefs(), name) of
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   799
	 None => warning ("Unknown pref: " ^ quote name)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   800
       | Some (_, (_, _, set)) => set value);
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   801
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   802
fun getpref name = 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   803
    (case assoc (allprefs(), name) of
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   804
	 None => warning ("Unknown pref: " ^ quote name)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   805
       | Some (_, (_, (_,get), _)) => 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   806
	   issue_pgip "prefval" [("name", name)] (get ()));
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   807
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   808
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   809
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   810
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   811
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   812
(**** PGIP:  Interface -> Isabelle/Isar ****)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   813
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   814
exception PGIP of string;
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   815
exception PGIP_QUIT;
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   816
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   817
(* Sending commands to Isar *)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   818
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   819
(* FIXME Makarius:
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   820
   'isarcmd': consider using 'Toplevel.>>>' instead of
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   821
   'Toplevel.loop'; unsure about the exact error behaviour required here;
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   822
*)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   823
val isarcmd = Toplevel.loop o
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   824
		(OuterSyntax.isar_readstring 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   825
		    (Position.name "PGIP message")) (* FIXME: could do better *)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   826
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   827
fun isarscript s = isarcmd s   (* send a script command *)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   828
   (* was: (isarcmd s;  issue_pgip "scriptinsert" [] (XML.text s)) *)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   829
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   830
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   831
(* load an arbitrary (.thy or .ML) file *)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   832
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   833
fun use_thy_or_ml_file file = 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   834
    let
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   835
	val (path,extn) = Path.split_ext (Path.unpack file)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   836
    in
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   837
	case extn of
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   838
	    "" => isarcmd ("use_thy " ^ (quote (Path.pack path)))
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   839
	  | "thy" => isarcmd ("use_thy " ^ (quote (Path.pack path)))
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   840
	  | "ML" => isarcmd ("use " ^ quote file)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   841
	  (* instead of error we could guess theory? *)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   842
	  | other => error ("Don't know how to read a file with extension " ^ other)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   843
    end  
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   844
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   845
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   846
local
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   847
  (* Proof control commands *)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   848
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   849
  fun xmlattro attrs attr = assoc(attrs,attr)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   850
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   851
  fun xmlattr attrs attr = 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   852
      (case xmlattro attrs attr of 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   853
	   Some value => value 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   854
	 | None => raise PGIP ("Missing attribute: " ^ attr))
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   855
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   856
  fun xmltext [XML.Text text] = text
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   857
    | xmltext ((XML.Text text)::ts) = text ^ " " ^ (xmltext ts)  (* FIXME: space shouldn't be needed *)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   858
    | xmltext _ = raise PGIP "Expected text (PCDATA/CDATA)"
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   859
			
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   860
  val thyname_attr = "thyname"
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   861
  val objtype_attr = "objtype"
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   862
  val name_attr = "name"
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   863
  val dirname_attr = "dir"
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   864
  fun comment x = "(* " ^ x ^ " *)"
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   865
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   866
(* return script portion corresponding to a PGIP command.
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   867
   We only unparse proper proof commands. 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   868
   (we might unparse gui opns too, if they didn't have opcmd settings?)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   869
*)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   870
  fun unparse (elem,attrs,xmls) = 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   871
      (case elem of 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   872
         "opengoal" => "lemma " ^ (xmlattr attrs "thmname") ^ ": " ^
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   873
					  (quote (xmltext xmls))
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   874
	  (* FIXME: should maybe remove    ^^^^^^^^^^ 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   875
	     to provide for Isar's parenthetical phrases (is ...) *)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   876
       | "proofstep" => xmltext xmls
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   877
       | "closegoal" => "done"   (* FIXME: or qed? Maybe nothing? *)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   878
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   879
       | "opentheory" => ("theory " ^ (xmlattr attrs thyname_attr) ^ 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   880
					" = " ^ (xmltext xmls) ^ ":")
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   881
       | "closetheory" => "end"
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   882
       | "postponegoal" => "sorry"
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   883
       | "giveupgoal" => "oops"
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   884
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   885
       | "bindid" => (bindid (xmlattr attrs objtype_attr, 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   886
				 xmlattr attrs name_attr, 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   887
				 xmls))
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   888
       | "comment" => comment (xmltext xmls)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   889
       | "litcomment" => xmltext xmls
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   890
       | _ => error ("unparse called with improper proof command: " ^ elem))
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   891
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   892
  fun unparsecmds xmls = 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   893
      let
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   894
	  fun upc (XML.Elem elt) = (unparse elt) 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   895
	    | upc (XML.Text t) = (warning ("unprasecmds: ignoring spurious text: " ^ t); "")
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   896
      in 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   897
	  issue_pgip "unparseresult" [] 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   898
		     (XML.text (cat_lines (map upc xmls))) (* FIXME: use cdata? *)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   899
      end
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   900
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   901
  (* parse URLs like "file://host/name.thy" *)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   902
  (* FIXME: instead of this, extend code in General/url.ML & use that. *)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   903
  fun decode_url url = 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   904
      (let 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   905
	  val sep = find_index_eq ":" (explode url)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   906
 	  val proto = String.substring(url,0,sep)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   907
	  val hostsep = find_index_eq "/" (drop (sep+3,explode url))
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   908
	  val host = String.substring(url,sep+3,hostsep-sep+4)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   909
	  val doc = if (size url >= sep+hostsep+3) then
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   910
			String.substring(url,sep+hostsep+4,size url-hostsep-sep-4) 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   911
		    else ""
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   912
      in 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   913
	  (proto,host,doc)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   914
      end) handle Subscript => error ("Badly formed URL " ^ url)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   915
 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   916
  fun localfile_of_url url =
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   917
      let
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   918
	  val (proto,host,name) = decode_url url
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   919
      in
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   920
	  if (proto = "file" andalso 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   921
	      (host = "" orelse 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   922
	       host = "localhost" orelse 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   923
	       host = (getenv "HOSTNAME")))
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   924
	     then name
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   925
	  else error ("Cannot access non-local URL " ^ url)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   926
      end
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   927
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   928
  fun fileurl_of attrs = localfile_of_url (xmlattr attrs "url")
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   929
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   930
  val topthy = Toplevel.theory_of o Toplevel.get_state
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   931
  val topthy_name = PureThy.get_name o topthy
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   932
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   933
  val currently_open_file = ref (None : string option)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   934
in
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   935
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   936
fun process_pgip_element pgipxml =
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   937
    (case pgipxml of 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   938
	 (XML.Text t) => warning ("Ignored text in PGIP packet: \n" ^ t)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   939
       | (XML.Elem (xml as (elem, attrs, xmls))) => (case elem of
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   940
(* protocol config *)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   941
  "askpgip"  	   => (usespgip (); send_pgip_config ())
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   942
| "askpgml"  	   => usespgml ()
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   943
(* proverconfig *)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   944
| "askprefs" 	   => hasprefs ()
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   945
| "getpref"  	   => getpref (xmlattr attrs name_attr)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   946
| "setpref"  	   => setpref (xmlattr attrs name_attr) (xmltext xmls)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   947
(* provercontrol *)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   948
| "proverinit" 	   => isar_restart ()
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   949
| "proverexit" 	   => isarcmd "quit"
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   950
| "startquiet" 	   => isarcmd "disable_pr"
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   951
| "stopquiet"  	   => isarcmd "enable_pr"
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   952
| "pgmlsymbolson"  => (print_mode := (["xsymbols", "symbols"] @ ! print_mode))
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   953
| "pgmlsymbolsoff" => (print_mode := (Library.gen_rems 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   954
					  (op =) (! print_mode, ["xsymbols", "symbols"])))
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   955
(* provercmd: proper commands which belong in script *)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   956
| "proofstep"      => isarscript (unparse xml)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   957
| "opengoal"       => isarscript (unparse xml)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   958
| "closegoal"      => isarscript (unparse xml)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   959
| "postponegoal"   => isarscript (unparse xml)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   960
| "giveupgoal"     => isarscript (unparse xml)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   961
| "comment"	   => isarscript (unparse xml)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   962
| "litcomment"	   => isarscript (unparse xml)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   963
(* provercmd: improper commands which *do not* belong in script *)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   964
| "undostep"       => isarcmd "ProofGeneral.undo"
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   965
| "abortgoal"      => isarcmd "ProofGeneral.kill_proof"  
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   966
| "forget"         => error ("Not implemented") 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   967
| "restoregoal"    => error ("Not implemented")  (* could just treat as forget? *)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   968
(* proofctxt: improper commands *)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   969
| "askids"         => askids (xmlattro attrs thyname_attr, 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   970
		              xmlattro attrs objtype_attr)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   971
| "showid"	   => showid (xmlattro attrs thyname_attr, 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   972
		              xmlattr attrs objtype_attr,
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   973
		     	      xmlattr attrs name_attr)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   974
| "parsescript"    => parsescript (xmltext xmls)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   975
| "unparsecmds"    => unparsecmds xmls
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   976
| "showproofstate" => isarcmd "pr"
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   977
| "showctxt"       => isarcmd "print_theory" (* more useful than print_context *)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   978
| "searchtheorems" => isarcmd ("thms_containing " ^ (xmltext xmls))
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   979
| "setlinewidth"   => isarcmd ("pretty_setmargin " ^ (xmltext xmls))
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   980
(* proofctxt: proper commands *)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   981
| "bindid"         => isarscript (unparse xml)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   982
(* filecmd: proper commands *)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   983
| "opentheory"     => isarscript (unparse xml)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   984
| "closetheory"    => (isarscript (unparse xml);
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   985
		       writeln ("Theory "^(topthy_name())^" completed."))
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   986
(* filecmd: improper commands *)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   987
| "aborttheory"    => isarcmd ("init_toplevel")
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   988
| "retracttheory"  => isarcmd ("kill_thy " ^
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   989
			       (quote (xmlattr attrs thyname_attr)))
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   990
| "loadfile"       => use_thy_or_ml_file    (fileurl_of attrs)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   991
| "openfile"       => (inform_file_retracted (fileurl_of attrs);
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   992
		       currently_open_file := Some (fileurl_of attrs))
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   993
| "closefile"      => (case !currently_open_file of 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   994
			   Some f => (inform_file_processed f;
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   995
				      currently_open_file := None)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   996
			 | None => raise PGIP ("closefile when no file is open!"))
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   997
| "abortfile"      => (currently_open_file := None) (* might give error for no file open *)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   998
| "changecwd"      => ThyLoad.add_path (xmlattr attrs dirname_attr)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   999
(* unofficial command for debugging *)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1000
| "quitpgip" => raise PGIP_QUIT  
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1001
| _ => raise PGIP ("Unrecognized PGIP element: " ^ elem)))
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1002
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1003
fun process_pgip_tree s = 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1004
    (pgip_refseq := None; 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1005
     pgip_refid := None;
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1006
     (case s of
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1007
	  XML.Elem ("pgip", attrs, pgips) => 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1008
	  (let 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1009
	       val class = xmlattr attrs "class"
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1010
	       val _ = (pgip_refseq := xmlattro attrs "seq";
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1011
			pgip_refid :=  xmlattro attrs "id")
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1012
	   in  
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1013
	       if (class = "pa") then
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1014
		   seq process_pgip_element pgips
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1015
	       else 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1016
		   raise PGIP "PGIP packet for me should have class=\"pa\""
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1017
	   end)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1018
	| _ => raise PGIP "Invalid PGIP packet received") 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1019
     handle (PGIP msg) => 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1020
	    (error (msg ^ "\nPGIP error occured in XML text below:\n" ^ 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1021
		    (XML.string_of_tree s))))
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1022
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1023
(* for export to Emacs *)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1024
(* val process_pgip = process_pgip_tree o XML.tree_of_string; *)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1025
(* FIXME: for temporary compatibility with PG 3.4, we engage special characters
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1026
   during output *)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1027
fun process_pgip s = 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1028
    (pgip_emacs_compatibility_flag := true;
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1029
     process_pgip_tree (XML.tree_of_string s);
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1030
     pgip_emacs_compatibility_flag := false)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1031
end
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1032
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1033
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1034
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1035
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1036
(* PGIP loop: process PGIP input only *)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1037
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1038
local  
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1039
(* NB: simple tty for now; later might read from other sources, open sockets, etc. *)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1040
(* FIXME da: doesn't setting the stopper at a single element mean we have to
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1041
  parse the whole tree on one go anyway? *)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1042
val tty_src = Source.set_prompt ""
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1043
	      (Source.source Symbol.stopper (XML.parse_elem >> single)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1044
					None Source.tty);
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1045
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1046
(* FIXME: Makarius:
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1047
 'read_pgip()': some content may be left in the internal buffer after
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1048
 Source.get_single, which will got lost between calls; try to avoid
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1049
 building the tty source over and over again;
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1050
*)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1051
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1052
fun read_pgip () =  Source.get_single tty_src
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1053
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1054
fun loop () =
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1055
    let 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1056
	val _ = issue_pgipe "ready" []
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1057
    in
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1058
	case (read_pgip()) of  
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1059
	     None  => ()
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1060
	   | Some (pgip,_) =>  (process_pgip_tree pgip; loop()) handle e => handler e
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1061
    end handle e => handler e
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1062
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1063
and handler e = 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1064
    case e of
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1065
        PGIP_QUIT => ()
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1066
      | ERROR => loop() (* message already given *)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1067
      | Interrupt => (error "Interrupt during PGIP processing"; loop())
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1068
      | Toplevel.UNDEF => (error "No working context defined"; loop()) (* usually *)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1069
      | e => (error (Toplevel.exn_message e); loop())
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1070
      (* Also seen: Scan.FAIL (not exported from Scan -- needs catching in xml.ML) *)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1071
in
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1072
   val pgip_toplevel =  loop
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1073
end
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1074
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1075
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1076
(* additional outer syntax for Isar *)
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1077
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1078
local structure P = OuterParse and K = OuterSyntax.Keyword in
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1079
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1080
val undoP = (* undo without output *)
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1081
  OuterSyntax.improper_command "ProofGeneral.undo" "(internal)" K.control
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1082
    (Scan.succeed (Toplevel.no_timing o IsarCmd.undo));
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1083
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1084
val context_thy_onlyP =
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1085
  OuterSyntax.improper_command "ProofGeneral.context_thy_only" "(internal)" K.control
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1086
    (P.name >> (Toplevel.no_timing oo IsarThy.init_context update_thy_only));
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1087
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1088
val try_context_thy_onlyP =
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1089
  OuterSyntax.improper_command "ProofGeneral.try_context_thy_only" "(internal)" K.control
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1090
    (P.name >> (Toplevel.no_timing oo
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1091
      (Toplevel.imperative (K ()) oo IsarThy.init_context try_update_thy_only)));
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1092
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1093
val restartP =
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1094
  OuterSyntax.improper_command "ProofGeneral.restart" "(internal)" K.control
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1095
    (P.opt_unit >> (Toplevel.no_timing oo K (Toplevel.imperative isar_restart)));
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1096
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1097
val kill_proofP =
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1098
  OuterSyntax.improper_command "ProofGeneral.kill_proof" "(internal)" K.control
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1099
    (Scan.succeed (Toplevel.no_timing o IsarCmd.kill_proof_notify tell_clear_goals));
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1100
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1101
val inform_file_processedP =
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1102
  OuterSyntax.improper_command "ProofGeneral.inform_file_processed" "(internal)" K.control
14902
bef0dc694c48 Path.split_ext; more robust inform_file_processed;
wenzelm
parents: 14880
diff changeset
  1103
    (P.name >> (fn file => Toplevel.no_timing o
bef0dc694c48 Path.split_ext; more robust inform_file_processed;
wenzelm
parents: 14880
diff changeset
  1104
      Toplevel.keep (vacuous_inform_file_processed file) o
bef0dc694c48 Path.split_ext; more robust inform_file_processed;
wenzelm
parents: 14880
diff changeset
  1105
      Toplevel.kill o
bef0dc694c48 Path.split_ext; more robust inform_file_processed;
wenzelm
parents: 14880
diff changeset
  1106
      Toplevel.keep (proper_inform_file_processed file)));
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1107
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1108
val inform_file_retractedP =
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1109
  OuterSyntax.improper_command "ProofGeneral.inform_file_retracted" "(internal)" K.control
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1110
    (P.name >> (Toplevel.no_timing oo
14902
bef0dc694c48 Path.split_ext; more robust inform_file_processed;
wenzelm
parents: 14880
diff changeset
  1111
      (fn file => Toplevel.imperative (fn () => inform_file_retracted file))));
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1112
14725
2ed5b960c6b1 ProofGeneral.process_pgip command;
wenzelm
parents: 14707
diff changeset
  1113
val process_pgipP =
2ed5b960c6b1 ProofGeneral.process_pgip command;
wenzelm
parents: 14707
diff changeset
  1114
  OuterSyntax.improper_command "ProofGeneral.process_pgip" "(internal)" K.control
2ed5b960c6b1 ProofGeneral.process_pgip command;
wenzelm
parents: 14707
diff changeset
  1115
    (P.text >> (Toplevel.no_timing oo
2ed5b960c6b1 ProofGeneral.process_pgip command;
wenzelm
parents: 14707
diff changeset
  1116
      (fn txt => Toplevel.imperative (fn () => process_pgip txt))));
2ed5b960c6b1 ProofGeneral.process_pgip command;
wenzelm
parents: 14707
diff changeset
  1117
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1118
fun init_outer_syntax () = OuterSyntax.add_parsers
14675
08b9c690f9cf removed obsolete 'undo';
wenzelm
parents: 14568
diff changeset
  1119
 [undoP, restartP, kill_proofP, context_thy_onlyP, try_context_thy_onlyP,
14725
2ed5b960c6b1 ProofGeneral.process_pgip command;
wenzelm
parents: 14707
diff changeset
  1120
  inform_file_processedP, inform_file_retractedP, process_pgipP];
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1121
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1122
end;
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1123
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1124
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1125
(* init *)
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1126
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1127
val initialized = ref false;
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1128
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1129
fun set_prompts true _ = ml_prompts "ML> " "ML# " 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1130
  | set_prompts false true = ml_prompts "PGIP-ML>" "PGIP-ML# "
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1131
  | set_prompts false false = 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1132
    ml_prompts ("> " ^ oct_char "372") ("- " ^ oct_char "373");
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1133
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1134
fun init_setup isar pgip =
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1135
 (conditional (not (! initialized)) (fn () =>
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1136
   (if isar then setmp warning_fn (K ()) init_outer_syntax () else ();
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1137
    setup_xsymbols_output ();
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1138
    setup_pgml_output ();
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1139
    setup_messages ();
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1140
    setup_state ();
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1141
    setup_thy_loader ();
13526
9269275e5da6 result dependency output;
wenzelm
parents: 13391
diff changeset
  1142
    setup_present_hook ();
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1143
    set initialized; ()));
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1144
  sync_thy_loader ();
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1145
  print_mode := proof_generalN :: (! print_mode \ proof_generalN);
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1146
  if pgip then 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1147
      print_mode := pgmlN :: (pgmlatomsN :: (! print_mode \ pgmlN \ pgmlatomsN)) 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1148
    else ();
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1149
  set quick_and_dirty;
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1150
  ThmDeps.enable ();
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1151
  set_prompts isar pgip;
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1152
  pgip_active := pgip)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1153
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1154
fun init isar = 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1155
    (init_setup isar false;
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1156
     if isar then ((* da: this welcome is problematic: clashes with welcome
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1157
		      issued for PG anyway. 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1158
		      welcome (); *)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1159
		    Isar.sync_main ()) else isa_restart ());
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1160
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1161
fun init_pgip false = panic "Sorry, PGIP not supported for Isabelle/classic mode."
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1162
  | init_pgip true = (init_setup true true; pgip_toplevel());
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1163
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1164
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1165
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1166
(** generate keyword classification elisp file **)
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1167
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1168
local
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1169
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1170
val regexp_meta = explode ".*+?[]^$";
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1171
val regexp_quote = 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1172
    implode o map  (fn c => if c mem regexp_meta then "\\\\" ^ c else c)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1173
    o explode;
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1174
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1175
fun defconst name strs =
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1176
  "\n(defconst isar-keywords-" ^ name ^
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1177
  "\n  '(" ^ space_implode "\n    " (map (quote o regexp_quote) strs) ^ "))\n";
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1178
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1179
fun make_elisp_commands commands kind =
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1180
  defconst kind (mapfilter 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1181
		     (fn (c, _, k, _) => if k = kind then Some c else None) 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1182
		     commands);
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1183
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1184
fun make_elisp_syntax (keywords, commands) =
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1185
  ";;\n\
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1186
  \;; Keyword classification tables for Isabelle/Isar.\n\
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1187
  \;; This file was generated by " ^ Session.name () ^ " -- DO NOT EDIT!\n\
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1188
  \;;\n\
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1189
  \;; $" ^ "Id$\n\
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1190
  \;;\n" ^
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1191
  defconst "major" (map #1 commands) ^
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1192
  defconst "minor" (filter Syntax.is_identifier keywords) ^
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1193
  implode (map (make_elisp_commands commands) OuterSyntax.Keyword.kinds) ^
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1194
  "\n(provide 'isar-keywords)\n";
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1195
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1196
in
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1197
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1198
fun write_keywords s =
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1199
  (init_outer_syntax ();
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1200
    File.write (Path.unpack ("isar-keywords" ^ (if s = "" then "" else "-" ^ s) ^".el"))
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1201
      (make_elisp_syntax (OuterSyntax.dest_keywords (), 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1202
			  OuterSyntax.dest_parsers ())));
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1203
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1204
end;
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1205
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1206
end