src/Pure/proof_general.ML
author aspinall
Thu, 19 Aug 2004 00:47:15 +0200
changeset 15146 eab7de0d0a31
parent 15145 07360eef9f4f
child 15147 e1ed51e0ec0f
permissions -rw-r--r--
Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
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
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
    16
A version of Emacs Proof General which supports the new PGIP format for
15134
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
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
    20
STATUS: this version is an experimental version that supports PGIP 2.X.
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    21
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    22
*)
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    23
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    24
signature PROOF_GENERAL =
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    25
sig
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    26
  val setup: (theory -> theory) list
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    27
  val update_thy_only: string -> unit
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    28
  val try_update_thy_only: string -> unit
13391
553e7b62680f fixed inform_file_retracted: remove_thy;
wenzelm
parents: 13284
diff changeset
    29
  val inform_file_retracted: string -> unit
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    30
  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
    31
  val preferences: 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    32
      (string * 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    33
	(string * 
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 * (string * (unit -> string)) * 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    36
	   (string -> unit)))) list) list ref
13728
8004e56204fd Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents: 13646
diff changeset
    37
  val process_pgip: string -> unit
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    38
  val thms_containing: string list -> unit
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    39
  val help: unit -> unit
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    40
  val show_context: unit -> theory
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    41
  val kill_goal: unit -> unit
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    42
  val repeat_undo: int -> unit
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    43
  val isa_restart: unit -> unit
12833
9f3226cfe021 full_proofs;
wenzelm
parents: 12780
diff changeset
    44
  val full_proofs: bool -> unit
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    45
  val isarcmd: string -> unit
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    46
  val init: bool -> unit
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    47
  val init_pgip: bool -> unit
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    48
  val write_keywords: string -> unit
15146
eab7de0d0a31 Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents: 15145
diff changeset
    49
  val xmls_of_str : string -> string list (* temp for testing parser *)
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    50
end;
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    51
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    52
structure ProofGeneral : PROOF_GENERAL =
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    53
struct
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    54
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
    55
