src/Pure/proof_general.ML
author wenzelm
Tue, 17 May 2005 18:51:16 +0200
changeset 15992 cb02d70a2040
parent 15985 f00dd5e06ffe
child 16022 96a9bf7ac18d
permissions -rw-r--r--
var_or_skolem: always print question mark for vars stemming from skolems;
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
15173
e1582a0d29b5 Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents: 15156
diff changeset
    10
settings menu in the currently released version of Proof General (3.5).
15134
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
15173
e1582a0d29b5 Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents: 15156
diff changeset
    13
The 3.6pre pre-release versions of Emacs Proof General now support the 
e1582a0d29b5 Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents: 15156
diff changeset
    14
new PGIP format for preferences and restore the settings menu.  
e1582a0d29b5 Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents: 15156
diff changeset
    15
Please visit http://proofgeneral.inf.ed.ac.uk/develdownload
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    16
===========================================================================
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    17
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
    18
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
    19
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    20
*)
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    21
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    22
signature PROOF_GENERAL =
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    23
sig
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    24
  val update_thy_only: string -> unit
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    25
  val try_update_thy_only: string -> unit
13391
553e7b62680f fixed inform_file_retracted: remove_thy;
wenzelm
parents: 13284
diff changeset
    26
  val inform_file_retracted: string -> unit
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    27
  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
    28
  val preferences: 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    29
      (string * 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    30
	(string * 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    31
	 (string * 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    32
	  (string * (string * (unit -> string)) * 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    33
	   (string -> unit)))) list) list ref
13728
8004e56204fd Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents: 13646
diff changeset
    34
  val process_pgip: string -> unit
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    35
  val thms_containing: string list -> unit
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    36
  val help: unit -> unit
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    37
  val show_context: unit -> theory
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    38
  val kill_goal: unit -> unit
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    39
  val repeat_undo: int -> unit
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    40
  val isa_restart: unit -> unit
12833
9f3226cfe021 full_proofs;
wenzelm
parents: 12780
diff changeset
    41
  val full_proofs: bool -> unit
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    42
  val isarcmd: string -> unit
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    43
  val init: bool -> unit
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    44
  val init_pgip: bool -> unit
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    45
  val write_keywords: string -> unit
15146
eab7de0d0a31 Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents: 15145
diff changeset
    46
  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
    47
end;
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    48
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    49
structure ProofGeneral : PROOF_GENERAL =
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    50
struct
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    51
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
    52
structure P = OuterParse
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
    53
15191
5ca1fd9dec83 Support parsing of -- {* comments *}. Add extra output channels.
aspinall
parents: 15173
diff changeset
    54
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    55
(* 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
    56
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    57
val pgip_active = ref false;
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    58
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
    59
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    60
fun pgip () = (!pgip_active);
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    61
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
    62
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    63
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    64
(* print modes *)
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    65
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    66
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
    67
val xsymbolsN = Symbol.xsymbolsN;    (* XSymbols symbols *)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    68
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
    69
val pgmlatomsN = "PGMLatoms";	     (* variable kind decorations *)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    70
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
    71
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    72
fun pgml () = pgmlN mem_string ! print_mode;
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    73
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    74
(* text output: print modes for xsymbol and PGML *)
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    75
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    76
local
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    77
14827
d973e7f820cb Output.add_mode; Output.timing;
wenzelm
parents: 14725
diff changeset
    78
fun xsym_output "\\" = "\\\\"
d973e7f820cb Output.add_mode; Output.timing;
wenzelm
parents: 14725
diff changeset
    79
  | 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
    80
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    81
fun xsymbols_output s =
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    82
  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
    83
    let val syms = Symbol.explode s
14827
d973e7f820cb Output.add_mode; Output.timing;
wenzelm
parents: 14725
diff changeset
    84
    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
    85
  else Symbol.default_output s;
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    86
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    87
fun pgml_sym s =
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    88
  (case Symbol.decode s of
15254
10cfd6a14682 Simplification to symbol processing; put quotes around theory name in message.
aspinall
parents: 15253
diff changeset
    89
    (* NB: an alternative here would be to output the default print mode alternative
10cfd6a14682 Simplification to symbol processing; put quotes around theory name in message.
aspinall
parents: 15253
diff changeset
    90
       in the element content, but unfortunately print modes are not that fine grained. *)
15266
0398af5501fe Revert change to pgml_sym
aspinall
parents: 15254
diff changeset
    91
    Symbol.Char s => XML.text s
15403
9e58e666074d Fix pgmlsymbolson/off.
aspinall
parents: 15401
diff changeset
    92
  | Symbol.Sym sn => XML.element "sym" [("name", sn)] [XML.text s]
9e58e666074d Fix pgmlsymbolson/off.
aspinall
parents: 15401
diff changeset
    93
  | Symbol.Ctrl sn => XML.element "ctrl" [("name", sn)] [XML.text s]   (* FIXME: no such PGML! *)
15266
0398af5501fe Revert change to pgml_sym
aspinall
parents: 15254
diff changeset
    94
  | Symbol.Raw s => s);
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    95
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    96
fun pgml_output str =
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    97
  let val syms = Symbol.explode str
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    98
  in (implode (map pgml_sym syms), real (Symbol.length syms)) end;
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    99
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   100
in 
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   101
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   102
fun setup_xsymbols_output () = 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   103
    Output.add_mode 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   104
	xsymbolsN 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   105
	(xsymbols_output, Symbol.default_indent, Symbol.encode_raw);
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   106
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   107
fun setup_pgml_output () = 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   108
    Output.add_mode 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   109
	pgmlN
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   110
	(pgml_output, Symbol.default_indent, Symbol.encode_raw);
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   111
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   112
end;
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   113
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   114
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   115
(* token translations *)
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   116
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   117
local
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   118
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   119
val end_tag = oct_char "350";
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   120
val class_tag = ("class", oct_char "351");
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   121
val tfree_tag = ("tfree", oct_char "352");
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   122
val tvar_tag = ("tvar", oct_char "353");
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   123
val free_tag = ("free", oct_char "354");
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   124
val bound_tag = ("bound", oct_char "355");
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   125
val var_tag = ("var", oct_char "356");
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   126
val skolem_tag = ("skolem", oct_char "357");
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   127
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   128
fun xml_atom kind x = XML.element "atom" [("kind", kind)] [XML.text x];
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   129
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   130
fun tagit (kind, bg_tag) x =
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   131
    (if Output.has_mode pgmlatomsN then 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   132
	 xml_atom kind x
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   133
     else bg_tag ^ x ^ end_tag, 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   134
     real (Symbol.length (Symbol.explode x)));
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   135
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   136
fun free_or_skolem x =
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   137
  (case try Syntax.dest_skolem x of
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15472
diff changeset
   138
    NONE => tagit free_tag x
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15472
diff changeset
   139
  | SOME x' => tagit skolem_tag x');
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   140
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   141
fun var_or_skolem s =
15985
f00dd5e06ffe renamed show_var_qmarks to show_question_marks;
wenzelm
parents: 15964
diff changeset
   142
  (case Syntax.read_variable s of
f00dd5e06ffe renamed show_var_qmarks to show_question_marks;
wenzelm
parents: 15964
diff changeset
   143
    SOME (x, i) =>
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   144
      (case try Syntax.dest_skolem x of
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15472
diff changeset
   145
        NONE => tagit var_tag s
15992
cb02d70a2040 var_or_skolem: always print question mark for vars stemming from skolems;
wenzelm
parents: 15985
diff changeset
   146
      | SOME x' => tagit skolem_tag
cb02d70a2040 var_or_skolem: always print question mark for vars stemming from skolems;
wenzelm
parents: 15985
diff changeset
   147
          (setmp show_question_marks true Syntax.string_of_vname (x', i)))
15985
f00dd5e06ffe renamed show_var_qmarks to show_question_marks;
wenzelm
parents: 15964
diff changeset
   148
  | NONE => tagit var_tag s);
12778
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
15801
d2f5ca3c048d superceded by Pure.thy and CPure.thy;
wenzelm
parents: 15629
diff changeset
   159
in
d2f5ca3c048d superceded by Pure.thy and CPure.thy;
wenzelm
parents: 15629
diff changeset
   160
d2f5ca3c048d superceded by Pure.thy and CPure.thy;
wenzelm
parents: 15629
diff changeset
   161
val _ = Context.add_setup [Theory.add_tokentrfuns proof_general_trans];
d2f5ca3c048d superceded by Pure.thy and CPure.thy;
wenzelm
parents: 15629
diff changeset
   162
d2f5ca3c048d superceded by Pure.thy and CPure.thy;
wenzelm
parents: 15629
diff changeset
   163
end;
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   164
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   165
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   166
(* assembling PGIP packets *)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   167
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15472
diff changeset
   168
val pgip_refseq = ref NONE : string option ref
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15472
diff changeset
   169
val pgip_refid = ref NONE : string option ref
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   170
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   171
local
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   172
    val myseq_no = ref 1;      (* PGIP packet counter *)
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   173
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   174
    val pgip_class  = "pg"
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   175
    val pgip_origin = "Isabelle/Isar"
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   176
    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
   177
		   (Time.toString(Time.now()))
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   178
	          (* 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
   179
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   180
    fun assemble_pgips pgips = 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   181
	XML.element 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   182
	     "pgip" 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   183
	     ([("class",  pgip_class),
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   184
	       ("origin", pgip_origin),
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   185
	       ("id",     pgip_id)] @
15570
8d8c70b41bab Move towards standard functions.
skalberg
parents: 15531
diff changeset
   186
	      getOpt (Option.map (single o (pair "refseq")) (!pgip_refseq), []) @
8d8c70b41bab Move towards standard functions.
skalberg
parents: 15531
diff changeset
   187
	      getOpt (Option.map (single o (pair "refid")) (!pgip_refid), []) @
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   188
	      [("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
   189
	     pgips
13526
9269275e5da6 result dependency output;
wenzelm
parents: 13391
diff changeset
   190
in
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   191
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   192
 fun decorated_output bg en prfx = 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   193
    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
   194
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   195
 (* 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
   196
    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
   197
 fun issue_pgips ps = 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   198
     if pgip_emacs_compatibility() then
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   199
	 decorated_output (* add urgent message annotation *)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   200
	     (oct_char "360") (oct_char "361") "" 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   201
	     (assemble_pgips ps)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   202
     else 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   203
	 writeln_default (assemble_pgips ps)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   204
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   205
 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
   206
				  
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   207
 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
   208
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   209
 (* FIXME: need to add stuff to gather PGIPs here *)
15173
e1582a0d29b5 Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents: 15156
diff changeset
   210
 fun issue_pgip resp attrs txt = 
e1582a0d29b5 Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents: 15156
diff changeset
   211
     if pgip_emacs_compatibility() then
e1582a0d29b5 Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents: 15156
diff changeset
   212
	 decorated_output (* add urgent message annotation *)
e1582a0d29b5 Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents: 15156
diff changeset
   213
	     (oct_char "360") (oct_char "361") "" 
e1582a0d29b5 Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents: 15156
diff changeset
   214
	     (assemble_pgip resp attrs txt)
e1582a0d29b5 Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents: 15156
diff changeset
   215
     else 
e1582a0d29b5 Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents: 15156
diff changeset
   216
	 writeln_default (assemble_pgip resp attrs txt)
15134
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
(*  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
   219
 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
   220
     if pgip_emacs_compatibility() then
15400
50bbdabd7326 Insert pgmltext element into responses in PGIP mode
aspinall
parents: 15289
diff changeset
   221
        (*  in PGIP mode, but using escape characters as well.  *)
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   222
	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
   223
     else 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   224
	issue_pgip resp attrs s
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   225
	
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   226
 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
   227
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   228
end
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   229
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   230
(* messages and notification *)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   231
15173
e1582a0d29b5 Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents: 15156
diff changeset
   232
local
e1582a0d29b5 Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents: 15156
diff changeset
   233
    val delay_msgs = ref false   (* whether to accumulate messages *)
e1582a0d29b5 Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents: 15156
diff changeset
   234
    val delayed_msgs = ref []
e1582a0d29b5 Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents: 15156
diff changeset
   235
in
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   236
15173
e1582a0d29b5 Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents: 15156
diff changeset
   237
 fun message resp attrs bg en prfx s =
e1582a0d29b5 Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents: 15156
diff changeset
   238
     if pgip() then 
e1582a0d29b5 Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents: 15156
diff changeset
   239
	 (if (!delay_msgs) then
e1582a0d29b5 Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents: 15156
diff changeset
   240
	      delayed_msgs := (resp,attrs,prefix_lines prfx s)::(!delayed_msgs) (* nb: no decs *)
e1582a0d29b5 Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents: 15156
diff changeset
   241
	  else 
15400
50bbdabd7326 Insert pgmltext element into responses in PGIP mode
aspinall
parents: 15289
diff changeset
   242
	      issue_pgip_maybe_decorated bg en resp attrs 
50bbdabd7326 Insert pgmltext element into responses in PGIP mode
aspinall
parents: 15289
diff changeset
   243
					 (XML.element "pgmltext" [] [prefix_lines prfx s]))
15173
e1582a0d29b5 Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents: 15156
diff changeset
   244
     else 
e1582a0d29b5 Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents: 15156
diff changeset
   245
	 decorated_output bg en prfx s;
e1582a0d29b5 Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents: 15156
diff changeset
   246
e1582a0d29b5 Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents: 15156
diff changeset
   247
 fun start_delay_msgs () = (delay_msgs := true;
e1582a0d29b5 Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents: 15156
diff changeset
   248
			    delayed_msgs := [])
e1582a0d29b5 Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents: 15156
diff changeset
   249
e1582a0d29b5 Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents: 15156
diff changeset
   250
 fun end_delayed_msgs () = 
e1582a0d29b5 Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents: 15156
diff changeset
   251
     (delay_msgs := false;
15400
50bbdabd7326 Insert pgmltext element into responses in PGIP mode
aspinall
parents: 15289
diff changeset
   252
      map (fn (resp,attrs,s) => XML.element resp attrs [XML.element "pgmltext" [] [s]]) (!delayed_msgs))
15173
e1582a0d29b5 Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents: 15156
diff changeset
   253
end
15134
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
local
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   256
    val display_area = ("area", "display")
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   257
    val message_area = ("area", "message")
15191
5ca1fd9dec83 Support parsing of -- {* comments *}. Add extra output channels.
aspinall
parents: 15173
diff changeset
   258
    val internal_category = ("messagecategory", "internal")
5ca1fd9dec83 Support parsing of -- {* comments *}. Add extra output channels.
aspinall
parents: 15173
diff changeset
   259
    val info_category = ("messagecategory", "information")
5ca1fd9dec83 Support parsing of -- {* comments *}. Add extra output channels.
aspinall
parents: 15173
diff changeset
   260
    val tracing_category = ("messagecategory", "tracing")
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   261
    val urgent_indication = ("urgent", "y")
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   262
    val nonfatal = ("fatality", "nonfatal")
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   263
    val fatal = ("fatality", "fatal")
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   264
    val panic = ("fatality", "panic")
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   265
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   266
    val thyname_attr = pair "thyname"
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   267
    val url_attr = pair "url"
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   268
    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
   269
in			   
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   270
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   271
fun setup_messages () =
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   272
 (writeln_fn  := message "normalresponse" [message_area] "" "" "";
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   273
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   274
  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
   275
			 (oct_char "360") (oct_char "361") "";
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   276
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   277
  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
   278
			(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
   279
15191
5ca1fd9dec83 Support parsing of -- {* comments *}. Add extra output channels.
aspinall
parents: 15173
diff changeset
   280
  info_fn := message "normalresponse" [message_area, info_category]
5ca1fd9dec83 Support parsing of -- {* comments *}. Add extra output channels.
aspinall
parents: 15173
diff changeset
   281
			(oct_char "362") (oct_char "363") "+++ ";
5ca1fd9dec83 Support parsing of -- {* comments *}. Add extra output channels.
aspinall
parents: 15173
diff changeset
   282
5ca1fd9dec83 Support parsing of -- {* comments *}. Add extra output channels.
aspinall
parents: 15173
diff changeset
   283
  debug_fn := message "normalresponse" [message_area, internal_category]
5ca1fd9dec83 Support parsing of -- {* comments *}. Add extra output channels.
aspinall
parents: 15173
diff changeset
   284
			(oct_char "362") (oct_char "363") "+++ ";
5ca1fd9dec83 Support parsing of -- {* comments *}. Add extra output channels.
aspinall
parents: 15173
diff changeset
   285
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   286
  warning_fn := message "errorresponse"    [nonfatal]
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   287
			(oct_char "362") (oct_char "363") "### ";
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   288
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   289
  error_fn := message "errorresponse" [fatal]
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   290
		      (oct_char "364") (oct_char "365") "*** ";
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   291
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   292
  panic_fn := message "errorresponse" [panic]
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   293
		      (oct_char "364") (oct_char "365") "!!! ")
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   294
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   295
15400
50bbdabd7326 Insert pgmltext element into responses in PGIP mode
aspinall
parents: 15289
diff changeset
   296
(* accumulate printed output in a single PGIP response (inside <pgmltext>) *)
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   297
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   298
fun with_displaywrap (elt,attrs) dispfn =
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   299
    let 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   300
	val lines = ref ([] : string list);
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   301
	fun wlgrablines s = (lines:= (s :: (!lines)))
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   302
    in 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   303
	(setmp writeln_fn wlgrablines dispfn ();
15400
50bbdabd7326 Insert pgmltext element into responses in PGIP mode
aspinall
parents: 15289
diff changeset
   304
	 (* FIXME: XML.element here inefficient, should use stream output *)
50bbdabd7326 Insert pgmltext element into responses in PGIP mode
aspinall
parents: 15289
diff changeset
   305
         issue_pgip elt attrs (XML.element "pgmltext" [] (!lines)))
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   306
    end
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   307
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   308
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
   309
    
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   310
fun tell_clear_goals () = 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   311
    if pgip() then
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   312
	issue_pgipe "cleardisplay" [display_area]
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   313
    else 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   314
	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
   315
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   316
fun tell_clear_response () = 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   317
    if pgip() then
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   318
	issue_pgipe "cleardisplay" [message_area]
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   319
    else 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   320
	emacs_notify "Proof General, please clear the response buffer.";
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   321
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   322
fun tell_file_loaded path = 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   323
    if pgip() then
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   324
	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
   325
		    [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
   326
		     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
   327
    else 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   328
	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
   329
		      ^ quote (File.sysify_path path));
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   330
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   331
fun tell_file_retracted path = 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   332
    if pgip() then
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   333
	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
   334
		    [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
   335
		     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
   336
    else 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   337
	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
   338
		      ^ quote (File.sysify_path path));
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   339
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   340
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   341
(* theory / proof state output *)
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   342
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   343
local
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   344
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   345
    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
   346
			      (oct_char "366", oct_char "367", "") f ()
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   347
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   348
    fun statedisplay prts =
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   349
	issue_pgip "proofstate" []
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   350
		   (XML.element "pgml" []
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   351
				[XML.element "statedisplay" 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   352
					     [] 
15173
e1582a0d29b5 Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents: 15156
diff changeset
   353
					     [(Pretty.output (Pretty.chunks prts))]])
13545
fcdbd6cf5f9f improved tell_thm_deps;
wenzelm
parents: 13538
diff changeset
   354
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   355
    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
   356
	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
   357
	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
   358
	     
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   359
    fun print_state b st =
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   360
	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
   361
	else tmp_markers (fn () => Toplevel.print_state_default b st)
13526
9269275e5da6 result dependency output;
wenzelm
parents: 13391
diff changeset
   362
in
9269275e5da6 result dependency output;
wenzelm
parents: 13391
diff changeset
   363
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   364
 fun setup_state () =
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   365
     (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
   366
      Toplevel.print_state_fn := print_state;
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   367
      (* 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
   368
      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
   369
				   Toplevel.prompt_state_default));
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   370
end
13728
8004e56204fd Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents: 13646
diff changeset
   371
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   372
end
13728
8004e56204fd Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents: 13646
diff changeset
   373
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   374
(* misc commands for ProofGeneral/isa *)
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   375
15964
f2074e12d1d4 searching for thms by combination of criteria (intro, elim, dest, name, term pattern)
kleing
parents: 15801
diff changeset
   376
(* PG/isa mode does not go through the Isar parser, hence we 
f2074e12d1d4 searching for thms by combination of criteria (intro, elim, dest, name, term pattern)
kleing
parents: 15801
diff changeset
   377
   interpret everything as term pattern only *)
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   378
fun thms_containing ss =
15964
f2074e12d1d4 searching for thms by combination of criteria (intro, elim, dest, name, term pattern)
kleing
parents: 15801
diff changeset
   379
  ProofContext.print_thms_containing (ProofContext.init (the_context ())) NONE NONE 
f2074e12d1d4 searching for thms by combination of criteria (intro, elim, dest, name, term pattern)
kleing
parents: 15801
diff changeset
   380
    (map (fn s => (true, ProofContext.Pattern s)) ss);
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   381
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   382
val welcome = priority o Session.welcome;
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   383
val help = welcome;
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   384
val show_context = Context.the_context;
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   385
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   386
fun kill_goal () = (Goals.reset_goals (); tell_clear_goals ());
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   387
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   388
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
   389
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   390
fun repeat_undo 0 = ()
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   391
  | repeat_undo 1 = undo ()
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   392
  | 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
   393
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   394
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   395
(* theory loader actions *)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   396
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   397
local
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   398
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   399
fun add_master_files name files =
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   400
  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
   401
  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
   402
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   403
fun trace_action action name =
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   404
  if action = ThyInfo.Update then
15570
8d8c70b41bab Move towards standard functions.
skalberg
parents: 15531
diff changeset
   405
    List.app tell_file_loaded (ThyInfo.loaded_files name)
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   406
  else if action = ThyInfo.Outdate orelse action = ThyInfo.Remove then
15570
8d8c70b41bab Move towards standard functions.
skalberg
parents: 15531
diff changeset
   407
    List.app tell_file_retracted (add_master_files name (ThyInfo.loaded_files name))
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   408
  else ();
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   409
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   410
in
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   411
  fun setup_thy_loader () = ThyInfo.add_hook trace_action;
15570
8d8c70b41bab Move towards standard functions.
skalberg
parents: 15531
diff changeset
   412
  fun sync_thy_loader () = List.app (trace_action ThyInfo.Update) (ThyInfo.names ());
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   413
end;
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   414
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   415
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   416
(* prepare theory context *)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   417
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   418
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
   419
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
   420
			    false ThyInfo.update_thy_only;
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   421
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   422
fun which_context () =
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   423
  (case Context.get_context () of
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15472
diff changeset
   424
    SOME thy => "  Using current (dynamic!) one: " ^
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15472
diff changeset
   425
      (case try PureThy.get_name thy of SOME name => quote name | NONE => "<unnamed>")
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15472
diff changeset
   426
  | NONE => "");
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   427
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   428
fun try_update_thy_only file =
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   429
  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
   430
    let val name = thy_name file in
15570
8d8c70b41bab Move towards standard functions.
skalberg
parents: 15531
diff changeset
   431
      if isSome (ThyLoad.check_file NONE (ThyLoad.thy_path name)) 
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   432
      then update_thy_only name
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   433
      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
   434
    end) ();
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   435
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   436
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   437
(* get informed about files *)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   438
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   439
val inform_file_retracted = 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   440
    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
   441
val inform_file_processed = 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   442
    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
   443
15629
4066f01f1beb Add askguise/informguise as best as easily possible. Prevent warning in openfile when file doesn't exist in theory database.
aspinall
parents: 15626
diff changeset
   444
fun if_known_thy_no_warning f name = if ThyInfo.known_thy name then f name else ();
4066f01f1beb Add askguise/informguise as best as easily possible. Prevent warning in openfile when file doesn't exist in theory database.
aspinall
parents: 15626
diff changeset
   445
4066f01f1beb Add askguise/informguise as best as easily possible. Prevent warning in openfile when file doesn't exist in theory database.
aspinall
parents: 15626
diff changeset
   446
val openfile_retract = 
4066f01f1beb Add askguise/informguise as best as easily possible. Prevent warning in openfile when file doesn't exist in theory database.
aspinall
parents: 15626
diff changeset
   447
    if_known_thy_no_warning ThyInfo.remove_thy o thy_name;
4066f01f1beb Add askguise/informguise as best as easily possible. Prevent warning in openfile when file doesn't exist in theory database.
aspinall
parents: 15626
diff changeset
   448
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   449
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
   450
  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
   451
    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
   452
     (ThyInfo.touch_child_thys name;
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   453
      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
   454
       (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
   455
        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
   456
    else raise Toplevel.UNDEF
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   457
  end;
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   458
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   459
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
   460
 (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
   461
  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
   462
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   463
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   464
(* restart top-level loop (keeps most state information) *)
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   465
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   466
local
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   467
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   468
fun restart isar =
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   469
 (if isar then tell_clear_goals () else kill_goal ();
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   470
  tell_clear_response ();
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   471
  welcome ());
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   472
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   473
in
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   474
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   475
fun isa_restart () = restart false;
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   476
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
   477
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   478
end;
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   479
12833
9f3226cfe021 full_proofs;
wenzelm
parents: 12780
diff changeset
   480
fun full_proofs true = proofs := 2
9f3226cfe021 full_proofs;
wenzelm
parents: 12780
diff changeset
   481
  | full_proofs false = proofs := 1;
9f3226cfe021 full_proofs;
wenzelm
parents: 12780
diff changeset
   482
9f3226cfe021 full_proofs;
wenzelm
parents: 12780
diff changeset
   483
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   484
(* theorem dependency output *)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   485
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   486
local
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   487
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   488
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
   489
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   490
fun thm_deps_message (thms, deps) = 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   491
    if pgip() then
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   492
	issue_pgips 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   493
	    [XML.element
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   494
		 "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
   495
		 [("infotype", "isabelle_theorem_dependencies")]
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   496
		 [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
   497
		  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
   498
    else emacs_notify 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   499
	     ("Proof General, theorem dependencies of " 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   500
	      ^ thms ^ " are " ^ deps)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   501
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   502
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   503
fun tell_thm_deps ths =
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   504
  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
   505
    let
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   506
      val names = map Thm.name_of_thm ths \ "";
15570
8d8c70b41bab Move towards standard functions.
skalberg
parents: 15531
diff changeset
   507
      val deps = Symtab.keys (Library.foldl (uncurry Proofterm.thms_of_proof)
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   508
				    (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
   509
    in
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   510
      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
   511
      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
   512
    end);
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   513
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   514
in
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   515
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   516
fun setup_present_hook () =
15570
8d8c70b41bab Move towards standard functions.
skalberg
parents: 15531
diff changeset
   517
  Present.add_hook (fn _ => fn res => tell_thm_deps (List.concat (map #2 res)));
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   518
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   519
end;
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   520
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   521
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   522
(*** Preferences ***)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   523
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   524
local
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   525
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
   526
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
   527
					    ("max", string_of_int max)] []
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   528
val pgipbool       = XML.element "pgipbool" [] []
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   529
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   530
fun withdefault f = (f(), f)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   531
in
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   532
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   533
fun nat_option r = (pgipnat,
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   534
  withdefault (fn () => string_of_int (!r)),
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   535
  (fn s => (case Syntax.read_nat s of
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15472
diff changeset
   536
       NONE => error ("nat_option: illegal value " ^ s)
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15472
diff changeset
   537
     | SOME i => r := i)));
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   538
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   539
fun bool_option r = (pgipbool,
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   540
  withdefault (fn () => Bool.toString (!r)),
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   541
  (fn "false" => r := false | "true" => r := true
15173
e1582a0d29b5 Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents: 15156
diff changeset
   542
    | x => error ("bool_option: illegal value" ^ x)));
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   543
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   544
val proof_option = (pgipbool,
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   545
  withdefault (fn () => Bool.toString (!proofs >= 2)),
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   546
  (fn "false" => proofs := 1 | "true" => proofs := 2
15173
e1582a0d29b5 Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents: 15156
diff changeset
   547
    | x => error ("proof_option: illegal value" ^ x)));
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   548
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   549
val thm_deps_option = (pgipbool,
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   550
  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
   551
  (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
   552
    | "true" => print_mode := ("thm_deps" ins (!print_mode))
15173
e1582a0d29b5 Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents: 15156
diff changeset
   553
    | x => error ("thm_deps_option: illegal value " ^ x)));
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   554
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   555
local 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   556
    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
   557
    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
   558
in
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   559
val print_depth_option = (pgipnat,
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   560
  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
   561
  (fn s => (case Syntax.read_nat s of
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15472
diff changeset
   562
       NONE => error ("print_depth_option: illegal value" ^ s)
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15472
diff changeset
   563
     | SOME i => pg_print_depth i)))
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   564
end
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   565
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   566
val preferences = ref 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   567
  [("Display",
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   568
    [("show-types", 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   569
      ("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
   570
       bool_option show_types)),
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   571
     ("show-sorts", 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   572
      ("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
   573
       bool_option show_sorts)),
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   574
     ("show-consts", 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   575
      ("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
   576
       bool_option show_consts)),
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   577
     ("long-names", 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   578
      ("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
   579
     ("show-brackets", 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   580
      ("Show full bracketing in Isabelle terms",
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   581
       bool_option show_brackets)),
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   582
     ("show-main-goal", 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   583
      ("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
   584
     ("eta-contract", 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   585
      ("Print terms eta-contracted",
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   586
       bool_option Syntax.eta_contract))]),
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   587
   ("Advanced Display",
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   588
    [("goals-limit", 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   589
      ("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
   590
       nat_option goals_limit)),
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   591
     ("prems-limit", 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   592
      ("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
   593
       nat_option ProofContext.prems_limit)),
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   594
     ("print-depth", 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   595
      ("Setting for the ML print depth",
15472
4674102737e9 Added show_var_qmarks flag.
berghofe
parents: 15457
diff changeset
   596
       print_depth_option)),
15985
f00dd5e06ffe renamed show_var_qmarks to show_question_marks;
wenzelm
parents: 15964
diff changeset
   597
     ("show-question-marks",
15472
4674102737e9 Added show_var_qmarks flag.
berghofe
parents: 15457
diff changeset
   598
      ("Show leading question mark of variable name",
15985
f00dd5e06ffe renamed show_var_qmarks to show_question_marks;
wenzelm
parents: 15964
diff changeset
   599
       bool_option show_question_marks))]),
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   600
   ("Tracing",
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   601
    [("trace-simplifier", 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   602
      ("Trace simplification rules.",
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   603
       bool_option trace_simp)),
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   604
     ("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
   605
		      bool_option trace_rules)),
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   606
     ("trace-unification", 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   607
      ("Output error diagnostics during unification",
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   608
       bool_option Pattern.trace_unify_fail)),
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   609
     ("global-timing", 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   610
      ("Whether to enable timing in Isabelle.",
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   611
       bool_option Output.timing))]),
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   612
   ("Proof", 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   613
    [("quick-and-dirty", 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   614
      ("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
   615
       bool_option quick_and_dirty)),
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   616
     ("full-proofs", 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   617
      ("Record full proof objects internally",
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   618
       proof_option)),
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   619
     ("theorem-dependencies", 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   620
       ("Track theorem dependencies within Proof General",
15238
cb559bd0b03c Added entry in Settings menu for Toplevel.skip_proofs flag.
berghofe
parents: 15225
diff changeset
   621
	thm_deps_option)),
cb559bd0b03c Added entry in Settings menu for Toplevel.skip_proofs flag.
berghofe
parents: 15225
diff changeset
   622
     ("skip-proofs", 
cb559bd0b03c Added entry in Settings menu for Toplevel.skip_proofs flag.
berghofe
parents: 15225
diff changeset
   623
      ("Skip all proof scripts (interactive-only)",
cb559bd0b03c Added entry in Settings menu for Toplevel.skip_proofs flag.
berghofe
parents: 15225
diff changeset
   624
       bool_option Toplevel.skip_proofs))])
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   625
   ];
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   626
end
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   627
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   628
(* Configuration: GUI config, proverinfo messages *)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   629
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   630
local
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   631
    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
   632
    val name_attr = pair "name"
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   633
    val version_attr = pair "version"
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   634
    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
   635
in
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   636
fun send_pgip_config () =
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   637
    let 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   638
	val path = Path.unpack config_file
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   639
	val exists = File.exists path
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   640
	val proverinfo = 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   641
	    XML.element "proverinfo"
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   642
              [("name",Session.name()), ("version", version),
15208
09271a87fbf0 Add filenamextns to prover info. Update doc location. Add whitespace element in parseresult
aspinall
parents: 15192
diff changeset
   643
	       ("url", isabelle_www), ("filenameextns", ".thy;")]
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   644
	    [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
   645
	     XML.element "helpdoc" 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   646
         (* 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
   647
          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
   648
          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
   649
		      [("name", "Isabelle/HOL Tutorial"),
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   650
		       ("descr", "A Gentle Introduction to Isabelle/HOL"), 
15208
09271a87fbf0 Add filenamextns to prover info. Update doc location. Add whitespace element in parseresult
aspinall
parents: 15192
diff changeset
   651
		       ("url",  "http://isabelle.in.tum.de/dist/Isabelle2004/doc/tutorial.pdf")]
15134
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
    in
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   654
	if exists then
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   655
	    (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
   656
	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
   657
    end;
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   658
end
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   659
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   660
15629
4066f01f1beb Add askguise/informguise as best as easily possible. Prevent warning in openfile when file doesn't exist in theory database.
aspinall
parents: 15626
diff changeset
   661
(* Reveal some information about prover state *)
4066f01f1beb Add askguise/informguise as best as easily possible. Prevent warning in openfile when file doesn't exist in theory database.
aspinall
parents: 15626
diff changeset
   662
fun send_informguise (openfile, opentheory, openproofpos) =
4066f01f1beb Add askguise/informguise as best as easily possible. Prevent warning in openfile when file doesn't exist in theory database.
aspinall
parents: 15626
diff changeset
   663
    let val guisefile = 
4066f01f1beb Add askguise/informguise as best as easily possible. Prevent warning in openfile when file doesn't exist in theory database.
aspinall
parents: 15626
diff changeset
   664
	    case openfile of SOME f => [XML.element "guisefile" 
4066f01f1beb Add askguise/informguise as best as easily possible. Prevent warning in openfile when file doesn't exist in theory database.
aspinall
parents: 15626
diff changeset
   665
						    [("url",Url.pack (Url.File (Path.unpack f)))] []]
4066f01f1beb Add askguise/informguise as best as easily possible. Prevent warning in openfile when file doesn't exist in theory database.
aspinall
parents: 15626
diff changeset
   666
			   | _ => []
4066f01f1beb Add askguise/informguise as best as easily possible. Prevent warning in openfile when file doesn't exist in theory database.
aspinall
parents: 15626
diff changeset
   667
	val guisetheory = 
4066f01f1beb Add askguise/informguise as best as easily possible. Prevent warning in openfile when file doesn't exist in theory database.
aspinall
parents: 15626
diff changeset
   668
	    case opentheory of SOME t => [XML.element "guisetheory" [("thyname", t)] []]
4066f01f1beb Add askguise/informguise as best as easily possible. Prevent warning in openfile when file doesn't exist in theory database.
aspinall
parents: 15626
diff changeset
   669
			     | _ => []
4066f01f1beb Add askguise/informguise as best as easily possible. Prevent warning in openfile when file doesn't exist in theory database.
aspinall
parents: 15626
diff changeset
   670
	val guiseproof = 
4066f01f1beb Add askguise/informguise as best as easily possible. Prevent warning in openfile when file doesn't exist in theory database.
aspinall
parents: 15626
diff changeset
   671
	    case openproofpos of SOME i => [XML.element "guiseproof" [("proofpos", string_of_int i)] []]
4066f01f1beb Add askguise/informguise as best as easily possible. Prevent warning in openfile when file doesn't exist in theory database.
aspinall
parents: 15626
diff changeset
   672
			       | _ => []
4066f01f1beb Add askguise/informguise as best as easily possible. Prevent warning in openfile when file doesn't exist in theory database.
aspinall
parents: 15626
diff changeset
   673
    in 
4066f01f1beb Add askguise/informguise as best as easily possible. Prevent warning in openfile when file doesn't exist in theory database.
aspinall
parents: 15626
diff changeset
   674
	issue_pgips [XML.element "informguise" [] (guisefile @ guisetheory @ guiseproof)]
4066f01f1beb Add askguise/informguise as best as easily possible. Prevent warning in openfile when file doesn't exist in theory database.
aspinall
parents: 15626
diff changeset
   675
    end 
4066f01f1beb Add askguise/informguise as best as easily possible. Prevent warning in openfile when file doesn't exist in theory database.
aspinall
parents: 15626
diff changeset
   676
4066f01f1beb Add askguise/informguise as best as easily possible. Prevent warning in openfile when file doesn't exist in theory database.
aspinall
parents: 15626
diff changeset
   677
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   678
(* PGIP identifier tables (prover objects). [incomplete] *)
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
local
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   681
    val objtype_thy  = "theory"
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   682
    val objtype_thm  = "theorem"
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   683
    val objtype_term = "term"
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   684
    val objtype_type = "type"
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   685
		       
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   686
    fun xml_idtable ty ctx ids = 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   687
	let
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15472
diff changeset
   688
            fun ctx_attr (SOME c)= [("context", c)]
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15472
diff changeset
   689
              | ctx_attr NONE    = []
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   690
	    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
   691
	in 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   692
	    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
   693
	                          (map xmlid ids)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   694
	end
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   695
in
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   696
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   697
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
   698
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
   699
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
   700
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15472
diff changeset
   701
fun delallids ty = setids (xml_idtable ty NONE [])
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   702
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   703
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
   704
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
   705
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   706
fun send_thm_idtable ctx thy = 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   707
    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
   708
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   709
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
   710
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   711
(* 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
   712
   & maybe not so useful anyway *)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   713
	
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   714
end
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   715
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   716
(* 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
   717
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   718
local
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   719
 val topthy = Toplevel.theory_of o Toplevel.get_state
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15472
diff changeset
   720
 fun pthm thy name = print_thm (get_thm thy (name, NONE))
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   721
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   722
 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
   723
in
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15472
diff changeset
   724
fun askids (NONE, SOME "theory")  = send_thy_idtable NONE (ThyInfo.names())
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15472
diff changeset
   725
  | askids (NONE, NONE) =  send_thy_idtable NONE (ThyInfo.names())
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   726
                           (* only theories known in top context *)
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15472
diff changeset
   727
  | askids (SOME thy, SOME "theory") = send_thy_idtable (SOME thy) (ThyInfo.get_preds thy)
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15472
diff changeset
   728
  | askids (SOME thy, SOME "theorem") = send_thm_idtable (SOME thy) (ThyInfo.get_theory thy)
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15472
diff changeset
   729
  | askids (SOME thy, NONE) = (send_thy_idtable (SOME thy) (ThyInfo.get_preds thy);
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15472
diff changeset
   730
                               send_thm_idtable (SOME thy) (ThyInfo.get_theory thy)) 
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15472
diff changeset
   731
  | askids (_, SOME ot) = error ("No objects of type "^(quote ot)^" are available here.")
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   732
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   733
fun showid (_,        "theory", n) = 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   734
    with_displaywrap (idvalue "theory" n) (fn ()=>(print_theory (ThyInfo.get_theory n)))
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15472
diff changeset
   735
  | showid (SOME thy, "theorem", t) = 
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   736
    with_displaywrap (idvalue "theorem" t) (fn ()=>(pthm (ThyInfo.get_theory thy) t))
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15472
diff changeset
   737
  | showid (NONE,     "theorem", t) = 
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   738
    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
   739
  | 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
   740
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   741
end
15629
4066f01f1beb Add askguise/informguise as best as easily possible. Prevent warning in openfile when file doesn't exist in theory database.
aspinall
parents: 15626
diff changeset
   742
4066f01f1beb Add askguise/informguise as best as easily possible. Prevent warning in openfile when file doesn't exist in theory database.
aspinall
parents: 15626
diff changeset
   743
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   744
(** Parsing proof scripts without execution **)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   745
15146
eab7de0d0a31 Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents: 15145
diff changeset
   746
(* Notes.
eab7de0d0a31 Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents: 15145
diff changeset
   747
   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
   748
   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
   749
   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
   750
   the parsing to extract interesting parts of commands.  The trace of
15254
10cfd6a14682 Simplification to symbol processing; put quotes around theory name in message.
aspinall
parents: 15253
diff changeset
   751
   tokens parsed which is now recorded in each transition (added by
10cfd6a14682 Simplification to symbol processing; put quotes around theory name in message.
aspinall
parents: 15253
diff changeset
   752
   Markus June '04) helps do this, but the mechanism is still a bad mess.
15146
eab7de0d0a31 Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents: 15145
diff changeset
   753
   
15254
10cfd6a14682 Simplification to symbol processing; put quotes around theory name in message.
aspinall
parents: 15253
diff changeset
   754
   If we had proper parse trees it would be easy, although having a
10cfd6a14682 Simplification to symbol processing; put quotes around theory name in message.
aspinall
parents: 15253
diff changeset
   755
   fixed type of trees might be tricky with Isar's extensible parser.
15146
eab7de0d0a31 Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents: 15145
diff changeset
   756
eab7de0d0a31 Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents: 15145
diff changeset
   757
   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
   758
   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
   759
   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
   760
   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
   761
   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
   762
eab7de0d0a31 Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents: 15145
diff changeset
   763
    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
   764
eab7de0d0a31 Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents: 15145
diff changeset
   765
    val command_withmetainfo: string -> string -> string ->
eab7de0d0a31 Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents: 15145
diff changeset
   766
      (token list -> 
eab7de0d0a31 Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents: 15145
diff changeset
   767
       ((Toplevel.transition -> Toplevel.transition) * metainfo list) * 
eab7de0d0a31 Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents: 15145
diff changeset
   768
       token list) -> parser
15254
10cfd6a14682 Simplification to symbol processing; put quotes around theory name in message.
aspinall
parents: 15253
diff changeset
   769
10cfd6a14682 Simplification to symbol processing; put quotes around theory name in message.
aspinall
parents: 15253
diff changeset
   770
   We'd also like to render terms as they appear in output, but this
10cfd6a14682 Simplification to symbol processing; put quotes around theory name in message.
aspinall
parents: 15253
diff changeset
   771
   will be difficult because inner syntax is extensible and we don't 
10cfd6a14682 Simplification to symbol processing; put quotes around theory name in message.
aspinall
parents: 15253
diff changeset
   772
   have the correct syntax to hand when just doing outer parsing
10cfd6a14682 Simplification to symbol processing; put quotes around theory name in message.
aspinall
parents: 15253
diff changeset
   773
   without execution.  A reasonable approximation could 
10cfd6a14682 Simplification to symbol processing; put quotes around theory name in message.
aspinall
parents: 15253
diff changeset
   774
   perhaps be obtained by using the syntax of the current context.
10cfd6a14682 Simplification to symbol processing; put quotes around theory name in message.
aspinall
parents: 15253
diff changeset
   775
   However, this would mean more mess trying to pick out terms, 
10cfd6a14682 Simplification to symbol processing; put quotes around theory name in message.
aspinall
parents: 15253
diff changeset
   776
   so at this stage a more serious change to the Isar functions
10cfd6a14682 Simplification to symbol processing; put quotes around theory name in message.
aspinall
parents: 15253
diff changeset
   777
   seems necessary.
15146
eab7de0d0a31 Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents: 15145
diff changeset
   778
*)
eab7de0d0a31 Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents: 15145
diff changeset
   779
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   780
local
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   781
    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
   782
    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
   783
    fun empty elt = [XML.element elt [] []]
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   784
15210
4ff917a91e16 Remove double escaping of backslash in PGML. Remove use of character refs in <whitespace>
aspinall
parents: 15208
diff changeset
   785
    fun whitespace str = XML.element "whitespace" [] [XML.text str]
15208
09271a87fbf0 Add filenamextns to prover info. Update doc location. Add whitespace element in parseresult
aspinall
parents: 15192
diff changeset
   786
15146
eab7de0d0a31 Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents: 15145
diff changeset
   787
    (* 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
   788
    val sync = OuterSyntax.scan "\\<^sync>";
eab7de0d0a31 Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents: 15145
diff changeset
   789
eab7de0d0a31 Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents: 15145
diff changeset
   790
    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
   791
	let 
15146
eab7de0d0a31 Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents: 15145
diff changeset
   792
	    val name = (fst (nameP (toks@sync)))
eab7de0d0a31 Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents: 15145
diff changeset
   793
			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
   794
					    "(objtype: " ^ objtyp ^ ")");
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   795
				     "")
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   796
				     
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   797
	in 
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   798
	    [XML.element elt 
15146
eab7de0d0a31 Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents: 15145
diff changeset
   799
			 ((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
   800
			  (if objtyp="" then [] else [("objtype", objtyp)]))
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   801
			 ([XML.text str])]
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   802
	end
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   803
15146
eab7de0d0a31 Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents: 15145
diff changeset
   804
    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
   805
    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
   806
 
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   807
    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
   808
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   809
    (* 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
   810
       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
   811
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15472
diff changeset
   812
    val keywords_classification_table = ref (NONE:(string Symtab.table) option)
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   813
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   814
    fun get_keywords_classification_table () = 
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   815
	case (!keywords_classification_table) of
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15472
diff changeset
   816
	    SOME t => t
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15472
diff changeset
   817
	  | NONE => (let
15570
8d8c70b41bab Move towards standard functions.
skalberg
parents: 15531
diff changeset
   818
			 val tab = Library.foldl (fn (tab,(c,_,k,_))=>Symtab.update((c,k),tab)) 
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   819
					 (Symtab.empty,OuterSyntax.dest_parsers())
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15472
diff changeset
   820
		     in (keywords_classification_table := SOME tab; tab) end)
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   821
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   822
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   823
		    
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   824
    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
   825
	let 
15146
eab7de0d0a31 Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents: 15145
diff changeset
   826
	    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
   827
	in 
15192
294f2eb211dd Tweak parentnames attribute on opentheory
aspinall
parents: 15191
diff changeset
   828
	    markup_text_attrs str "opentheory" 
294f2eb211dd Tweak parentnames attribute on opentheory
aspinall
parents: 15191
diff changeset
   829
			      ([("thyname",thyname)] @
294f2eb211dd Tweak parentnames attribute on opentheory
aspinall
parents: 15191
diff changeset
   830
			       (if imports=[] then [] else
294f2eb211dd Tweak parentnames attribute on opentheory
aspinall
parents: 15191
diff changeset
   831
				[("parentnames", (space_implode ";" imports) ^ ";")]))
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   832
	end 
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   833
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   834
    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
   835
	let 
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   836
	    (* 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
   837
	       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
   838
	       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
   839
	       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
   840
	       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
   841
	       instead of reconstructing it here. *)
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   842
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   843
	    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
   844
		["defaultsort","arities","judgement","finalconsts",
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   845
		 "syntax", "nonterminals", "translations",
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   846
		 "global", "local", "hide",
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   847
		 "ML_setup", "setup", "method_setup",
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   848
		 "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
   849
		 "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
   850
		 "oracle",
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   851
		 "declare"]
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   852
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   853
	    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
   854
	    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
   855
	    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
   856
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   857
	    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
   858
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   859
	    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
   860
		let 
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   861
		    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
   862
		    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
   863
		in 
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   864
		    theoremsP
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   865
		end
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   866
	in 
15254
10cfd6a14682 Simplification to symbol processing; put quotes around theory name in message.
aspinall
parents: 15253
diff changeset
   867
	    (* TODO: ideally we would like to render terms properly, just as they are
10cfd6a14682 Simplification to symbol processing; put quotes around theory name in message.
aspinall
parents: 15253
diff changeset
   868
	       in output. This implies using PGML for symbols and variables/atoms. 
10cfd6a14682 Simplification to symbol processing; put quotes around theory name in message.
aspinall
parents: 15253
diff changeset
   869
	       BUT it's rather tricky without having the correct concrete syntax to hand,
10cfd6a14682 Simplification to symbol processing; put quotes around theory name in message.
aspinall
parents: 15253
diff changeset
   870
	       and even if we did, we'd have to mess around here a whole lot more first
10cfd6a14682 Simplification to symbol processing; put quotes around theory name in message.
aspinall
parents: 15253
diff changeset
   871
	       to pick out the terms from the syntax. *)
10cfd6a14682 Simplification to symbol processing; put quotes around theory name in message.
aspinall
parents: 15253
diff changeset
   872
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   873
	    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
   874
	    else case name of
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   875
		     "text"      => comment_item
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   876
		   | "text_raw"  => comment_item
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   877
		   | "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
   878
		   | "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
   879
		   | "classes"   => named_item P.name "class"
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   880
		   | "classrel"  => named_item P.name "class"
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   881
		   | "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
   882
		   | "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
   883
		   | "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
   884
		   | "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
   885
		   | "theorems"  => named_item thmnameP "thmset"
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   886
		   | "lemmas"    => named_item thmnameP "thmset"
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   887
		   | "oracle"    => named_item P.name "oracle"
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   888
		   | "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
   889
		   | _ => (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
   890
	end
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   891
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   892
    fun xmls_of_thy_goal (name,toks,str) = 
15225
68ab0f4eb457 Add openblock/closeblock to other opengoal/closegoal elements
aspinall
parents: 15220
diff changeset
   893
	let 
68ab0f4eb457 Add openblock/closeblock to other opengoal/closegoal elements
aspinall
parents: 15220
diff changeset
   894
	    (* see isar_syn.ML/gen_theorem *)
15146
eab7de0d0a31 Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents: 15145
diff changeset
   895
         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
   896
	 val general_statement =
eab7de0d0a31 Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents: 15145
diff changeset
   897
	    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
   898
	    
eab7de0d0a31 Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents: 15145
diff changeset
   899
	    val gen_theoremP =
eab7de0d0a31 Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents: 15145
diff changeset
   900
		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
   901
                 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
   902
				 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
   903
							 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
   904
eab7de0d0a31 Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents: 15145
diff changeset
   905
	    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
   906
	    (* TODO: add preference values for attributes 
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   907
	       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
   908
	    *)
15225
68ab0f4eb457 Add openblock/closeblock to other opengoal/closegoal elements
aspinall
parents: 15220
diff changeset
   909
	in 
68ab0f4eb457 Add openblock/closeblock to other opengoal/closegoal elements
aspinall
parents: 15220
diff changeset
   910
	    (thmnamed_item_elt toks str "opengoal" nameP "") @
68ab0f4eb457 Add openblock/closeblock to other opengoal/closegoal elements
aspinall
parents: 15220
diff changeset
   911
	    (empty "openblock")
68ab0f4eb457 Add openblock/closeblock to other opengoal/closegoal elements
aspinall
parents: 15220
diff changeset
   912
	end
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   913
15225
68ab0f4eb457 Add openblock/closeblock to other opengoal/closegoal elements
aspinall
parents: 15220
diff changeset
   914
    fun xmls_of_qed (name,markup) = (case name of
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   915
      "sorry"         => markup "giveupgoal"
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   916
    | "oops"          => markup "postponegoal"
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   917
    | "done"          => markup "closegoal" 
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   918
    | "by"            => markup "closegoal"  (* nested or toplevel *)
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   919
    | "qed"           => markup "closegoal"  (* nested or toplevel *)
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   920
    | "."	      => markup "closegoal"  (* nested or toplevel *)
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   921
    | ".."	      => markup "closegoal"  (* nested or toplevel *)
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   922
    | other => (* default to closegoal: may be wrong for extns *)
15225
68ab0f4eb457 Add openblock/closeblock to other opengoal/closegoal elements
aspinall
parents: 15220
diff changeset
   923
      (parse_warning ("Unrecognized qed command: " ^ quote other); markup "closegoal"))
68ab0f4eb457 Add openblock/closeblock to other opengoal/closegoal elements
aspinall
parents: 15220
diff changeset
   924
	@ (empty "closeblock")
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   925
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   926
    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
   927
    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
   928
    case kind of
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   929
      "control"        => markup "badcmd"
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   930
    | "diag"           => markup "spuriouscmd"
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   931
    (* theory/files *)
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   932
    | "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
   933
    | "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
   934
    | "theory-heading" => markup "litcomment"
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   935
    | "theory-script"  => markup "theorystep"
15146
eab7de0d0a31 Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents: 15145
diff changeset
   936
    | "theory-end"     => markup "closetheory"
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   937
    (* proof control *)
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   938
    | "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
   939
    | "proof-heading"  => markup "litcomment"
15225
68ab0f4eb457 Add openblock/closeblock to other opengoal/closegoal elements
aspinall
parents: 15220
diff changeset
   940
    | "proof-goal"     => (markup "opengoal") @ (empty "openblock")  (* nested proof: have, show, ... *)
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   941
    | "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
   942
    | "proof-open"     => (empty "openblock") @ (markup "proofstep")
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   943
    | "proof-close"    => (markup "proofstep") @ (empty "closeblock")
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   944
    | "proof-script"   => markup "proofstep"
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   945
    | "proof-chain"    => markup "proofstep"
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   946
    | "proof-decl"     => markup "proofstep"
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   947
    | "proof-asm"      => markup "proofstep"
15289
1d2dba93ef08 Markup obtain as introducing a nested goal.
aspinall
parents: 15286
diff changeset
   948
    | "proof-asm-goal" => (markup "opengoal") @ (empty "openblock")  (* nested proof: obtain *)
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   949
    | "qed"            => xmls_of_qed (name,markup)
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   950
    | "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
   951
    | "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
   952
    | 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
   953
      (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
   954
       markup "spuriouscmd")
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   955
    end 
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   956
in
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   957
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   958
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
   959
   let 
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   960
       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
   961
   in case classification of
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15472
diff changeset
   962
	  SOME k => (xmls_of_kind k (name,toks,str))
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15472
diff changeset
   963
	| NONE => (* an uncategorized keyword ignored for undo (maybe wrong) *)
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   964
	  (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
   965
	   markup_text str "spuriouscmd")
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   966
   end 
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   967
15191
5ca1fd9dec83 Support parsing of -- {* comments *}. Add extra output channels.
aspinall
parents: 15173
diff changeset
   968
fun markup_toks [] _ = []
5ca1fd9dec83 Support parsing of -- {* comments *}. Add extra output channels.
aspinall
parents: 15173
diff changeset
   969
  | markup_toks toks x = markup_text (implode (map OuterLex.unparse toks)) x
5ca1fd9dec83 Support parsing of -- {* comments *}. Add extra output channels.
aspinall
parents: 15173
diff changeset
   970
5ca1fd9dec83 Support parsing of -- {* comments *}. Add extra output channels.
aspinall
parents: 15173
diff changeset
   971
fun markup_comment_whs [] = []
5ca1fd9dec83 Support parsing of -- {* comments *}. Add extra output channels.
aspinall
parents: 15173
diff changeset
   972
  | markup_comment_whs (toks as t::ts) = (* this would be a lot neater if we could match on toks! *)
5ca1fd9dec83 Support parsing of -- {* comments *}. Add extra output channels.
aspinall
parents: 15173
diff changeset
   973
    let 
5ca1fd9dec83 Support parsing of -- {* comments *}. Add extra output channels.
aspinall
parents: 15173
diff changeset
   974
	val (prewhs,rest) = take_prefix (OuterLex.is_kind OuterLex.Space) toks
5ca1fd9dec83 Support parsing of -- {* comments *}. Add extra output channels.
aspinall
parents: 15173
diff changeset
   975
    in 
5ca1fd9dec83 Support parsing of -- {* comments *}. Add extra output channels.
aspinall
parents: 15173
diff changeset
   976
	if (prewhs <> []) then
15210
4ff917a91e16 Remove double escaping of backslash in PGML. Remove use of character refs in <whitespace>
aspinall
parents: 15208
diff changeset
   977
	    whitespace (implode (map OuterLex.unparse prewhs))
15191
5ca1fd9dec83 Support parsing of -- {* comments *}. Add extra output channels.
aspinall
parents: 15173
diff changeset
   978
	    :: (markup_comment_whs rest)
5ca1fd9dec83 Support parsing of -- {* comments *}. Add extra output channels.
aspinall
parents: 15173
diff changeset
   979
	else 
5ca1fd9dec83 Support parsing of -- {* comments *}. Add extra output channels.
aspinall
parents: 15173
diff changeset
   980
	    (markup_text (OuterLex.unparse t) "comment") @
5ca1fd9dec83 Support parsing of -- {* comments *}. Add extra output channels.
aspinall
parents: 15173
diff changeset
   981
	    (markup_comment_whs ts)
5ca1fd9dec83 Support parsing of -- {* comments *}. Add extra output channels.
aspinall
parents: 15173
diff changeset
   982
    end
5ca1fd9dec83 Support parsing of -- {* comments *}. Add extra output channels.
aspinall
parents: 15173
diff changeset
   983
5ca1fd9dec83 Support parsing of -- {* comments *}. Add extra output channels.
aspinall
parents: 15173
diff changeset
   984
fun xmls_pre_cmd [] = ([],[])
5ca1fd9dec83 Support parsing of -- {* comments *}. Add extra output channels.
aspinall
parents: 15173
diff changeset
   985
  | xmls_pre_cmd toks = 
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   986
    let 
15191
5ca1fd9dec83 Support parsing of -- {* comments *}. Add extra output channels.
aspinall
parents: 15173
diff changeset
   987
	(* an extra token is needed to terminate the command *)
5ca1fd9dec83 Support parsing of -- {* comments *}. Add extra output channels.
aspinall
parents: 15173
diff changeset
   988
	val sync = OuterSyntax.scan "\\<^sync>";
5ca1fd9dec83 Support parsing of -- {* comments *}. Add extra output channels.
aspinall
parents: 15173
diff changeset
   989
	val spaceP = Scan.bulk (Scan.one (fn t =>not (OuterLex.is_proper t)) >> OuterLex.val_of) >> implode
5ca1fd9dec83 Support parsing of -- {* comments *}. Add extra output channels.
aspinall
parents: 15173
diff changeset
   990
	val text_with_whs = 
5ca1fd9dec83 Support parsing of -- {* comments *}. Add extra output channels.
aspinall
parents: 15173
diff changeset
   991
	    ((spaceP || Scan.succeed "") --
5ca1fd9dec83 Support parsing of -- {* comments *}. Add extra output channels.
aspinall
parents: 15173
diff changeset
   992
	     (P.short_ident || P.long_ident || P.sym_ident || P.string || P.number || P.verbatim) >> op^)
5ca1fd9dec83 Support parsing of -- {* comments *}. Add extra output channels.
aspinall
parents: 15173
diff changeset
   993
	     -- (spaceP || Scan.succeed "") >> op^
5ca1fd9dec83 Support parsing of -- {* comments *}. Add extra output channels.
aspinall
parents: 15173
diff changeset
   994
	val (prewhs,rest1) = take_prefix (not o OuterLex.is_proper) (toks@sync)
5ca1fd9dec83 Support parsing of -- {* comments *}. Add extra output channels.
aspinall
parents: 15173
diff changeset
   995
        (* NB: this collapses  litcomment,(litcomment|whitespace)* to a single litcomment *)
5ca1fd9dec83 Support parsing of -- {* comments *}. Add extra output channels.
aspinall
parents: 15173
diff changeset
   996
	val (_,rest2) = (Scan.bulk (P.$$$ "--" |-- text_with_whs) >> implode || Scan.succeed "") rest1
5ca1fd9dec83 Support parsing of -- {* comments *}. Add extra output channels.
aspinall
parents: 15173
diff changeset
   997
	val (postwhs,rest3) = take_prefix (not o OuterLex.is_proper) rest2
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   998
    in
15191
5ca1fd9dec83 Support parsing of -- {* comments *}. Add extra output channels.
aspinall
parents: 15173
diff changeset
   999
	((markup_comment_whs prewhs) @
5ca1fd9dec83 Support parsing of -- {* comments *}. Add extra output channels.
aspinall
parents: 15173
diff changeset
  1000
	 (if (length rest2 = length rest1)  then []
5ca1fd9dec83 Support parsing of -- {* comments *}. Add extra output channels.
aspinall
parents: 15173
diff changeset
  1001
	  else markup_text (implode 
15570
8d8c70b41bab Move towards standard functions.
skalberg
parents: 15531
diff changeset
  1002
				(map OuterLex.unparse (Library.take (length rest1 - length rest2, rest1))))
15191
5ca1fd9dec83 Support parsing of -- {* comments *}. Add extra output channels.
aspinall
parents: 15173
diff changeset
  1003
	       "litcomment") @
5ca1fd9dec83 Support parsing of -- {* comments *}. Add extra output channels.
aspinall
parents: 15173
diff changeset
  1004
	 (markup_comment_whs postwhs),
15570
8d8c70b41bab Move towards standard functions.
skalberg
parents: 15531
diff changeset
  1005
	 Library.take (length rest3 - 1,rest3))
15191
5ca1fd9dec83 Support parsing of -- {* comments *}. Add extra output channels.
aspinall
parents: 15173
diff changeset
  1006
    end
5ca1fd9dec83 Support parsing of -- {* comments *}. Add extra output channels.
aspinall
parents: 15173
diff changeset
  1007
5ca1fd9dec83 Support parsing of -- {* comments *}. Add extra output channels.
aspinall
parents: 15173
diff changeset
  1008
fun xmls_of_impropers toks = 
5ca1fd9dec83 Support parsing of -- {* comments *}. Add extra output channels.
aspinall
parents: 15173
diff changeset
  1009
    let 
5ca1fd9dec83 Support parsing of -- {* comments *}. Add extra output channels.
aspinall
parents: 15173
diff changeset
  1010
	val (xmls,rest) = xmls_pre_cmd toks
5ca1fd9dec83 Support parsing of -- {* comments *}. Add extra output channels.
aspinall
parents: 15173
diff changeset
  1011
    in
5ca1fd9dec83 Support parsing of -- {* comments *}. Add extra output channels.
aspinall
parents: 15173
diff changeset
  1012
	xmls @ (markup_toks rest "unparseable")
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1013
    end
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1014
    
15173
e1582a0d29b5 Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents: 15156
diff changeset
  1015
fun markup_unparseable str = markup_text str "unparseable" 
e1582a0d29b5 Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents: 15156
diff changeset
  1016
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1017
end
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1018
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1019
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1020
local
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1021
    (* 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
  1022
       to reconstruct the input. *)
15191
5ca1fd9dec83 Support parsing of -- {* comments *}. Add extra output channels.
aspinall
parents: 15173
diff changeset
  1023
    (* TODO: see if duplicating isar_output/parse_thy can help here *)
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1024
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1025
    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
  1026
      | 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
  1027
	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
  1028
	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
  1029
      | 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
  1030
in
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1031
    fun xmls_of_str str =
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1032
    let 
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1033
       (* 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
  1034
       fun parse_loop ([],[],xmls) = xmls
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1035
	 | 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
  1036
	 | 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
  1037
	   let 
15191
5ca1fd9dec83 Support parsing of -- {* comments *}. Add extra output channels.
aspinall
parents: 15173
diff changeset
  1038
	       (* first proper token after whitespace/litcomment/whitespace is command *)
5ca1fd9dec83 Support parsing of -- {* comments *}. Add extra output channels.
aspinall
parents: 15173
diff changeset
  1039
	       val (xmls_pre_cmd,cmditoks') = xmls_pre_cmd itoks
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1040
	       val (cmdtok,itoks') = case cmditoks' of x::xs => (x,xs)
15191
5ca1fd9dec83 Support parsing of -- {* comments *}. Add extra output channels.
aspinall
parents: 15173
diff changeset
  1041
						     | _ => error("proof_general/parse_loop impossible") 
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1042
	       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
  1043
               (* 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
  1044
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1045
	       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
  1046
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1047
	       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
  1048
	   in
15191
5ca1fd9dec83 Support parsing of -- {* comments *}. Add extra output channels.
aspinall
parents: 15173
diff changeset
  1049
	       parse_loop(trs,itoks'',xmls @ xmls_pre_cmd @ xmls_tr)
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1050
	   end
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1051
    in
15173
e1582a0d29b5 Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents: 15156
diff changeset
  1052
	(let val toks = OuterSyntax.scan str
e1582a0d29b5 Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents: 15156
diff changeset
  1053
	 in 
e1582a0d29b5 Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents: 15156
diff changeset
  1054
	     parse_loop (OuterSyntax.read toks, toks, [])
e1582a0d29b5 Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents: 15156
diff changeset
  1055
	 end)
e1582a0d29b5 Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents: 15156
diff changeset
  1056
 	   handle _ => markup_unparseable str
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1057
    end
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1058
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1059
15173
e1582a0d29b5 Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents: 15156
diff changeset
  1060
fun parsescript str attrs = 
e1582a0d29b5 Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents: 15156
diff changeset
  1061
    let 
e1582a0d29b5 Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents: 15156
diff changeset
  1062
	val _ = start_delay_msgs ()  (* accumulate error messages to put inside parseresult *)
e1582a0d29b5 Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents: 15156
diff changeset
  1063
	val xmls = xmls_of_str str
e1582a0d29b5 Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents: 15156
diff changeset
  1064
        val errs = end_delayed_msgs ()
e1582a0d29b5 Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents: 15156
diff changeset
  1065
     in 
e1582a0d29b5 Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents: 15156
diff changeset
  1066
	issue_pgips [XML.element "parseresult" attrs (errs@xmls)]
e1582a0d29b5 Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents: 15156
diff changeset
  1067
    end
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1068
end
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1069
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1070
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1071
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1072
(**** PGIP:  Isabelle -> Interface ****)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1073
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1074
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
  1075
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
  1076
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1077
fun usespgip () = 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1078
    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
  1079
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1080
fun usespgml () = 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1081
    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
  1082
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1083
fun hasprefs () = 
15570
8d8c70b41bab Move towards standard functions.
skalberg
parents: 15531
diff changeset
  1084
    List.app (fn (prefcat, prefs) =>
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1085
	    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
  1086
		 (map (fn (name, (descr, (ty, (default,_),_))) => 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1087
		       XML.element "haspref" [("name", name), 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1088
					      ("descr", descr), 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1089
					      ("default", default)]
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1090
		       [ty]) prefs)]) (!preferences);
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1091
15570
8d8c70b41bab Move towards standard functions.
skalberg
parents: 15531
diff changeset
  1092
fun allprefs () = Library.foldl (op @) ([], map snd (!preferences))
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1093
	
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1094
fun setpref name value = 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1095
    (case assoc (allprefs(), name) of
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15472
diff changeset
  1096
	 NONE => warning ("Unknown pref: " ^ quote name)
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15472
diff changeset
  1097
       | SOME (_, (_, _, set)) => set value);
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1098
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1099
fun getpref name = 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1100
    (case assoc (allprefs(), name) of
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15472
diff changeset
  1101
	 NONE => warning ("Unknown pref: " ^ quote name)
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15472
diff changeset
  1102
       | SOME (_, (_, (_,get), _)) => 
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1103
	   issue_pgip "prefval" [("name", name)] (get ()));
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1104
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1105
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1106
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1107
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1108
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1109
(**** PGIP:  Interface -> Isabelle/Isar ****)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1110
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1111
exception PGIP of string;
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1112
exception PGIP_QUIT;
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1113
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1114
(* Sending commands to Isar *)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1115
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1116
fun isarcmd s = 
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1117
    s |> OuterSyntax.scan |> OuterSyntax.read 
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1118
      |> 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
  1119
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1120
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
  1121
  | xmltext [] = ""
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1122
  | 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
  1123
			
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1124
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
  1125
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1126
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1127
(* 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
  1128
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1129
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
  1130
    let
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1131
	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
  1132
    in
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1133
	case extn of
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1134
	    "" => 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
  1135
	  | "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
  1136
	  | "ML" => isarcmd ("use " ^ quote file)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1137
	  (* 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
  1138
	  | 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
  1139
    end  
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1140
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1141
15173
e1582a0d29b5 Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents: 15156
diff changeset
  1142
(* Proof control commands *)
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1143
15173
e1582a0d29b5 Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents: 15156
diff changeset
  1144
local
e1582a0d29b5 Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents: 15156
diff changeset
  1145
  fun xmlattro attr attrs = assoc(attrs,attr)
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1146
15173
e1582a0d29b5 Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents: 15156
diff changeset
  1147
  fun xmlattr attr attrs = 
e1582a0d29b5 Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents: 15156
diff changeset
  1148
      (case xmlattro attr attrs of 
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15472
diff changeset
  1149
	   SOME value => value 
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15472
diff changeset
  1150
	 | NONE => raise PGIP ("Missing attribute: " ^ attr))
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1151
15173
e1582a0d29b5 Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents: 15156
diff changeset
  1152
  val thyname_attro = xmlattro "thyname"
e1582a0d29b5 Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents: 15156
diff changeset
  1153
  val thyname_attr = xmlattr "thyname"
e1582a0d29b5 Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents: 15156
diff changeset
  1154
  val objtype_attro = xmlattro "objtype"
e1582a0d29b5 Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents: 15156
diff changeset
  1155
  val objtype_attr = xmlattr "objtype"
e1582a0d29b5 Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents: 15156
diff changeset
  1156
  val name_attr = xmlattr "name"
e1582a0d29b5 Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents: 15156
diff changeset
  1157
  val dirname_attr = xmlattr "dir"
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1158
  fun comment x = "(* " ^ x ^ " *)"
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1159
15173
e1582a0d29b5 Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents: 15156
diff changeset
  1160
  fun localfile_of_url url = (* only handle file:/// or file://localhost/ *)
e1582a0d29b5 Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents: 15156
diff changeset
  1161
      case Url.unpack url of
e1582a0d29b5 Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents: 15156
diff changeset
  1162
	  (Url.File path) => File.sysify_path path
e1582a0d29b5 Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents: 15156
diff changeset
  1163
	| _ => error ("Cannot access non-local URL " ^ url)
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1164
15173
e1582a0d29b5 Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents: 15156
diff changeset
  1165
  val fileurl_of = localfile_of_url o (xmlattr "url")
15134
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
  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
  1168
  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
  1169
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15472
diff changeset
  1170
  val currently_open_file = ref (NONE : string option)
15629
4066f01f1beb Add askguise/informguise as best as easily possible. Prevent warning in openfile when file doesn't exist in theory database.
aspinall
parents: 15626
diff changeset
  1171
4066f01f1beb Add askguise/informguise as best as easily possible. Prevent warning in openfile when file doesn't exist in theory database.
aspinall
parents: 15626
diff changeset
  1172
  val topnode = Toplevel.node_of o Toplevel.get_state
4066f01f1beb Add askguise/informguise as best as easily possible. Prevent warning in openfile when file doesn't exist in theory database.
aspinall
parents: 15626
diff changeset
  1173
  fun topproofpos () = (case topnode() of Toplevel.Proof ph => SOME(ProofHistory.position ph) 
4066f01f1beb Add askguise/informguise as best as easily possible. Prevent warning in openfile when file doesn't exist in theory database.
aspinall
parents: 15626
diff changeset
  1174
					| _ => NONE) handle Toplevel.UNDEF => NONE
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1175
in
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1176
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1177
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
  1178
  (XML.Text t) => warning ("Ignored text in PGIP packet: \n" ^ t)
15173
e1582a0d29b5 Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents: 15156
diff changeset
  1179
| (xml as (XML.Elem (elem, attrs, data))) => 
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1180
  (case elem of
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1181
       (* protocol config *)
15191
5ca1fd9dec83 Support parsing of -- {* comments *}. Add extra output channels.
aspinall
parents: 15173
diff changeset
  1182
       "askpgip"  	=> (pgip_emacs_compatibility_flag:=false; (* PG>=3.6 or other PGIP interface *)
5ca1fd9dec83 Support parsing of -- {* comments *}. Add extra output channels.
aspinall
parents: 15173
diff changeset
  1183
			    usespgip (); send_pgip_config ())
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1184
     | "askpgml"  	=> usespgml ()
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1185
     (* proverconfig *)
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1186
     | "askprefs" 	=> hasprefs ()
15173
e1582a0d29b5 Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents: 15156
diff changeset
  1187
     | "getpref"  	=> getpref (name_attr attrs)
e1582a0d29b5 Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents: 15156
diff changeset
  1188
     | "setpref"  	=> setpref (name_attr attrs) (xmltext data)
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1189
     (* provercontrol *)
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1190
     | "proverinit" 	=> isar_restart ()
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1191
     | "proverexit" 	=> isarcmd "quit"
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1192
     | "startquiet" 	=> isarcmd "disable_pr"
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1193
     | "stopquiet"  	=> isarcmd "enable_pr"
15403
9e58e666074d Fix pgmlsymbolson/off.
aspinall
parents: 15401
diff changeset
  1194
     | "pgmlsymbolson"   => (print_mode := !print_mode @ ["xsymbols"])
9e58e666074d Fix pgmlsymbolson/off.
aspinall
parents: 15401
diff changeset
  1195
     | "pgmlsymbolsoff"  => (print_mode := (!print_mode \ "xsymbols"))
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1196
     (* properproofcmd: proper commands which belong in script *)
15401
ba28d103bada Support PGIP <whitespace>, <dostep>, <doitem> elements as input
aspinall
parents: 15400
diff changeset
  1197
     (* FIXME: next ten are by Eclipse interface, can be removed in favour of dostep *)
15629
4066f01f1beb Add askguise/informguise as best as easily possible. Prevent warning in openfile when file doesn't exist in theory database.
aspinall
parents: 15626
diff changeset
  1198
     (* NB: Isar doesn't make lemma name of goal accessible during proof *)
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1199
     | "opengoal"       => isarscript data
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1200
     | "proofstep"      => isarscript data
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1201
     | "closegoal"      => isarscript data
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1202
     | "giveupgoal"     => isarscript data
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1203
     | "postponegoal"   => isarscript data
15191
5ca1fd9dec83 Support parsing of -- {* comments *}. Add extra output channels.
aspinall
parents: 15173
diff changeset
  1204
     | "comment"	=> isarscript data  (* NB: should be ignored, but process anyway *)
15401
ba28d103bada Support PGIP <whitespace>, <dostep>, <doitem> elements as input
aspinall
parents: 15400
diff changeset
  1205
     | "whitespace"	=> isarscript data  (* NB: should be ignored, but process anyway *)
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1206
     | "litcomment"     => isarscript data
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1207
     | "spuriouscmd"    => isarscript data
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1208
     | "badcmd"		=> isarscript data
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1209
     (* improperproofcmd: improper commands which *do not* belong in script *)
15401
ba28d103bada Support PGIP <whitespace>, <dostep>, <doitem> elements as input
aspinall
parents: 15400
diff changeset
  1210
     | "dostep"         => isarscript data
15286
b084384960d1 Add <undoitem> for theory-state undos.
aspinall
parents: 15268
diff changeset
  1211
     | "undostep"       => isarcmd "undos_proof 1"
15626
a8f718939500 Support new PGIP commands redostep, redoitem
aspinall
parents: 15570
diff changeset
  1212
     | "redostep"       => isarcmd "redo"
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1213
     | "abortgoal"      => isarcmd "ProofGeneral.kill_proof"  
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1214
     | "forget"         => error "Not implemented" 
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1215
     | "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
  1216
     (* proofctxt: improper commands *)
15173
e1582a0d29b5 Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents: 15156
diff changeset
  1217
     | "askids"         => askids (thyname_attro attrs, objtype_attro attrs)
e1582a0d29b5 Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents: 15156
diff changeset
  1218
     | "showid"	        => showid (thyname_attro attrs, objtype_attr attrs, name_attr attrs)
15629
4066f01f1beb Add askguise/informguise as best as easily possible. Prevent warning in openfile when file doesn't exist in theory database.
aspinall
parents: 15626
diff changeset
  1219
     | "askguise"	=> send_informguise (!currently_open_file,
4066f01f1beb Add askguise/informguise as best as easily possible. Prevent warning in openfile when file doesn't exist in theory database.
aspinall
parents: 15626
diff changeset
  1220
					     SOME (topthy_name()) handle Toplevel.UNDEF => NONE,
4066f01f1beb Add askguise/informguise as best as easily possible. Prevent warning in openfile when file doesn't exist in theory database.
aspinall
parents: 15626
diff changeset
  1221
					     topproofpos())
15173
e1582a0d29b5 Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents: 15156
diff changeset
  1222
     | "parsescript"    => parsescript (xmltext data) attrs (* just pass back attrs unchanged *)
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1223
     | "showproofstate" => isarcmd "pr"
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1224
     | "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
  1225
     | "searchtheorems" => isarcmd ("thms_containing " ^ (xmltext data))
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1226
     | "setlinewidth"   => isarcmd ("pretty_setmargin " ^ (xmltext data))
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1227
     | "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
  1228
     (* properfilecmd: proper theory-level script commands *)
15401
ba28d103bada Support PGIP <whitespace>, <dostep>, <doitem> elements as input
aspinall
parents: 15400
diff changeset
  1229
     (* FIXME: next three are sent by Eclipse, can be removed in favour of doitem *)
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1230
     | "opentheory"     => isarscript data
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1231
     | "theoryitem"     => isarscript data
15253
6e20cc79bde6 Fix <closetheory>
aspinall
parents: 15238
diff changeset
  1232
     | "closetheory"    => let 
6e20cc79bde6 Fix <closetheory>
aspinall
parents: 15238
diff changeset
  1233
			      val thyname = topthy_name()
6e20cc79bde6 Fix <closetheory>
aspinall
parents: 15238
diff changeset
  1234
			   in (isarscript data;
15254
10cfd6a14682 Simplification to symbol processing; put quotes around theory name in message.
aspinall
parents: 15253
diff changeset
  1235
			       writeln ("Theory \""^thyname^"\" completed."))
15253
6e20cc79bde6 Fix <closetheory>
aspinall
parents: 15238
diff changeset
  1236
			   end
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1237
     (* improperfilecmd: theory-level commands not in script *)
15401
ba28d103bada Support PGIP <whitespace>, <dostep>, <doitem> elements as input
aspinall
parents: 15400
diff changeset
  1238
     | "doitem"         => isarscript data
15286
b084384960d1 Add <undoitem> for theory-state undos.
aspinall
parents: 15268