structure P = OuterParse
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
    56
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    57
(* 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
    58
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    59
val pgip_active = ref false;
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    60
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
    61
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    62
fun pgip () = (!pgip_active);
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    63
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
    64
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    65
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    66
(* print modes *)
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    67
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    68
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
    69
val xsymbolsN = Symbol.xsymbolsN;    (* XSymbols symbols *)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    70
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
    71
val pgmlatomsN = "PGMLatoms";	     (* variable kind decorations *)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    72
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
    73
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    74
fun pgml () = pgmlN mem_string ! print_mode;
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    75
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    76
(* text output: print modes for xsymbol and PGML *)
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    77
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    78
local
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    79
14827
d973e7f820cb Output.add_mode; Output.timing;
wenzelm
parents: 14725
diff changeset
    80
fun xsym_output "\\" = "\\\\"
d973e7f820cb Output.add_mode; Output.timing;
wenzelm
parents: 14725
diff changeset
    81
  | 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
    82
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    83
fun xsymbols_output s =
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    84
  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
    85
    let val syms = Symbol.explode s
14827
d973e7f820cb Output.add_mode; Output.timing;
wenzelm
parents: 14725
diff changeset
    86
    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
    87
  else Symbol.default_output s;
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    88
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    89
fun pgml_sym s =
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    90
  (case Symbol.decode s of
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    91
    Symbol.Char "\\" => "\\\\"
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    92
  | Symbol.Char s => XML.text s
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    93
  | 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
    94
  | 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
    95
  | Symbol.Raw s => s);
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    96
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    97
fun pgml_output str =
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    98
  let val syms = Symbol.explode str
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    99
  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
   100
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   101
in 
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   102
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   103
fun setup_xsymbols_output () = 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   104
    Output.add_mode 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   105
	xsymbolsN 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   106
	(xsymbols_output, Symbol.default_indent, Symbol.encode_raw);
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   107
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   108
fun setup_pgml_output () = 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   109
    Output.add_mode 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   110
	pgmlN
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   111
	(pgml_output, Symbol.default_indent, Symbol.encode_raw);
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   112
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   113
end;
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
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   116
(* token translations *)
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   117
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   118
local
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   119
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   120
val end_tag = oct_char "350";
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   121
val class_tag = ("class", oct_char "351");
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   122
val tfree_tag = ("tfree", oct_char "352");
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   123
val tvar_tag = ("tvar", oct_char "353");
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   124
val free_tag = ("free", oct_char "354");
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   125
val bound_tag = ("bound", oct_char "355");
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   126
val var_tag = ("var", oct_char "356");
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   127
val skolem_tag = ("skolem", oct_char "357");
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   128
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   129
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
   130
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   131
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
   132
    (if Output.has_mode pgmlatomsN then 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   133
	 xml_atom kind x
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   134
     else bg_tag ^ x ^ end_tag, 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   135
     real (Symbol.length (Symbol.explode x)));
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   136
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   137
fun free_or_skolem x =
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   138
  (case try Syntax.dest_skolem x of
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   139
    None => tagit free_tag x
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   140
  | Some x' => tagit skolem_tag x');
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   141
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   142
fun var_or_skolem s =
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   143
  (case Syntax.read_var s of
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   144
    Var ((x, i), _) =>
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   145
      (case try Syntax.dest_skolem x of
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   146
        None => tagit var_tag s
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   147
      | 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
   148
  | _ => tagit var_tag s);
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   149
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   150
val proof_general_trans =
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   151
 Syntax.tokentrans_mode proof_generalN
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   152
  [("class", tagit class_tag),
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   153
   ("tfree", tagit tfree_tag),
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   154
   ("tvar", tagit tvar_tag),
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   155
   ("free", free_or_skolem),
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   156
   ("bound", tagit bound_tag),
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   157
   ("var", var_or_skolem)];
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   158
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   159
in val setup = [Theory.add_tokentrfuns proof_general_trans] end;
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   160
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   161
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   162
(* assembling PGIP packets *)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   163
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   164
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
   165
val pgip_refid = ref None : string option ref
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   166
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   167
local
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   168
    val myseq_no = ref 1;      (* PGIP packet counter *)
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   169
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   170
    val pgip_class  = "pg"
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   171
    val pgip_origin = "Isabelle/Isar"
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   172
    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
   173
		   (Time.toString(Time.now()))
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   174
	          (* 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
   175
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   176
    fun assemble_pgips pgips = 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   177
	XML.element 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   178
	     "pgip" 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   179
	     ([("class",  pgip_class),
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   180
	       ("origin", pgip_origin),
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   181
	       ("id",     pgip_id)] @
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 "refseq")) (!pgip_refseq)) []) @
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   183
	      (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
   184
	      [("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
   185
	     pgips
13526
9269275e5da6 result dependency output;
wenzelm
parents: 13391
diff changeset
   186
in
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   187
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   188
 fun decorated_output bg en prfx = 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   189
    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
   190
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   191
 (* 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
   192
    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
   193
 fun issue_pgips ps = 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   194
     if pgip_emacs_compatibility() then
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   195
	 decorated_output (* add urgent message annotation *)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   196
	     (oct_char "360") (oct_char "361") "" 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   197
	     (assemble_pgips ps)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   198
     else 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   199
	 writeln_default (assemble_pgips ps)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   200
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   201
 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
   202
				  
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   203
 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
   204
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   205
 (* FIXME: need to add stuff to gather PGIPs here *)
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   206
 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
   207
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   208
(*  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
   209
 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
   210
     if pgip_emacs_compatibility() then
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   211
      (*  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
   212
	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
   213
     else 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   214
	issue_pgip resp attrs s
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
 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
   217
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   218
end
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
(* messages and notification *)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   221
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   222
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
   223
  if pgip() then 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   224
      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
   225
  else 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   226
      decorated_output bg en prfx s;
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   227
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   228
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   229
local
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   230
    val display_area = ("area", "display")
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   231
    val message_area = ("area", "message")
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   232
    val tracing_category = ("category", "tracing")
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   233
    val urgent_indication = ("urgent", "y")
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   234
    val nonfatal = ("fatality", "nonfatal")
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   235
    val fatal = ("fatality", "fatal")
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   236
    val panic = ("fatality", "panic")
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   237
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   238
    val thyname_attr = pair "thyname"
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   239
    val url_attr = pair "url"
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   240
    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
   241
in			   
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   242
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   243
fun setup_messages () =
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   244
 (writeln_fn  := message "normalresponse" [message_area] "" "" "";
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   245
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   246
  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
   247
			 (oct_char "360") (oct_char "361") "";
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   248
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   249
  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
   250
			(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
   251
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   252
  warning_fn := message "errorresponse"    [nonfatal]
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   253
			(oct_char "362") (oct_char "363") "### ";
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   254
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   255
  error_fn := message "errorresponse" [fatal]
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   256
		      (oct_char "364") (oct_char "365") "*** ";
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   257
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   258
  panic_fn := message "errorresponse" [panic]
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   259
		      (oct_char "364") (oct_char "365") "!!! ")
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   260
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
(* 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
   263
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   264
fun with_displaywrap (elt,attrs) dispfn =
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   265
    let 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   266
	val lines = ref ([] : string list);
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   267
	fun wlgrablines s = (lines:= (s :: (!lines)))
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   268
    in 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   269
	(setmp writeln_fn wlgrablines dispfn ();
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   270
	 (* 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
   271
         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
   272
    end
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   273
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   274
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
   275
    
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   276
fun tell_clear_goals () = 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   277
    if pgip() then
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   278
	issue_pgipe "cleardisplay" [display_area]
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   279
    else 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   280
	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
   281
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   282
fun tell_clear_response () = 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   283
    if pgip() then
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   284
	issue_pgipe "cleardisplay" [message_area]
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   285
    else 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   286
	emacs_notify "Proof General, please clear the response buffer.";
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   287
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   288
fun tell_file_loaded path = 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   289
    if pgip() then
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   290
	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
   291
		    [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
   292
		     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
   293
    else 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   294
	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
   295
		      ^ quote (File.sysify_path path));
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   296
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   297
fun tell_file_retracted path = 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   298
    if pgip() then
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   299
	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
   300
		    [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
   301
		     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
   302
    else 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   303
	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
   304
		      ^ quote (File.sysify_path path));
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   305
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
(* theory / proof state output *)
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   308
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   309
local
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   310
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   311
    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
   312
			      (oct_char "366", oct_char "367", "") f ()
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   313
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   314
    fun statedisplay prts =
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   315
	issue_pgip "proofstate" []
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   316
		   (XML.element "pgml" []
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   317
				[XML.element "statedisplay" 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   318
					     [] 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   319
					     [Output.output (* FIXME: needed? *)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   320
						  (Pretty.output
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   321
						       (Pretty.chunks prts))]])
13545
fcdbd6cf5f9f improved tell_thm_deps;
wenzelm
parents: 13538
diff changeset
   322
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   323
    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
   324
	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
   325
	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
   326
	     
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   327
    fun print_state b st =
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   328
	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
   329
	else tmp_markers (fn () => Toplevel.print_state_default b st)
13526
9269275e5da6 result dependency output;
wenzelm
parents: 13391
diff changeset
   330
in
9269275e5da6 result dependency output;
wenzelm
parents: 13391
diff changeset
   331
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   332
 fun setup_state () =
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   333
     (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
   334
      Toplevel.print_state_fn := print_state;
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   335
      (* 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
   336
      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
   337
				   Toplevel.prompt_state_default));
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
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   340
end
13728
8004e56204fd Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents: 13646
diff changeset
   341
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   342
(* misc commands for ProofGeneral/isa *)
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   343
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   344
fun thms_containing ss =
13284
20c818c966e6 thms_containing: optional limit argument;
wenzelm
parents: 13273
diff changeset
   345
  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
   346
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   347
val welcome = priority o Session.welcome;
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   348
val help = welcome;
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   349
val show_context = Context.the_context;
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 kill_goal () = (Goals.reset_goals (); tell_clear_goals ());
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 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
   354
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   355
fun repeat_undo 0 = ()
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   356
  | repeat_undo 1 = undo ()
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   357
  | 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
   358
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   359
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   360
(* theory loader actions *)
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
local
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   363
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   364
fun add_master_files name files =
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   365
  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
   366
  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
   367
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   368
fun trace_action action name =
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   369
  if action = ThyInfo.Update then
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   370
    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
   371
  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
   372
    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
   373
  else ();
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   374
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   375
in
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   376
  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
   377
  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
   378
end;
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   379
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
(* prepare theory context *)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   382
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   383
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
   384
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
   385
			    false ThyInfo.update_thy_only;
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   386
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   387
fun which_context () =
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   388
  (case Context.get_context () of
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   389
    Some thy => "  Using current (dynamic!) one: " ^
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   390
      (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
   391
  | None => "");
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   392
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   393
fun try_update_thy_only file =
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   394
  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
   395
    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
   396
      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
   397
      then update_thy_only name
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   398
      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
   399
    end) ();
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   400
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
(* get informed about files *)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   403
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   404
val inform_file_retracted = 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   405
    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
   406
val inform_file_processed = 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   407
    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
   408
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   409
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
   410
  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
   411
    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
   412
     (ThyInfo.touch_child_thys name;
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   413
      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
   414
       (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
   415
        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
   416
    else raise Toplevel.UNDEF
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   417
  end;
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   418
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   419
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
   420
 (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
   421
  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
   422
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   423
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   424
(* restart top-level loop (keeps most state information) *)
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
local
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   427
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   428
fun restart isar =
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   429
 (if isar then tell_clear_goals () else kill_goal ();
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   430
  tell_clear_response ();
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   431
  welcome ());
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
in
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   434
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   435
fun isa_restart () = restart false;
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   436
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
   437
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   438
end;
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   439
12833
9f3226cfe021 full_proofs;
wenzelm
parents: 12780
diff changeset
   440
fun full_proofs true = proofs := 2
9f3226cfe021 full_proofs;
wenzelm
parents: 12780
diff changeset
   441
  | full_proofs false = proofs := 1;
9f3226cfe021 full_proofs;
wenzelm
parents: 12780
diff changeset
   442
9f3226cfe021 full_proofs;
wenzelm
parents: 12780
diff changeset
   443
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   444
(* theorem dependency output *)
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
local
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
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
   449
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   450
fun thm_deps_message (thms, deps) = 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   451
    if pgip() then
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   452
	issue_pgips 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   453
	    [XML.element
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   454
		 "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
   455
		 [("infotype", "isabelle_theorem_dependencies")]
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   456
		 [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
   457
		  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
   458
    else emacs_notify 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   459
	     ("Proof General, theorem dependencies of " 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   460
	      ^ thms ^ " are " ^ deps)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   461
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   462
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   463
fun tell_thm_deps ths =
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   464
  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
   465
    let
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   466
      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
   467
      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
   468
				    (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
   469
    in
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   470
      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
   471
      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
   472
    end);
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
in
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   475
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   476
fun setup_present_hook () =
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   477
  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
   478
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   479
end;
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   480
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
(*** Preferences ***)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   483
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   484
local
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   485
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
   486
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
   487
					    ("max", string_of_int max)] []
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   488
val pgipbool       = XML.element "pgipbool" [] []
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   489
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   490
fun withdefault f = (f(), f)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   491
in
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   492
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   493
fun nat_option r = (pgipnat,
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   494
  withdefault (fn () => string_of_int (!r)),
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   495
  (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
   496
       None => error "nat_option: illegal value"
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   497
     | Some i => r := i)));
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   498
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   499
fun bool_option r = (pgipbool,
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   500
  withdefault (fn () => Bool.toString (!r)),
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   501
  (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
   502
    | _ => error "bool_option: illegal value"));
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   503
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   504
val proof_option = (pgipbool,
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   505
  withdefault (fn () => Bool.toString (!proofs >= 2)),
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   506
  (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
   507
    | _ => error "proof_option: illegal value"));
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   508
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   509
val thm_deps_option = (pgipbool,
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   510
  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
   511
  (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
   512
    | "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
   513
    | _ => error "thm_deps_option: illegal value"));
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   514
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   515
local 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   516
    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
   517
    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
   518
in
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   519
val print_depth_option = (pgipnat,
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   520
  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
   521
  (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
   522
       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
   523
     | Some i => pg_print_depth i)))
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   524
end
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   525
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   526
val preferences = ref 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   527
  [("Display",
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   528
    [("show-types", 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   529
      ("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
   530
       bool_option show_types)),
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   531
     ("show-sorts", 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   532
      ("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
   533
       bool_option show_sorts)),
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   534
     ("show-consts", 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   535
      ("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
   536
       bool_option show_consts)),
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   537
     ("long-names", 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   538
      ("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
   539
     ("show-brackets", 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   540
      ("Show full bracketing in Isabelle terms",
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   541
       bool_option show_brackets)),
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   542
     ("show-main-goal", 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   543
      ("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
   544
     ("eta-contract", 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   545
      ("Print terms eta-contracted",
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   546
       bool_option Syntax.eta_contract))]),
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   547
   ("Advanced Display",
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   548
    [("goals-limit", 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   549
      ("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
   550
       nat_option goals_limit)),
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   551
     ("prems-limit", 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   552
      ("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
   553
       nat_option ProofContext.prems_limit)),
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   554
     ("print-depth", 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   555
      ("Setting for the ML print depth",
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   556
       print_depth_option))]),
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   557
   ("Tracing",
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   558
    [("trace-simplifier", 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   559
      ("Trace simplification rules.",
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   560
       bool_option trace_simp)),
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   561
     ("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
   562
		      bool_option trace_rules)),
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   563
     ("trace-unification", 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   564
      ("Output error diagnostics during unification",
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   565
       bool_option Pattern.trace_unify_fail)),
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   566
     ("global-timing", 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   567
      ("Whether to enable timing in Isabelle.",
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   568
       bool_option Output.timing))]),
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   569
   ("Proof", 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   570
    [("quick-and-dirty", 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   571
      ("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
   572
       bool_option quick_and_dirty)),
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   573
     ("full-proofs", 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   574
      ("Record full proof objects internally",
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   575
       proof_option)),
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   576
     ("theorem-dependencies", 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   577
       ("Track theorem dependencies within Proof General",
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   578
	thm_deps_option))])
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
end
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
(* Configuration: GUI config, proverinfo messages *)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   583
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   584
local
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   585
    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
   586
    val name_attr = pair "name"
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   587
    val version_attr = pair "version"
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   588
    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
   589
in
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   590
fun send_pgip_config () =
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   591
    let 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   592
	val path = Path.unpack config_file
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   593
	val exists = File.exists path
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   594
	val proverinfo = 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   595
	    XML.element "proverinfo"
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   596
              [("name",Session.name()), ("version", version),
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   597
	       ("url", isabelle_www)]
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   598
	    [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
   599
	     XML.element "helpdoc" 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   600
         (* 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
   601
          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
   602
          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
   603
		      [("name", "Isabelle/HOL Tutorial"),
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   604
		       ("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
   605
		       ("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
   606
	      []]
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   607
    in
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   608
	if exists then
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   609
	    (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
   610
	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
   611
    end;
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   612
end
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   613
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
(* PGIP identifier tables (prover objects). [incomplete] *)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   616
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   617
local
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   618
    val objtype_thy  = "theory"
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   619
    val objtype_thm  = "theorem"
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   620
    val objtype_term = "term"
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   621
    val objtype_type = "type"
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   622
		       
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   623
    fun xml_idtable ty ctx ids = 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   624
	let
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   625
            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
   626
              | ctx_attr None    = []
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   627
	    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
   628
	in 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   629
	    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
   630
	                          (map xmlid ids)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   631
	end
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   632
in
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   633
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   634
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
   635
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
   636
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
   637
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   638
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
   639
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   640
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
   641
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
   642
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   643
fun send_thm_idtable ctx thy = 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   644
    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
   645
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   646
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
   647
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   648
(* 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
   649
   & maybe not so useful anyway *)
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
end
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
(* 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
   654
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   655
local
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   656
 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
   657
 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
   658
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   659
 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
   660
in
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   661
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
   662
  | 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
   663
                           (* only theories known in top context *)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   664
  | 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
   665
  | 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
   666
  | 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
   667
                               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
   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
end
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   679
	 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   680
(** Parsing proof scripts without execution **)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   681
15146
eab7de0d0a31 Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents: 15145
diff changeset
   682
(* Notes.
eab7de0d0a31 Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents: 15145
diff changeset
   683
   This is quite tricky, because 1) we need to put back whitespace which
eab7de0d0a31 Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents: 15145
diff changeset
   684
   was removed during parsing so we can provide markup around commands;
eab7de0d0a31 Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents: 15145
diff changeset
   685
   2) parsing is intertwined with execution in Isar so we have to repeat
eab7de0d0a31 Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents: 15145
diff changeset
   686
   the parsing to extract interesting parts of commands.  The trace of
eab7de0d0a31 Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents: 15145
diff changeset
   687
   tokens parsed which is now recorded in each transition helps do this.
eab7de0d0a31 Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents: 15145
diff changeset
   688
   
eab7de0d0a31 Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents: 15145
diff changeset
   689
   If we had proper parse trees it would be easy, or if we could go
eab7de0d0a31 Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents: 15145
diff changeset
   690
   beyond ML's type system to allow existential types to be part of
eab7de0d0a31 Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents: 15145
diff changeset
   691
   parsers (the quantified type representing the result of the parse
eab7de0d0a31 Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents: 15145
diff changeset
   692
   which is used to make the transition function) it might be possible.
eab7de0d0a31 Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents: 15145
diff changeset
   693
eab7de0d0a31 Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents: 15145
diff changeset
   694
   Probably the best solution is to produce the meta-information at
eab7de0d0a31 Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents: 15145
diff changeset
   695
   the same time as the parse, for each command, e.g. by recording a 
eab7de0d0a31 Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents: 15145
diff changeset
   696
   list of (name,objtype) pairs which record the bindings created by 
eab7de0d0a31 Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents: 15145
diff changeset
   697
   a command.  This would require changing the interfaces in 
eab7de0d0a31 Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents: 15145
diff changeset
   698
   outer_syntax.ML (or providing new ones), 
eab7de0d0a31 Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents: 15145
diff changeset
   699
eab7de0d0a31 Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents: 15145
diff changeset
   700
    datatype metainfo = Binding of string * string  (* name, objtype *)
eab7de0d0a31 Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents: 15145
diff changeset
   701
eab7de0d0a31 Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents: 15145
diff changeset
   702
    val command_withmetainfo: string -> string -> string ->
eab7de0d0a31 Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents: 15145
diff changeset
   703
      (token list -> 
eab7de0d0a31 Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents: 15145
diff changeset
   704
       ((Toplevel.transition -> Toplevel.transition) * metainfo list) * 
eab7de0d0a31 Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents: 15145
diff changeset
   705
       token list) -> parser
eab7de0d0a31 Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents: 15145
diff changeset
   706
*)
eab7de0d0a31 Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents: 15145
diff changeset
   707
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   708
local
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   709
    fun markup_text str elt = [XML.element elt [] [XML.text str]]
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   710
    fun markup_text_attrs str elt attrs = [XML.element elt attrs [XML.text str]]
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   711
    fun empty elt = [XML.element elt [] []]
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   712
15146
eab7de0d0a31 Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents: 15145
diff changeset
   713
    (* an extra token is needed to terminate the command *)
eab7de0d0a31 Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents: 15145
diff changeset
   714
    val sync = OuterSyntax.scan "\\<^sync>";
eab7de0d0a31 Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents: 15145
diff changeset
   715
eab7de0d0a31 Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents: 15145
diff changeset
   716
    fun named_item_elt_with nameattr toks str elt nameP objtyp = 
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   717
	let 
15146
eab7de0d0a31 Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents: 15145
diff changeset
   718
	    val name = (fst (nameP (toks@sync)))
eab7de0d0a31 Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents: 15145
diff changeset
   719
			handle _ => (error ("Error occurred in name parser for " ^ elt ^ 
eab7de0d0a31 Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents: 15145
diff changeset
   720
					    "(objtype: " ^ objtyp ^ ")");
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   721
				     "")
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   722
				     
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   723
	in 
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   724
	    [XML.element elt 
15146
eab7de0d0a31 Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents: 15145
diff changeset
   725
			 ((if name="" then [] else [(nameattr, name)])@
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   726
			  (if objtyp="" then [] else [("objtype", objtyp)]))
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   727
			 ([XML.text str])]
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   728
	end
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   729
15146
eab7de0d0a31 Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents: 15145
diff changeset
   730
    val named_item_elt = named_item_elt_with "name"
eab7de0d0a31 Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents: 15145
diff changeset
   731
    val thmnamed_item_elt = named_item_elt_with "thmname"
eab7de0d0a31 Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents: 15145
diff changeset
   732
 
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   733
    fun parse_warning msg = warning ("script->PGIP markup parser: " ^ msg)
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   734
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   735
    (* FIXME: allow dynamic extensions to language here: we need a hook in
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   736
       outer_syntax.ML to reset this table. *)
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   737
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   738
    val keywords_classification_table = ref (None:(string Symtab.table) option)
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   739
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   740
    fun get_keywords_classification_table () = 
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   741
	case (!keywords_classification_table) of
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   742
	    Some t => t
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   743
	  | None => (let
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   744
			 val tab = foldl (fn (tab,(c,_,k,_))=>Symtab.update((c,k),tab)) 
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   745
					 (Symtab.empty,OuterSyntax.dest_parsers())
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   746
		     in (keywords_classification_table := Some tab; tab) end)
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   747
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   748
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   749
		    
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   750
    fun xmls_of_thy_begin (name,toks,str) = (* see isar_syn.ML/theoryP *)
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   751
	let 
15146
eab7de0d0a31 Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents: 15145
diff changeset
   752
	    val ((thyname,imports,files),_) = ThyHeader.args (toks@sync)
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   753
	in 
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   754
	    markup_text_attrs str "opentheory" [("thyname",thyname)]
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   755
	end 
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   756
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   757
    fun xmls_of_thy_decl (name,toks,str) = (* see isar_syn.ML/thy_decl cases  *)
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   758
	let 
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   759
	    (* NB: PGIP only deals with single name bindings at the moment;
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   760
	       potentially we could markup grouped definitions several times but
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   761
	       that might suggest the wrong structure to the editor?
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   762
	       Better alternative would be to put naming closer around text,
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   763
	       but to do that we'd be much better off modifying the real parser
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   764
	       instead of reconstructing it here. *)
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   765
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   766
	    val plain_items = (* no names, unimportant names, or too difficult *)
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   767
		["defaultsort","arities","judgement","finalconsts",
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   768
		 "syntax", "nonterminals", "translations",
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   769
		 "global", "local", "hide",
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   770
		 "ML_setup", "setup", "method_setup",
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   771
		 "parse_ast_translation", "parse_translation", "print_translation",
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   772
		 "typed_print_translation", "print_ast_translation", "token_translation",
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   773
		 "oracle",
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   774
		 "declare"]
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   775
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   776
	    val plain_item   = markup_text str "theoryitem"
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   777
	    val comment_item = markup_text str "litcomment"
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   778
	    val named_item   = named_item_elt toks str "theoryitem"
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   779
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   780
	    val opt_overloaded = P.opt_keyword "overloaded";
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   781
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   782
	    val thmnameP = (* see isar_syn.ML/theoremsP *)
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   783
		let 
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   784
		    val name_facts = P.and_list1 ((P.opt_thm_name "=" --| P.xthms1) >> #1)
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   785
		    val theoremsP = P.locale_target |-- name_facts >> (fn [] => "" | x::_ => x)
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   786
		in 
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   787
		    theoremsP
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   788
		end
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   789
	in 
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   790
	    if (name mem plain_items) then plain_item
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   791
	    else case name of
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   792
		     "text"      => comment_item
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   793
		   | "text_raw"  => comment_item
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   794
		   | "typedecl"  => named_item (P.type_args |-- P.name) "type"
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   795
		   | "types"     => named_item (P.type_args |-- P.name) "type"
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   796
		   | "classes"   => named_item P.name "class"
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   797
		   | "classrel"  => named_item P.name "class"
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   798
		   | "consts"    => named_item (P.const >> #1) "term"
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   799
		   | "axioms"    => named_item (P.spec_name >> (#1 o #1)) "theorem"
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   800
		   | "defs"	 => named_item (opt_overloaded |-- P.spec_name >> (#1 o #1)) "theorem"
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   801
		   | "constdefs" => named_item P.name (* FIXME: heavily simplified/wrong *) "term"
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   802
		   | "theorems"  => named_item thmnameP "thmset"
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   803
		   | "lemmas"    => named_item thmnameP "thmset"
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   804
		   | "oracle"    => named_item P.name "oracle"
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   805
		   | "locale"	 => named_item ((P.opt_keyword "open" >> not) |-- P.name) "locale"
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   806
		   | _ => (parse_warning ("Unrecognized thy-decl command: " ^ name); plain_item)
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   807
	end
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   808
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   809
    fun xmls_of_thy_goal (name,toks,str) = 
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   810
	let 
15146
eab7de0d0a31 Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents: 15145
diff changeset
   811
	    (* see isar_syn.ML/gen_theorem *)
eab7de0d0a31 Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents: 15145
diff changeset
   812
         val statement = P.and_list1 (P.opt_thm_name ":" -- Scan.repeat1 P.propp);
eab7de0d0a31 Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents: 15145
diff changeset
   813
	 val general_statement =
eab7de0d0a31 Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents: 15145
diff changeset
   814
	    statement >> pair [] || Scan.repeat P.locale_elem_or_expr -- (P.$$$ "shows" |-- statement);
eab7de0d0a31 Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents: 15145
diff changeset
   815
	    
eab7de0d0a31 Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents: 15145
diff changeset
   816
	    val gen_theoremP =
eab7de0d0a31 Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents: 15145
diff changeset
   817
		P.locale_target -- Scan.optional (P.opt_thm_name ":" --|
eab7de0d0a31 Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents: 15145
diff changeset
   818
                 Scan.ahead (P.locale_keyword || P.$$$ "shows")) ("", []) --
eab7de0d0a31 Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents: 15145
diff changeset
   819
				 general_statement >> (fn ((locale, a), (elems, concl)) => 
eab7de0d0a31 Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents: 15145
diff changeset
   820
							 fst a) (* a : (bstring * Args.src list) *)
eab7de0d0a31 Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents: 15145
diff changeset
   821
eab7de0d0a31 Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents: 15145
diff changeset
   822
	    val nameP = P.locale_target |-- (Scan.optional ((P.opt_thm_name ":") >> #1) "")
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   823
	    (* TODO: add preference values for attributes 
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   824
	       val prefval = XML.element "prefval" [("name","thm-kind"),("value",name)]
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   825
	    *)
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   826
	in 
15146
eab7de0d0a31 Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents: 15145
diff changeset
   827
	    thmnamed_item_elt toks str "opengoal" nameP ""
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   828
	end
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   829
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   830
    fun xmls_of_qed (name,markup) = case name of
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   831
      "sorry"         => markup "giveupgoal"
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   832
    | "oops"          => markup "postponegoal"
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   833
    | "done"          => markup "closegoal" 
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   834
    | "by"            => markup "closegoal"  (* nested or toplevel *)
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   835
    | "qed"           => markup "closegoal"  (* nested or toplevel *)
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   836
    | "."	      => markup "closegoal"  (* nested or toplevel *)
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   837
    | ".."	      => markup "closegoal"  (* nested or toplevel *)
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   838
    | other => (* default to closegoal: may be wrong for extns *)
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   839
      (parse_warning ("Unrecognized qed command: " ^ quote other); markup "closegoal")
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   840
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   841
    fun xmls_of_kind kind (name,toks,str) = 
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   842
    let val markup = markup_text str in 
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   843
    case kind of
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   844
      "control"        => markup "badcmd"
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   845
    | "diag"           => markup "spuriouscmd"
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   846
    (* theory/files *)
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   847
    | "theory-begin"   => xmls_of_thy_begin (name,toks,str)
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   848
    | "theory-decl"    => xmls_of_thy_decl (name,toks,str)
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   849
    | "theory-heading" => markup "litcomment"
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   850
    | "theory-script"  => markup "theorystep"
15146
eab7de0d0a31 Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents: 15145
diff changeset
   851
    | "theory-end"     => markup "closetheory"
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   852
    (* proof control *)
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   853
    | "theory-goal"    => xmls_of_thy_goal (name,toks,str)
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   854
    | "proof-heading"  => markup "litcomment"
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   855
    | "proof-goal"     => markup "opengoal"  (* nested proof: have, show, ... *)
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   856
    | "proof-block"    => markup "proofstep" (* context-shift: proof, next; really "newgoal" *)
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   857
    | "proof-open"     => (empty "openblock") @ (markup "proofstep")
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   858
    | "proof-close"    => (markup "proofstep") @ (empty "closeblock")
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   859
    | "proof-script"   => markup "proofstep"
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   860
    | "proof-chain"    => markup "proofstep"
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   861
    | "proof-decl"     => markup "proofstep"
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   862
    | "proof-asm"      => markup "proofstep"
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   863
    | "proof-asm-goal" => markup "proofstep"
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   864
    | "qed"            => xmls_of_qed (name,markup)
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   865
    | "qed-block"      => xmls_of_qed (name,markup)
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   866
    | "qed-global"     => xmls_of_qed (name,markup)
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   867
    | other => (* default for anything else is "spuriouscmd", ignored for undo. *)
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   868
      (parse_warning ("Internal inconsistency, unrecognized keyword kind: " ^ quote other);
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   869
       markup "spuriouscmd")
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   870
    end 
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   871
in
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   872
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   873
fun xmls_of_transition (name,str,toks) = 
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   874
   let 
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   875
       val classification = Symtab.lookup (get_keywords_classification_table(),name)
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   876
   in case classification of
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   877
	  Some k => (xmls_of_kind k (name,toks,str))
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   878
	| None => (* an uncategorized keyword ignored for undo (maybe wrong) *)
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   879
	  (parse_warning ("Uncategorized command found: " ^ name ^ " -- using spuriouscmd");
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   880
	   markup_text str "spuriouscmd")
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   881
   end 
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   882
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   883
fun xmls_of_impropers [] = []
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   884
  | xmls_of_impropers toks = 
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   885
    let 
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   886
	val (whs,rest) = take_prefix (not o OuterLex.is_proper) toks
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   887
	fun markup [] _ = []
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   888
	  | markup toks x = markup_text (implode (map OuterLex.unparse toks)) x
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   889
    in
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   890
	(markup whs "comment") @ (markup rest "unparseable")
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   891
    end
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   892
    
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   893
end
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   894
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   895
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   896
local
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   897
    (* we have to weave together the whitespace/comments with proper tokens 
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   898
       to reconstruct the input. *)
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   899
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   900
    fun match_tokens ([],us,vs) = (rev vs,us)  (* used, unused *)
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   901
      | match_tokens (t::ts,w::ws,vs) = 
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   902
	if (t = w) then match_tokens (ts,ws,w::vs)
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   903
	else match_tokens (t::ts,ws,w::vs)
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   904
      | match_tokens _ = error ("match_tokens: mismatched input parse")
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   905
in
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   906
    fun xmls_of_str str =
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   907
    let 
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   908
       val toks = OuterSyntax.scan str
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   909
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   910
       (* parsing:   See outer_syntax.ML/toplevel_source *)
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   911
    
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   912
       fun parse_loop ([],[],xmls) = xmls
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   913
	 | parse_loop ([],itoks,xmls) = xmls @ (xmls_of_impropers itoks)
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   914
	 | parse_loop ((nm,toks,_)::trs,itoks,xmls) =
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   915
	   let 
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   916
	       (* first proper token is command, except FIXME for -- *)
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   917
	       val (prewhs,cmditoks') = take_prefix (not o OuterLex.is_proper) itoks
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   918
	       val (cmdtok,itoks') = case cmditoks' of x::xs => (x,xs)
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   919
						  | _ => error("proof_general/parse_loop impossible") 
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   920
	       val (utoks,itoks'') = match_tokens (toks,itoks',[])
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   921
               (* FIXME: should take trailing [w/s+] semicolon too in utoks *)
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   922
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   923
	       val str = implode (map OuterLex.unparse (cmdtok::utoks))
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   924
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   925
	       val xmls_whs = xmls_of_impropers prewhs 
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   926
	       val xmls_tr  = xmls_of_transition (nm,str,toks)
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   927
	   in
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   928
	       parse_loop(trs,itoks'',xmls @ xmls_whs @ xmls_tr)
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   929
	   end
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   930
    in
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   931
	(* FIXME: put errors/warnings inside the parse result *)
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   932
	parse_loop (OuterSyntax.read toks, toks, [])
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   933
    end
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   934
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 parsescript str = 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   937
    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
   938
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   939
end
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   940
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   941
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   942
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   943
(**** PGIP:  Isabelle -> Interface ****)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   944
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   945
val isabelle_pgml_version_supported = "1.0"; 
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   946
val isabelle_pgip_version_supported = "2.0"
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   947
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   948
fun usespgip () = 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   949
    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
   950
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   951
fun usespgml () = 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   952
    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
   953
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   954
fun hasprefs () = 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   955
    seq (fn (prefcat, prefs) =>
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   956
	    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
   957
		 (map (fn (name, (descr, (ty, (default,_),_))) => 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   958
		       XML.element "haspref" [("name", name), 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   959
					      ("descr", descr), 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   960
					      ("default", default)]
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   961
		       [ty]) prefs)]) (!preferences);
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   962
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   963
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
   964
	
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   965
fun setpref name value = 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   966
    (case assoc (allprefs(), name) of
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   967
	 None => warning ("Unknown pref: " ^ quote name)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   968
       | Some (_, (_, _, set)) => set value);
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   969
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   970
fun getpref name = 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   971
    (case assoc (allprefs(), name) of
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   972
	 None => warning ("Unknown pref: " ^ quote name)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   973
       | Some (_, (_, (_,get), _)) => 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   974
	   issue_pgip "prefval" [("name", name)] (get ()));
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   975
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   976
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   977
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   978
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   979
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   980
(**** PGIP:  Interface -> Isabelle/Isar ****)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   981
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   982
exception PGIP of string;
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   983
exception PGIP_QUIT;
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   984
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   985
(* Sending commands to Isar *)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   986
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   987
fun isarcmd s = 
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   988
    s |> OuterSyntax.scan |> OuterSyntax.read 
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   989
      |> map (Toplevel.position (Position.name "PGIP message") o #3) |> Toplevel.>>>;
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   990
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   991
fun xmltext ((XML.Text text)::ts) = text ^ (xmltext ts)
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   992
  | xmltext [] = ""
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   993
  | xmltext _ = raise PGIP "Expected text (PCDATA/CDATA)"
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   994
			
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   995
fun isarscript xmls = isarcmd (xmltext xmls)   (* send a script command *)
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   996
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   997
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   998
(* 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
   999
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1000
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
  1001
    let
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1002
	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
  1003
    in
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1004
	case extn of
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1005
	    "" => 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
  1006
	  | "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
  1007
	  | "ML" => isarcmd ("use " ^ quote file)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1008
	  (* 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
  1009
	  | 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
  1010
    end  
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1011
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1012
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1013
local
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1014
  (* Proof control commands *)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1015
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1016
  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
  1017
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1018
  fun xmlattr attrs attr = 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1019
      (case xmlattro attrs attr of 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1020
	   Some value => value 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1021
	 | None => raise PGIP ("Missing attribute: " ^ attr))
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
  val thyname_attr = "thyname"
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1024
  val objtype_attr = "objtype"
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1025
  val name_attr = "name"
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1026
  val dirname_attr = "dir"
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1027
  fun comment x = "(* " ^ x ^ " *)"
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1028
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1029
  (* 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
  1030
  (* 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
  1031
  fun decode_url url = 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1032
      (let 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1033
	  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
  1034
 	  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
  1035
	  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
  1036
	  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
  1037
	  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
  1038
			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
  1039
		    else ""
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1040
      in 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1041
	  (proto,host,doc)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1042
      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
  1043
 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1044
  fun localfile_of_url url =
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1045
      let
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1046
	  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
  1047
      in
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1048
	  if (proto = "file" andalso 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1049
	      (host = "" orelse 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1050
	       host = "localhost" orelse 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1051
	       host = (getenv "HOSTNAME")))
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1052
	     then name
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1053
	  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
  1054
      end
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1055
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1056
  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
  1057
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1058
  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
  1059
  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
  1060
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1061
  val currently_open_file = ref (None : string option)
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1062
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1063
in
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1064
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1065
fun process_pgip_element pgipxml = (case pgipxml of 
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1066
  (XML.Text t) => warning ("Ignored text in PGIP packet: \n" ^ t)
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1067
| (XML.Elem (xml as (elem, attrs, data))) => 
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1068
  (case elem of
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1069
       (* protocol config *)
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1070
       "askpgip"  	=> (usespgip (); send_pgip_config ())
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1071
     | "askpgml"  	=> usespgml ()
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1072
     (* proverconfig *)
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1073
     | "askprefs" 	=> hasprefs ()
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1074
     | "getpref"  	=> getpref (xmlattr attrs name_attr)
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1075
     | "setpref"  	=> setpref (xmlattr attrs name_attr) (xmltext data)
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1076
     (* provercontrol *)
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1077
     | "proverinit" 	=> isar_restart ()
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1078
     | "proverexit" 	=> isarcmd "quit"
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1079
     | "startquiet" 	=> isarcmd "disable_pr"
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1080
     | "stopquiet"  	=> isarcmd "enable_pr"
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1081
     | "pgmlsymbolson"   => (print_mode := (["xsymbols", "symbols"] @ ! print_mode))
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1082
     | "pgmlsymbolsoff"  => (print_mode := (Library.gen_rems 
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1083
						(op =) 
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1084
						(! print_mode, ["xsymbols", "symbols"])))
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1085
     (* properproofcmd: proper commands which belong in script *)
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1086
     | "opengoal"       => isarscript data
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1087
     | "proofstep"      => isarscript data
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1088
     | "closegoal"      => isarscript data
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1089
     | "giveupgoal"     => isarscript data
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1090
     | "postponegoal"   => isarscript data
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1091
     | "comment"	=> isarscript data
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1092
     | "litcomment"     => isarscript data
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1093
     | "spuriouscmd"    => isarscript data
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1094
     | "badcmd"		=> isarscript data
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1095
     (* improperproofcmd: improper commands which *do not* belong in script *)
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1096
     | "undostep"       => isarcmd "ProofGeneral.undo"
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1097
     | "abortgoal"      => isarcmd "ProofGeneral.kill_proof"  
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1098
     | "forget"         => error "Not implemented" 
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1099
     | "restoregoal"    => error "Not implemented"  (* could just treat as forget? *)
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1100
     (* proofctxt: improper commands *)
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1101
     | "askids"         => askids (xmlattro attrs thyname_attr, 
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1102
				   xmlattro attrs objtype_attr)
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1103
     | "showid"	        => showid (xmlattro attrs thyname_attr, 
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1104
				   xmlattr attrs objtype_attr,
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1105
		     		   xmlattr attrs name_attr)
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1106
     | "parsescript"    => parsescript (xmltext data)
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1107
     | "showproofstate" => isarcmd "pr"
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1108
     | "showctxt"       => isarcmd "print_theory"   (* more useful than print_context *)
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1109
     | "searchtheorems" => isarcmd ("thms_containing " ^ (xmltext data))
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1110
     | "setlinewidth"   => isarcmd ("pretty_setmargin " ^ (xmltext data))
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1111
     | "viewdoc"	=> isarcmd ("print_" ^ (xmltext data)) (* FIXME: isatool doc? *)
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1112
     (* properfilecmd: proper theory-level script commands *)
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1113
     | "opentheory"     => isarscript data
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1114
     | "theoryitem"     => isarscript data
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1115
     | "closetheory"    => (isarscript data;
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1116
			    writeln ("Theory "^(topthy_name())^" completed."))
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1117
     (* improperfilecmd: theory-level commands not in script *)
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1118
     | "aborttheory"    => isarcmd ("init_toplevel")
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1119
     | "retracttheory"  => isarcmd ("kill_thy " ^
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1120
				    (quote (xmlattr attrs thyname_attr)))
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1121
     | "loadfile"       => use_thy_or_ml_file    (fileurl_of attrs)
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1122
     | "openfile"       => (inform_file_retracted (fileurl_of attrs);
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1123
			    currently_open_file := Some (fileurl_of attrs))
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1124
     | "closefile"      => (case !currently_open_file of 
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1125
				Some f => (inform_file_processed f;
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1126
					   currently_open_file := None)
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1127
			      | None => raise PGIP ("closefile when no file is open!"))
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1128
     | "abortfile"      => (currently_open_file := None) (* perhaps error for no file open *)
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1129
     | "changecwd"      => ThyLoad.add_path (xmlattr attrs dirname_attr)
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1130
     (* unofficial command for debugging *)
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1131
     | "quitpgip" => raise PGIP_QUIT  
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1132
     | _ => raise PGIP ("Unrecognized PGIP element: " ^ elem)))
15134
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 process_pgip_tree s = 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1135
    (pgip_refseq := None; 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1136
     pgip_refid := None;
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1137
     (case s of
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1138
	  XML.Elem ("pgip", attrs, pgips) => 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1139
	  (let 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1140
	       val class = xmlattr attrs "class"
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1141
	       val _ = (pgip_refseq := xmlattro attrs "seq";
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1142
			pgip_refid :=  xmlattro attrs "id")
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1143
	   in  
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1144
	       if (class = "pa") then
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1145
		   seq process_pgip_element pgips
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1146
	       else 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1147
		   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
  1148
	   end)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1149
	| _ => raise PGIP "Invalid PGIP packet received") 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1150
     handle (PGIP msg) => 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1151
	    (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
  1152
		    (XML.string_of_tree s))))
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
(* for export to Emacs *)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1155
(* 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
  1156
(* 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
  1157
   during output *)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1158
fun process_pgip s = 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1159
    (pgip_emacs_compatibility_flag := true;
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1160
     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
  1161
     pgip_emacs_compatibility_flag := false)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1162
end
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1163
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1164
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1165
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1166
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1167
(* PGIP loop: process PGIP input only *)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1168
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1169
local  
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1170
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1171
exception XML_PARSE
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1172
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1173
fun loop src : unit =
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1174
    let 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1175
	val _ = issue_pgipe "ready" []
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1176
	val pgipo = (Source.get_single src) 
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1177
			handle e => raise XML_PARSE
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1178
    in
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1179
	case pgipo of  
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1180
	     None  => ()
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1181
	   | Some (pgip,src') =>  
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1182
	     ((process_pgip_tree pgip); loop src') handle e => handler (e,Some src')
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1183
    end handle e => handler (e,Some src)  (* i.e. error in ready/XML parse *)
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1184
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1185
and handler (e,srco) = 
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1186
    case (e,srco) of
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1187
        (XML_PARSE,Some src) => 
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1188
	(* (!error_fn "Invalid XML input, aborting"; ()) NB: loop OK for tty, but want exit on EOF *)
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1189
         panic "Invalid XML input, aborting"
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1190
      | (PGIP_QUIT,_) => ()
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1191
      | (ERROR,Some src) => loop src (* message already given *)
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1192
      | (Interrupt,Some src) => (!error_fn "Interrupt during PGIP processing"; loop src)
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1193
      | (Toplevel.UNDEF,Some src) => (error "No working context defined"; loop src) (* usually *)
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1194
      | (e,Some src) => (error (Toplevel.exn_message e); loop src)
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1195
      | (_,None) => ()
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1196
in
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1197
  (* NB: simple tty for now; later might read from other tty-style sources (e.g. sockets). *)
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1198
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1199
  val xmlP = XML.scan_comment_whspc |-- XML.parse_elem >> single
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1200
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1201
  val tty_src = Source.set_prompt "" (Source.source Symbol.stopper xmlP None Source.tty)
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1202
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1203
  val pgip_toplevel =  loop 
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1204
end
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1205
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1206
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1207
(* additional outer syntax for Isar *)
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1208
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1209
local structure P = OuterParse and K = OuterSyntax.Keyword in
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1210
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1211
val undoP = (* undo without output *)
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1212
  OuterSyntax.improper_command "ProofGeneral.undo" "(internal)" K.control
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1213
    (Scan.succeed (Toplevel.no_timing o IsarCmd.undo));
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1214
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1215
val context_thy_onlyP =
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1216
  OuterSyntax.improper_command "ProofGeneral.context_thy_only" "(internal)" K.control
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1217
    (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
  1218
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1219
val try_context_thy_onlyP =
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1220
  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
  1221
    (P.name >> (Toplevel.no_timing oo
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1222
      (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
  1223
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1224
val restartP =
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1225
  OuterSyntax.improper_command "ProofGeneral.restart" "(internal)" K.control
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1226
    (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
  1227
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1228
val kill_proofP =
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1229
  OuterSyntax.improper_command "ProofGeneral.kill_proof" "(internal)" K.control
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1230
    (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
  1231
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1232
val inform_file_processedP =
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1233
  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
  1234
    (P.name >> (fn file => Toplevel.no_timing o
bef0dc694c48 Path.split_ext; more robust inform_file_processed;
wenzelm
parents: 14880
diff changeset
  1235
      Toplevel.keep (vacuous_inform_file_processed file) o
bef0dc694c48 Path.split_ext; more robust inform_file_processed;
wenzelm
parents: 14880
diff changeset
  1236
      Toplevel.kill o
bef0dc694c48 Path.split_ext; more robust inform_file_processed;
wenzelm
parents: 14880
diff changeset
  1237
      Toplevel.keep (proper_inform_file_processed file)));
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1238
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1239
val inform_file_retractedP =
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1240
  OuterSyntax.improper_command "ProofGeneral.inform_file_retracted" "(internal)" K.control
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1241
    (P.name >> (Toplevel.no_timing oo
14902
bef0dc694c48 Path.split_ext; more robust inform_file_processed;
wenzelm
parents: 14880
diff changeset
  1242
      (fn file => Toplevel.imperative (fn () => inform_file_retracted file))));
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1243
14725
2ed5b960c6b1 ProofGeneral.process_pgip command;
wenzelm
parents: 14707
diff changeset
  1244
val process_pgipP =
2ed5b960c6b1 ProofGeneral.process_pgip command;
wenzelm
parents: 14707
diff changeset
  1245
  OuterSyntax.improper_command "ProofGeneral.process_pgip" "(internal)" K.control
2ed5b960c6b1 ProofGeneral.process_pgip command;
wenzelm
parents: 14707
diff changeset
  1246
    (P.text >> (Toplevel.no_timing oo
2ed5b960c6b1 ProofGeneral.process_pgip command;
wenzelm
parents: 14707
diff changeset
  1247
      (fn txt => Toplevel.imperative (fn () => process_pgip txt))));
2ed5b960c6b1 ProofGeneral.process_pgip command;
wenzelm
parents: 14707
diff changeset
  1248
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1249
fun init_outer_syntax () = OuterSyntax.add_parsers
14675
08b9c690f9cf removed obsolete 'undo';
wenzelm
parents: 14568
diff changeset
  1250
 [undoP, restartP, kill_proofP, context_thy_onlyP, try_context_thy_onlyP,
14725
2ed5b960c6b1 ProofGeneral.process_pgip command;
wenzelm
parents: 14707
diff changeset
  1251
  inform_file_processedP, inform_file_retractedP, process_pgipP];
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1252
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1253
end;
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1254
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1255
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1256
(* init *)
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1257
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1258
val initialized = ref false;
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1259
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1260
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
  1261
  | 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
  1262
  | set_prompts false false = 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1263
    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
  1264
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1265
fun init_setup isar pgip =
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1266
 (conditional (not (! initialized)) (fn () =>
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1267
   (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
  1268
    setup_xsymbols_output ();
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1269
    setup_pgml_output ();
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1270
    setup_messages ();
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1271
    setup_state ();
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1272
    setup_thy_loader ();