src/Pure/proof_general.ML
author wenzelm
Thu, 01 Sep 2005 15:58:08 +0200
changeset 17217 954c0f265203
parent 17057 0934ac31985f
child 17221 6cd180204582
permissions -rw-r--r--
added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z; tuned;
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
16534
wenzelm
parents: 16486
diff changeset
    13
The 3.6pre pre-release versions of Emacs Proof General now support the
wenzelm
parents: 16486
diff changeset
    14
new PGIP format for preferences and restore the settings menu.
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
    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.
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    19
*)
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
signature PROOF_GENERAL =
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    22
sig
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    23
  val update_thy_only: string -> unit
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    24
  val try_update_thy_only: string -> unit
13391
553e7b62680f fixed inform_file_retracted: remove_thy;
wenzelm
parents: 13284
diff changeset
    25
  val inform_file_retracted: string -> unit
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    26
  val inform_file_processed: string -> unit
16534
wenzelm
parents: 16486
diff changeset
    27
  val preferences:
wenzelm
parents: 16486
diff changeset
    28
      (string *
wenzelm
parents: 16486
diff changeset
    29
        (string *
wenzelm
parents: 16486
diff changeset
    30
         (string *
wenzelm
parents: 16486
diff changeset
    31
          (string * (string * (unit -> string)) *
wenzelm
parents: 16486
diff changeset
    32
           (string -> unit)))) list) list ref
13728
8004e56204fd Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents: 13646
diff changeset
    33
  val process_pgip: string -> unit
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    34
  val thms_containing: string list -> unit
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    35
  val help: unit -> unit
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    36
  val show_context: unit -> theory
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    37
  val kill_goal: unit -> unit
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    38
  val repeat_undo: int -> unit
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    39
  val isa_restart: unit -> unit
12833
9f3226cfe021 full_proofs;
wenzelm
parents: 12780
diff changeset
    40
  val full_proofs: bool -> unit
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    41
  val isarcmd: string -> unit
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    42
  val init: bool -> unit
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    43
  val init_pgip: bool -> unit
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    44
  val write_keywords: string -> unit
16534
wenzelm
parents: 16486
diff changeset
    45
  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
    46
end;
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    47
16534
wenzelm
parents: 16486
diff changeset
    48
structure ProofGeneral: PROOF_GENERAL =
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    49
struct
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    50
16534
wenzelm
parents: 16486
diff changeset
    51
structure P = OuterParse;
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
    52
15191
5ca1fd9dec83 Support parsing of -- {* comments *}. Add extra output channels.
aspinall
parents: 15173
diff changeset
    53
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    54
(* 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
    55
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    56
val pgip_active = ref false;
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    57
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
    58
16534
wenzelm
parents: 16486
diff changeset
    59
fun pgip () = (! pgip_active);
wenzelm
parents: 16486
diff changeset
    60
fun pgip_emacs_compatibility () = (! pgip_emacs_compatibility_flag);
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    61
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    62
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    63
(* print modes *)
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    64
16534
wenzelm
parents: 16486
diff changeset
    65
val proof_generalN = "ProofGeneral";  (*token markup (colouring vars, etc.)*)
17217
954c0f265203 added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents: 17057
diff changeset
    66
val pgasciiN = "PGASCII";             (*plain 7-bit ASCII communication*)
16534
wenzelm
parents: 16486
diff changeset
    67
val xsymbolsN = Symbol.xsymbolsN;     (*X-Symbol symbols*)
wenzelm
parents: 16486
diff changeset
    68
val pgmlN = "PGML";                   (*XML escapes and PGML symbol elements*)
wenzelm
parents: 16486
diff changeset
    69
val pgmlatomsN = "PGMLatoms";         (*variable kind decorations*)
wenzelm
parents: 16486
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
16534
wenzelm
parents: 16486
diff changeset
    72
fun pgml () = Output.has_mode pgmlN;
wenzelm
parents: 16486
diff changeset
    73
17217
954c0f265203 added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents: 17057
diff changeset
    74
fun special oct =
954c0f265203 added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents: 17057
diff changeset
    75
  if Output.has_mode pgasciiN then chr 1 ^ chr (ord (oct_char oct) - 167)
954c0f265203 added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents: 17057
diff changeset
    76
  else oct_char oct;
954c0f265203 added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents: 17057
diff changeset
    77
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    78
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    79
(* text output: print modes for xsymbol and PGML *)
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    80
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    81
local
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    82
14827
d973e7f820cb Output.add_mode; Output.timing;
wenzelm
parents: 14725
diff changeset
    83
fun xsym_output "\\" = "\\\\"
d973e7f820cb Output.add_mode; Output.timing;
wenzelm
parents: 14725
diff changeset
    84
  | 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
    85
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    86
fun xsymbols_output s =
16534
wenzelm
parents: 16486
diff changeset
    87
  if Output.has_mode xsymbolsN andalso exists_string (equal "\\") s then
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    88
    let val syms = Symbol.explode s
14827
d973e7f820cb Output.add_mode; Output.timing;
wenzelm
parents: 14725
diff changeset
    89
    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
    90
  else Symbol.default_output s;
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    91
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    92
fun pgml_sym s =
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    93
  (case Symbol.decode s of
16534
wenzelm
parents: 16486
diff changeset
    94
    (*NB: an alternative here would be to output the default print mode alternative
wenzelm
parents: 16486
diff changeset
    95
      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
    96
    Symbol.Char s => XML.text s
15403
9e58e666074d Fix pgmlsymbolson/off.
aspinall
parents: 15401
diff changeset
    97
  | Symbol.Sym sn => XML.element "sym" [("name", sn)] [XML.text s]
16534
wenzelm
parents: 16486
diff changeset
    98
  | 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
    99
  | Symbol.Raw s => s);
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   100
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   101
fun pgml_output str =
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   102
  let val syms = Symbol.explode str
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   103
  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
   104
16534
wenzelm
parents: 16486
diff changeset
   105
in
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   106
16534
wenzelm
parents: 16486
diff changeset
   107
fun setup_xsymbols_output () =
wenzelm
parents: 16486
diff changeset
   108
  Output.add_mode xsymbolsN
wenzelm
parents: 16486
diff changeset
   109
    (xsymbols_output, Symbol.default_indent, Symbol.encode_raw);
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   110
16534
wenzelm
parents: 16486
diff changeset
   111
fun setup_pgml_output () =
wenzelm
parents: 16486
diff changeset
   112
  Output.add_mode pgmlN
wenzelm
parents: 16486
diff changeset
   113
    (pgml_output, Symbol.default_indent, Symbol.encode_raw);
12778
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
end;
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
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   118
(* token translations *)
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   119
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   120
local
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   121
17217
954c0f265203 added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents: 17057
diff changeset
   122
fun end_tag () = special "350";
954c0f265203 added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents: 17057
diff changeset
   123
val class_tag = ("class", fn () => special "351");
954c0f265203 added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents: 17057
diff changeset
   124
val tfree_tag = ("tfree", fn () => special "352");
954c0f265203 added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents: 17057
diff changeset
   125
val tvar_tag = ("tvar", fn () => special "353");
954c0f265203 added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents: 17057
diff changeset
   126
val free_tag = ("free", fn () => special "354");
954c0f265203 added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents: 17057
diff changeset
   127
val bound_tag = ("bound", fn () => special "355");
954c0f265203 added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents: 17057
diff changeset
   128
val var_tag = ("var", fn () => special "356");
954c0f265203 added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents: 17057
diff changeset
   129
val skolem_tag = ("skolem", fn () => special "357");
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   130
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   131
fun 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
   132
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   133
fun tagit (kind, bg_tag) x =
16534
wenzelm
parents: 16486
diff changeset
   134
 (if Output.has_mode pgmlatomsN then xml_atom kind x
17217
954c0f265203 added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents: 17057
diff changeset
   135
  else bg_tag () ^ x ^ end_tag (), real (Symbol.length (Symbol.explode x)));
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   136
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   137
fun free_or_skolem x =
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   138
  (case try Syntax.dest_skolem x of
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15472
diff changeset
   139
    NONE => tagit free_tag x
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15472
diff changeset
   140
  | SOME x' => tagit skolem_tag x');
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   141
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   142
fun var_or_skolem s =
15985
f00dd5e06ffe renamed show_var_qmarks to show_question_marks;
wenzelm
parents: 15964
diff changeset
   143
  (case Syntax.read_variable s of
f00dd5e06ffe renamed show_var_qmarks to show_question_marks;
wenzelm
parents: 15964
diff changeset
   144
    SOME (x, i) =>
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   145
      (case try Syntax.dest_skolem x of
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15472
diff changeset
   146
        NONE => tagit var_tag s
15992
cb02d70a2040 var_or_skolem: always print question mark for vars stemming from skolems;
wenzelm
parents: 15985
diff changeset
   147
      | SOME x' => tagit skolem_tag
cb02d70a2040 var_or_skolem: always print question mark for vars stemming from skolems;
wenzelm
parents: 15985
diff changeset
   148
          (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
   149
  | NONE => tagit var_tag s);
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   150
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   151
val proof_general_trans =
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   152
 Syntax.tokentrans_mode proof_generalN
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   153
  [("class", tagit class_tag),
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   154
   ("tfree", tagit tfree_tag),
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   155
   ("tvar", tagit tvar_tag),
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   156
   ("free", free_or_skolem),
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   157
   ("bound", tagit bound_tag),
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   158
   ("var", var_or_skolem)];
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   159
15801
d2f5ca3c048d superceded by Pure.thy and CPure.thy;
wenzelm
parents: 15629
diff changeset
   160
in
d2f5ca3c048d superceded by Pure.thy and CPure.thy;
wenzelm
parents: 15629
diff changeset
   161
d2f5ca3c048d superceded by Pure.thy and CPure.thy;
wenzelm
parents: 15629
diff changeset
   162
val _ = Context.add_setup [Theory.add_tokentrfuns proof_general_trans];
d2f5ca3c048d superceded by Pure.thy and CPure.thy;
wenzelm
parents: 15629
diff changeset
   163
d2f5ca3c048d superceded by Pure.thy and CPure.thy;
wenzelm
parents: 15629
diff changeset
   164
end;
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   165
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   166
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   167
(* assembling PGIP packets *)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   168
17217
954c0f265203 added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents: 17057
diff changeset
   169
val pgip_refid  = ref NONE: string option ref;
16534
wenzelm
parents: 16486
diff changeset
   170
val pgip_refseq = ref NONE: string option ref;
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   171
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   172
local
16821
ba1f6aba44ed Update PGIP packet handling, fixing unique session identifier.
aspinall
parents: 16816
diff changeset
   173
  val pgip_class  = "pg"
ba1f6aba44ed Update PGIP packet handling, fixing unique session identifier.
aspinall
parents: 16816
diff changeset
   174
  val pgip_tag = "Isabelle/Isar"
ba1f6aba44ed Update PGIP packet handling, fixing unique session identifier.
aspinall
parents: 16816
diff changeset
   175
  val pgip_id = ref ""
ba1f6aba44ed Update PGIP packet handling, fixing unique session identifier.
aspinall
parents: 16816
diff changeset
   176
  val pgip_seq = ref 0
ba1f6aba44ed Update PGIP packet handling, fixing unique session identifier.
aspinall
parents: 16816
diff changeset
   177
  fun pgip_serial () = inc pgip_seq
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   178
16534
wenzelm
parents: 16486
diff changeset
   179
  fun assemble_pgips pgips =
wenzelm
parents: 16486
diff changeset
   180
    XML.element
wenzelm
parents: 16486
diff changeset
   181
      "pgip"
16821
ba1f6aba44ed Update PGIP packet handling, fixing unique session identifier.
aspinall
parents: 16816
diff changeset
   182
      ([("tag",    pgip_tag),
ba1f6aba44ed Update PGIP packet handling, fixing unique session identifier.
aspinall
parents: 16816
diff changeset
   183
        ("class",  pgip_class),
17217
954c0f265203 added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents: 17057
diff changeset
   184
        ("seq",    string_of_int (pgip_serial())),
16821
ba1f6aba44ed Update PGIP packet handling, fixing unique session identifier.
aspinall
parents: 16816
diff changeset
   185
        ("id",     !pgip_id)] @
ba1f6aba44ed Update PGIP packet handling, fixing unique session identifier.
aspinall
parents: 16816
diff changeset
   186
       if_none (Option.map (single o (pair "destid")) (! pgip_refid)) [] @
ba1f6aba44ed Update PGIP packet handling, fixing unique session identifier.
aspinall
parents: 16816
diff changeset
   187
       (* destid=refid since Isabelle only communicates back to sender,
ba1f6aba44ed Update PGIP packet handling, fixing unique session identifier.
aspinall
parents: 16816
diff changeset
   188
          so we may omit refid from attributes.
ba1f6aba44ed Update PGIP packet handling, fixing unique session identifier.
aspinall
parents: 16816
diff changeset
   189
       if_none (Option.map (single o (pair "refid"))  (! pgip_refid)) [] @
ba1f6aba44ed Update PGIP packet handling, fixing unique session identifier.
aspinall
parents: 16816
diff changeset
   190
       *)
ba1f6aba44ed Update PGIP packet handling, fixing unique session identifier.
aspinall
parents: 16816
diff changeset
   191
       if_none (Option.map (single o (pair "refseq")) (! pgip_refseq)) [])
16534
wenzelm
parents: 16486
diff changeset
   192
      pgips;
16821
ba1f6aba44ed Update PGIP packet handling, fixing unique session identifier.
aspinall
parents: 16816
diff changeset
   193
13526
9269275e5da6 result dependency output;
wenzelm
parents: 13391
diff changeset
   194
in
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   195
17217
954c0f265203 added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents: 17057
diff changeset
   196
fun init_pgip_session_id () =
16821
ba1f6aba44ed Update PGIP packet handling, fixing unique session identifier.
aspinall
parents: 16816
diff changeset
   197
    pgip_id := getenv "HOSTNAME" ^ "/" ^ getenv "USER" ^ "/" ^
ba1f6aba44ed Update PGIP packet handling, fixing unique session identifier.
aspinall
parents: 16816
diff changeset
   198
               getenv "ISABELLE_PID" ^ "/" ^ Time.toString (Time.now ())
17217
954c0f265203 added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents: 17057
diff changeset
   199
16821
ba1f6aba44ed Update PGIP packet handling, fixing unique session identifier.
aspinall
parents: 16816
diff changeset
   200
ba1f6aba44ed Update PGIP packet handling, fixing unique session identifier.
aspinall
parents: 16816
diff changeset
   201
fun matching_pgip_id id = (id = !pgip_id)
ba1f6aba44ed Update PGIP packet handling, fixing unique session identifier.
aspinall
parents: 16816
diff changeset
   202
16534
wenzelm
parents: 16486
diff changeset
   203
fun decorated_output bg en prfx =
wenzelm
parents: 16486
diff changeset
   204
  writeln_default o enclose bg en o prefix_lines prfx;
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   205
16534
wenzelm
parents: 16486
diff changeset
   206
(* FIXME: see Rev 1.48 [PG CVS] for cleaner version of this which can be used
wenzelm
parents: 16486
diff changeset
   207
   for PG 4.0 which processes PGIP without needing special chars *)
wenzelm
parents: 16486
diff changeset
   208
fun issue_pgips ps =
wenzelm
parents: 16486
diff changeset
   209
  if pgip_emacs_compatibility() then
wenzelm
parents: 16486
diff changeset
   210
    decorated_output (*add urgent message annotation*)
17217
954c0f265203 added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents: 17057
diff changeset
   211
      (special "360") (special "361") ""
16534
wenzelm
parents: 16486
diff changeset
   212
      (assemble_pgips ps)
wenzelm
parents: 16486
diff changeset
   213
  else
wenzelm
parents: 16486
diff changeset
   214
    writeln_default (assemble_pgips ps);
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   215
16534
wenzelm
parents: 16486
diff changeset
   216
fun assemble_pgip resp attrs s = assemble_pgips [XML.element resp attrs [s]];
wenzelm
parents: 16486
diff changeset
   217
fun assemble_pgipe resp attrs = assemble_pgips [XML.element resp attrs []];
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   218
16534
wenzelm
parents: 16486
diff changeset
   219
(* FIXME: need to add stuff to gather PGIPs here *)
wenzelm
parents: 16486
diff changeset
   220
fun issue_pgip resp attrs txt =
wenzelm
parents: 16486
diff changeset
   221
  if pgip_emacs_compatibility () then
wenzelm
parents: 16486
diff changeset
   222
    decorated_output (*add urgent message annotation*)
17217
954c0f265203 added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents: 17057
diff changeset
   223
      (special "360") (special "361") ""
16534
wenzelm
parents: 16486
diff changeset
   224
      (assemble_pgip resp attrs txt)
wenzelm
parents: 16486
diff changeset
   225
  else
wenzelm
parents: 16486
diff changeset
   226
    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
   227
16534
wenzelm
parents: 16486
diff changeset
   228
(* FIXME: temporarily to support PG 3.4 *)
wenzelm
parents: 16486
diff changeset
   229
fun issue_pgip_maybe_decorated bg en resp attrs s =
wenzelm
parents: 16486
diff changeset
   230
  if pgip_emacs_compatibility () then
wenzelm
parents: 16486
diff changeset
   231
    (*in PGIP mode, but using escape characters as well*)
wenzelm
parents: 16486
diff changeset
   232
    writeln_default (enclose bg en (assemble_pgip resp attrs s))
wenzelm
parents: 16486
diff changeset
   233
  else
wenzelm
parents: 16486
diff changeset
   234
    issue_pgip resp attrs s;
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   235
16534
wenzelm
parents: 16486
diff changeset
   236
fun issue_pgipe resp attrs = writeln_default (assemble_pgipe resp attrs);
wenzelm
parents: 16486
diff changeset
   237
wenzelm
parents: 16486
diff changeset
   238
end;
wenzelm
parents: 16486
diff changeset
   239
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   240
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   241
(* messages and notification *)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   242
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
   243
local
16534
wenzelm
parents: 16486
diff changeset
   244
  val delay_msgs = ref false;   (*true: accumulate messages*)
wenzelm
parents: 16486
diff changeset
   245
  val delayed_msgs = ref [];
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
   246
in
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   247
16534
wenzelm
parents: 16486
diff changeset
   248
fun message resp attrs bg en prfx s =
wenzelm
parents: 16486
diff changeset
   249
  if pgip () then
wenzelm
parents: 16486
diff changeset
   250
   (if (! delay_msgs) then
wenzelm
parents: 16486
diff changeset
   251
      delayed_msgs := (resp, attrs, prefix_lines prfx s) :: ! delayed_msgs (*NB: no decs*)
wenzelm
parents: 16486
diff changeset
   252
    else
wenzelm
parents: 16486
diff changeset
   253
      issue_pgip_maybe_decorated bg en resp attrs
wenzelm
parents: 16486
diff changeset
   254
        (XML.element "pgmltext" [] [prefix_lines prfx s]))
wenzelm
parents: 16486
diff changeset
   255
  else decorated_output bg en 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
   256
16534
wenzelm
parents: 16486
diff changeset
   257
fun start_delay_msgs () = (set delay_msgs; 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
   258
16534
wenzelm
parents: 16486
diff changeset
   259
fun end_delayed_msgs () = (reset delay_msgs;
wenzelm
parents: 16486
diff changeset
   260
  (! delayed_msgs) |> map (fn (resp, attrs, s) =>
wenzelm
parents: 16486
diff changeset
   261
    XML.element resp attrs [XML.element "pgmltext" [] [s]]));
wenzelm
parents: 16486
diff changeset
   262
wenzelm
parents: 16486
diff changeset
   263
end;
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   264
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   265
local
16534
wenzelm
parents: 16486
diff changeset
   266
  val display_area = ("area", "display");
wenzelm
parents: 16486
diff changeset
   267
  val message_area = ("area", "message");
wenzelm
parents: 16486
diff changeset
   268
  val internal_category = ("messagecategory", "internal");
wenzelm
parents: 16486
diff changeset
   269
  val info_category = ("messagecategory", "information");
wenzelm
parents: 16486
diff changeset
   270
  val tracing_category = ("messagecategory", "tracing");
wenzelm
parents: 16486
diff changeset
   271
  val urgent_indication = ("urgent", "y");
wenzelm
parents: 16486
diff changeset
   272
  val nonfatal = ("fatality", "nonfatal");
wenzelm
parents: 16486
diff changeset
   273
  val fatal = ("fatality", "fatal");
wenzelm
parents: 16486
diff changeset
   274
  val panic = ("fatality", "panic");
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   275
16534
wenzelm
parents: 16486
diff changeset
   276
  val thyname_attr = pair "thyname";
wenzelm
parents: 16486
diff changeset
   277
  val url_attr = pair "url";
wenzelm
parents: 16486
diff changeset
   278
  fun localfile_url_attr path = url_attr ("file:///" ^ path);
wenzelm
parents: 16486
diff changeset
   279
in
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   280
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   281
fun setup_messages () =
17217
954c0f265203 added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents: 17057
diff changeset
   282
 (writeln_fn := (fn s => message "normalresponse" [message_area] "" "" "" s);
954c0f265203 added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents: 17057
diff changeset
   283
  priority_fn := (fn s => message "normalresponse" [message_area, urgent_indication]
954c0f265203 added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents: 17057
diff changeset
   284
    (special "360") (special "361") "" s);
954c0f265203 added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents: 17057
diff changeset
   285
  tracing_fn := (fn s => message "normalresponse"  [message_area, tracing_category]
954c0f265203 added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents: 17057
diff changeset
   286
    (special "360" ^ special "375") (special "361") "" s);
954c0f265203 added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents: 17057
diff changeset
   287
  info_fn := (fn s => message "normalresponse" [message_area, info_category]
954c0f265203 added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents: 17057
diff changeset
   288
    (special "362") (special "363") "+++ " s);
954c0f265203 added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents: 17057
diff changeset
   289
  debug_fn := (fn s => message "normalresponse" [message_area, internal_category]
954c0f265203 added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents: 17057
diff changeset
   290
    (special "362") (special "363") "+++ " s);
954c0f265203 added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents: 17057
diff changeset
   291
  warning_fn := (fn s => message "errorresponse" [nonfatal]
954c0f265203 added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents: 17057
diff changeset
   292
    (special "362") (special "363") "### " s);
954c0f265203 added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents: 17057
diff changeset
   293
  error_fn := (fn s => message "errorresponse" [fatal]
954c0f265203 added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents: 17057
diff changeset
   294
    (special "364") (special "365") "*** " s);
954c0f265203 added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents: 17057
diff changeset
   295
  panic_fn := (fn s => message "errorresponse" [panic]
954c0f265203 added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents: 17057
diff changeset
   296
    (special "364") (special "365") "!!! " s));
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
15400
50bbdabd7326 Insert pgmltext element into responses in PGIP mode
aspinall
parents: 15289
diff changeset
   299
(* 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
   300
16534
wenzelm
parents: 16486
diff changeset
   301
fun with_displaywrap (elt, attrs) dispfn =
wenzelm
parents: 16486
diff changeset
   302
  let
wenzelm
parents: 16486
diff changeset
   303
    val lines = ref ([]: string list);
wenzelm
parents: 16486
diff changeset
   304
    fun wlgrablines s = lines := s :: ! lines;
wenzelm
parents: 16486
diff changeset
   305
  in
wenzelm
parents: 16486
diff changeset
   306
    setmp writeln_fn wlgrablines dispfn ();
16798
36d34186741b Add acceptedpgipelems message
aspinall
parents: 16791
diff changeset
   307
    (* IMPORTANT FIXME: XML.element here too inefficient, should use stream output *)
16534
wenzelm
parents: 16486
diff changeset
   308
    issue_pgip elt attrs (XML.element "pgmltext" [] (! lines))
wenzelm
parents: 16486
diff changeset
   309
  end;
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   310
17217
954c0f265203 added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents: 17057
diff changeset
   311
fun emacs_notify s = decorated_output (special "360") (special "361") "" s;
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   312
16534
wenzelm
parents: 16486
diff changeset
   313
fun tell_clear_goals () =
wenzelm
parents: 16486
diff changeset
   314
  if pgip () then
wenzelm
parents: 16486
diff changeset
   315
    issue_pgipe "cleardisplay" [display_area]
wenzelm
parents: 16486
diff changeset
   316
  else
wenzelm
parents: 16486
diff changeset
   317
    emacs_notify "Proof General, please clear the goals buffer.";
wenzelm
parents: 16486
diff changeset
   318
wenzelm
parents: 16486
diff changeset
   319
fun tell_clear_response () =
wenzelm
parents: 16486
diff changeset
   320
  if pgip () then
wenzelm
parents: 16486
diff changeset
   321
    issue_pgipe "cleardisplay" [message_area]
wenzelm
parents: 16486
diff changeset
   322
  else
wenzelm
parents: 16486
diff changeset
   323
    emacs_notify "Proof General, please clear the response buffer.";
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   324
16534
wenzelm
parents: 16486
diff changeset
   325
fun tell_file_loaded path =
wenzelm
parents: 16486
diff changeset
   326
  if pgip () then
16788
0c6f5fe30676 Fix informtheoryloaded/retracted -> informfileloaded/retracted to match pgip.rnc
aspinall
parents: 16534
diff changeset
   327
    issue_pgipe "informfileloaded"
0c6f5fe30676 Fix informtheoryloaded/retracted -> informfileloaded/retracted to match pgip.rnc
aspinall
parents: 16534
diff changeset
   328
      [localfile_url_attr  (XML.text (File.platform_path path))]
16534
wenzelm
parents: 16486
diff changeset
   329
  else
wenzelm
parents: 16486
diff changeset
   330
    emacs_notify ("Proof General, this file is loaded: " ^ quote (File.platform_path path));
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   331
16534
wenzelm
parents: 16486
diff changeset
   332
fun tell_file_retracted path =
wenzelm
parents: 16486
diff changeset
   333
  if pgip() then
16788
0c6f5fe30676 Fix informtheoryloaded/retracted -> informfileloaded/retracted to match pgip.rnc
aspinall
parents: 16534
diff changeset
   334
    issue_pgipe "informfileretracted"
0c6f5fe30676 Fix informtheoryloaded/retracted -> informfileloaded/retracted to match pgip.rnc
aspinall
parents: 16534
diff changeset
   335
      [localfile_url_attr  (XML.text (File.platform_path path))]
16534
wenzelm
parents: 16486
diff changeset
   336
  else
wenzelm
parents: 16486
diff changeset
   337
    emacs_notify ("Proof General, you can unlock the file " ^ quote (File.platform_path path));
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   338
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
(* theory / proof state output *)
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   341
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   342
local
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   343
16534
wenzelm
parents: 16486
diff changeset
   344
fun tmp_markers f =
17217
954c0f265203 added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents: 17057
diff changeset
   345
  setmp Display.current_goals_markers (special "366", special "367", "") f ();
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   346
16534
wenzelm
parents: 16486
diff changeset
   347
fun statedisplay prts =
wenzelm
parents: 16486
diff changeset
   348
  issue_pgip "proofstate" []
wenzelm
parents: 16486
diff changeset
   349
    (XML.element "pgml" []
wenzelm
parents: 16486
diff changeset
   350
      [XML.element "statedisplay" [] [Pretty.output (Pretty.chunks prts)]]);
17217
954c0f265203 added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents: 17057
diff changeset
   351
16534
wenzelm
parents: 16486
diff changeset
   352
fun print_current_goals n m st =
wenzelm
parents: 16486
diff changeset
   353
  if pgml () then statedisplay (Display.pretty_current_goals n m st)
wenzelm
parents: 16486
diff changeset
   354
  else tmp_markers (fn () => Display.print_current_goals_default n m st);
13545
fcdbd6cf5f9f improved tell_thm_deps;
wenzelm
parents: 13538
diff changeset
   355
16534
wenzelm
parents: 16486
diff changeset
   356
fun print_state b st =
wenzelm
parents: 16486
diff changeset
   357
  if pgml () then statedisplay (Toplevel.pretty_state b st)
wenzelm
parents: 16486
diff changeset
   358
  else tmp_markers (fn () => Toplevel.print_state_default b st);
wenzelm
parents: 16486
diff changeset
   359
13526
9269275e5da6 result dependency output;
wenzelm
parents: 13391
diff changeset
   360
in
9269275e5da6 result dependency output;
wenzelm
parents: 13391
diff changeset
   361
16534
wenzelm
parents: 16486
diff changeset
   362
fun setup_state () =
wenzelm
parents: 16486
diff changeset
   363
  (Display.print_current_goals_fn := print_current_goals;
wenzelm
parents: 16486
diff changeset
   364
   Toplevel.print_state_fn := print_state;
wenzelm
parents: 16486
diff changeset
   365
   (* FIXME: check next octal char won't appear in pgip? *)
17217
954c0f265203 added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents: 17057
diff changeset
   366
   Toplevel.prompt_state_fn := (fn s => suffix (special "372")
954c0f265203 added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents: 17057
diff changeset
   367
     (Toplevel.prompt_state_default s)));
13728
8004e56204fd Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents: 13646
diff changeset
   368
16534
wenzelm
parents: 16486
diff changeset
   369
end;
wenzelm
parents: 16486
diff changeset
   370
wenzelm
parents: 16486
diff changeset
   371
end;
13728
8004e56204fd Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents: 13646
diff changeset
   372
16022
96a9bf7ac18d FindTheorems.print_theorems;
wenzelm
parents: 15992
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
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   376
fun thms_containing ss =
16534
wenzelm
parents: 16486
diff changeset
   377
  FindTheorems.print_theorems (ProofContext.init (the_context ())) NONE NONE
16022
96a9bf7ac18d FindTheorems.print_theorems;
wenzelm
parents: 15992
diff changeset
   378
    (map (fn s => (true, FindTheorems.Pattern s)) ss);
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   379
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   380
val welcome = priority o Session.welcome;
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   381
val help = welcome;
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   382
val show_context = Context.the_context;
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   383
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   384
fun kill_goal () = (Goals.reset_goals (); tell_clear_goals ());
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 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
   387
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   388
fun repeat_undo 0 = ()
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   389
  | repeat_undo 1 = undo ()
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   390
  | 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
   391
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   392
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   393
(* theory loader actions *)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   394
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   395
local
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
fun add_master_files name files =
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   398
  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
   399
  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
   400
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   401
fun trace_action action name =
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   402
  if action = ThyInfo.Update then
15570
8d8c70b41bab Move towards standard functions.
skalberg
parents: 15531
diff changeset
   403
    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
   404
  else if action = ThyInfo.Outdate orelse action = ThyInfo.Remove then
15570
8d8c70b41bab Move towards standard functions.
skalberg
parents: 15531
diff changeset
   405
    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
   406
  else ();
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   407
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   408
in
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   409
  fun setup_thy_loader () = ThyInfo.add_hook trace_action;
15570
8d8c70b41bab Move towards standard functions.
skalberg
parents: 15531
diff changeset
   410
  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
   411
end;
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   412
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   413
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   414
(* prepare theory context *)
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
val thy_name = Path.pack o #1 o Path.split_ext o Path.base o Path.unpack;
16534
wenzelm
parents: 16486
diff changeset
   417
wenzelm
parents: 16486
diff changeset
   418
(* FIXME general treatment of tracing*)
wenzelm
parents: 16486
diff changeset
   419
val update_thy_only = setmp MetaSimplifier.trace_simp false ThyInfo.update_thy_only;
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   420
16440
9b6e6d5fba05 Context.theory_name;
wenzelm
parents: 16259
diff changeset
   421
fun dynamic_context () =
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   422
  (case Context.get_context () of
16440
9b6e6d5fba05 Context.theory_name;
wenzelm
parents: 16259
diff changeset
   423
    SOME thy => "  Using current (dynamic!) one: " ^ quote (Context.theory_name thy)
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15472
diff changeset
   424
  | NONE => "");
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   425
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   426
fun try_update_thy_only file =
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   427
  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
   428
    let val name = thy_name file in
16534
wenzelm
parents: 16486
diff changeset
   429
      if is_some (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
   430
      then update_thy_only name
16440
9b6e6d5fba05 Context.theory_name;
wenzelm
parents: 16259
diff changeset
   431
      else warning ("Unkown theory context of ML file." ^ dynamic_context ())
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   432
    end) ();
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   433
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   434
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   435
(* get informed about files *)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   436
16534
wenzelm
parents: 16486
diff changeset
   437
val inform_file_retracted = ThyInfo.if_known_thy ThyInfo.remove_thy o thy_name;
wenzelm
parents: 16486
diff changeset
   438
val inform_file_processed = ThyInfo.if_known_thy ThyInfo.touch_child_thys o thy_name;
wenzelm
parents: 16486
diff changeset
   439
val openfile_retract = Output.no_warnings (ThyInfo.if_known_thy ThyInfo.remove_thy) o thy_name;
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
   440
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   441
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
   442
  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
   443
    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
   444
     (ThyInfo.touch_child_thys name;
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   445
      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
   446
       (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
   447
        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
   448
    else raise Toplevel.UNDEF
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   449
  end;
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   450
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   451
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
   452
 (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
   453
  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
   454
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   455
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   456
(* restart top-level loop (keeps most state information) *)
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   457
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   458
local
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   459
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   460
fun restart isar =
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   461
 (if isar then tell_clear_goals () else kill_goal ();
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   462
  tell_clear_response ();
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   463
  welcome ());
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   464
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   465
in
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   466
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   467
fun isa_restart () = restart false;
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   468
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
   469
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   470
end;
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   471
12833
9f3226cfe021 full_proofs;
wenzelm
parents: 12780
diff changeset
   472
fun full_proofs true = proofs := 2
9f3226cfe021 full_proofs;
wenzelm
parents: 12780
diff changeset
   473
  | full_proofs false = proofs := 1;
9f3226cfe021 full_proofs;
wenzelm
parents: 12780
diff changeset
   474
9f3226cfe021 full_proofs;
wenzelm
parents: 12780
diff changeset
   475
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   476
(* theorem dependency output *)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   477
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   478
local
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   479
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   480
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
   481
16789
e8f7a6ec92e5 Note about theorem dependencies including themselves.
aspinall
parents: 16788
diff changeset
   482
(* FIXME: investigate why dependencies at the moment include themselves! *)
16534
wenzelm
parents: 16486
diff changeset
   483
fun thm_deps_message (thms, deps) =
wenzelm
parents: 16486
diff changeset
   484
  if pgip() then
wenzelm
parents: 16486
diff changeset
   485
    issue_pgips
wenzelm
parents: 16486
diff changeset
   486
      [XML.element
wenzelm
parents: 16486
diff changeset
   487
        "metainforesponse"  (* FIXME: get thy name from info here? *)
wenzelm
parents: 16486
diff changeset
   488
        [("infotype", "isabelle_theorem_dependencies")]
wenzelm
parents: 16486
diff changeset
   489
        [XML.element "value" [("name", "thms")] [XML.text thms],
wenzelm
parents: 16486
diff changeset
   490
         XML.element "value" [("name", "deps")] [XML.text deps]]]
wenzelm
parents: 16486
diff changeset
   491
  else emacs_notify ("Proof General, theorem dependencies of " ^ thms ^ " are " ^ deps);
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   492
16534
wenzelm
parents: 16486
diff changeset
   493
fun tell_thm_deps ths = conditional (Output.has_mode thm_depsN) (fn () =>
wenzelm
parents: 16486
diff changeset
   494
  let
wenzelm
parents: 16486
diff changeset
   495
    val names = filter_out (equal "") (map Thm.name_of_thm ths);
wenzelm
parents: 16486
diff changeset
   496
    val deps = filter_out (equal "")
17018
1e9e0f5877f2 Adapted to new interface of thms_of_proof.
berghofe
parents: 16958
diff changeset
   497
      (Symtab.keys (fold Proofterm.thms_of_proof
1e9e0f5877f2 Adapted to new interface of thms_of_proof.
berghofe
parents: 16958
diff changeset
   498
        (map Thm.proof_of ths) Symtab.empty));
16534
wenzelm
parents: 16486
diff changeset
   499
  in
wenzelm
parents: 16486
diff changeset
   500
    if null names orelse null deps then ()
wenzelm
parents: 16486
diff changeset
   501
    else thm_deps_message (spaces_quote names, spaces_quote deps)
wenzelm
parents: 16486
diff changeset
   502
  end);
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   503
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   504
in
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   505
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   506
fun setup_present_hook () =
15570
8d8c70b41bab Move towards standard functions.
skalberg
parents: 15531
diff changeset
   507
  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
   508
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   509
end;
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   510
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   511
16534
wenzelm
parents: 16486
diff changeset
   512
wenzelm
parents: 16486
diff changeset
   513
(** preferences **)
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   514
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   515
local
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   516
16534
wenzelm
parents: 16486
diff changeset
   517
val pgipnat = XML.element "pgipint" [("min", "0")] [];
wenzelm
parents: 16486
diff changeset
   518
fun pgipnatmax max = XML.element "pgipint" [("min", "0"), ("max", string_of_int max)] [];
wenzelm
parents: 16486
diff changeset
   519
val pgipbool = XML.element "pgipbool" [] [];
wenzelm
parents: 16486
diff changeset
   520
wenzelm
parents: 16486
diff changeset
   521
fun with_default f = (f (), f);
wenzelm
parents: 16486
diff changeset
   522
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   523
in
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   524
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   525
fun nat_option r = (pgipnat,
16534
wenzelm
parents: 16486
diff changeset
   526
  with_default (fn () => string_of_int (! r)),
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   527
  (fn s => (case Syntax.read_nat s of
16534
wenzelm
parents: 16486
diff changeset
   528
      NONE => error ("nat_option: illegal value: " ^ s)
wenzelm
parents: 16486
diff changeset
   529
    | SOME i => r := i)));
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   530
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   531
fun bool_option r = (pgipbool,
16534
wenzelm
parents: 16486
diff changeset
   532
  with_default (fn () => Bool.toString (! r)),
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   533
  (fn "false" => r := false | "true" => r := true
16534
wenzelm
parents: 16486
diff changeset
   534
    | 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
   535
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   536
val proof_option = (pgipbool,
16534
wenzelm
parents: 16486
diff changeset
   537
  with_default (fn () => Bool.toString (! proofs >= 2)),
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   538
  (fn "false" => proofs := 1 | "true" => proofs := 2
16534
wenzelm
parents: 16486
diff changeset
   539
    | 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
   540
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   541
val thm_deps_option = (pgipbool,
16534
wenzelm
parents: 16486
diff changeset
   542
  with_default (fn () => Bool.toString (Output.has_mode thm_depsN)),
17217
954c0f265203 added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents: 17057
diff changeset
   543
  (fn "false" => change print_mode (remove (op =) thm_depsN)
954c0f265203 added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents: 17057
diff changeset
   544
    | "true" => change print_mode (insert (op =) thm_depsN)
16534
wenzelm
parents: 16486
diff changeset
   545
    | 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
   546
16534
wenzelm
parents: 16486
diff changeset
   547
local
wenzelm
parents: 16486
diff changeset
   548
  val pg_print_depth_val = ref 10;
wenzelm
parents: 16486
diff changeset
   549
  fun pg_print_depth n = (print_depth n; pg_print_depth_val := n)
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   550
in
16534
wenzelm
parents: 16486
diff changeset
   551
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   552
val print_depth_option = (pgipnat,
16534
wenzelm
parents: 16486
diff changeset
   553
  with_default (fn () => string_of_int (! pg_print_depth_val)),
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   554
  (fn s => (case Syntax.read_nat s of
16534
wenzelm
parents: 16486
diff changeset
   555
      NONE => error ("print_depth_option: illegal value: " ^ s)
wenzelm
parents: 16486
diff changeset
   556
    | SOME i => pg_print_depth i)));
wenzelm
parents: 16486
diff changeset
   557
end;
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   558
16534
wenzelm
parents: 16486
diff changeset
   559
val preferences = ref
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   560
  [("Display",
16534
wenzelm
parents: 16486
diff changeset
   561
    [("show-types",
wenzelm
parents: 16486
diff changeset
   562
      ("Include types in display of Isabelle terms",
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   563
       bool_option show_types)),
16534
wenzelm
parents: 16486
diff changeset
   564
     ("show-sorts",
wenzelm
parents: 16486
diff changeset
   565
      ("Include sorts in display of Isabelle terms",
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   566
       bool_option show_sorts)),
16534
wenzelm
parents: 16486
diff changeset
   567
     ("show-consts",
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   568
      ("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
   569
       bool_option show_consts)),
16534
wenzelm
parents: 16486
diff changeset
   570
     ("long-names",
wenzelm
parents: 16486
diff changeset
   571
      ("Show fully qualified names in Isabelle terms",
wenzelm
parents: 16486
diff changeset
   572
       bool_option long_names)),
wenzelm
parents: 16486
diff changeset
   573
     ("show-brackets",
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   574
      ("Show full bracketing in Isabelle terms",
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   575
       bool_option show_brackets)),
16534
wenzelm
parents: 16486
diff changeset
   576
     ("show-main-goal",
wenzelm
parents: 16486
diff changeset
   577
      ("Show main goal in proof state display",
wenzelm
parents: 16486
diff changeset
   578
       bool_option Proof.show_main_goal)),
wenzelm
parents: 16486
diff changeset
   579
     ("eta-contract",
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   580
      ("Print terms eta-contracted",
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   581
       bool_option Syntax.eta_contract))]),
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   582
   ("Advanced Display",
16534
wenzelm
parents: 16486
diff changeset
   583
    [("goals-limit",
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   584
      ("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
   585
       nat_option goals_limit)),
16534
wenzelm
parents: 16486
diff changeset
   586
     ("prems-limit",
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   587
      ("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
   588
       nat_option ProofContext.prems_limit)),
16534
wenzelm
parents: 16486
diff changeset
   589
     ("print-depth",
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   590
      ("Setting for the ML print depth",
15472
4674102737e9 Added show_var_qmarks flag.
berghofe
parents: 15457
diff changeset
   591
       print_depth_option)),
15985
f00dd5e06ffe renamed show_var_qmarks to show_question_marks;
wenzelm
parents: 15964
diff changeset
   592
     ("show-question-marks",
15472
4674102737e9 Added show_var_qmarks flag.
berghofe
parents: 15457
diff changeset
   593
      ("Show leading question mark of variable name",
15985
f00dd5e06ffe renamed show_var_qmarks to show_question_marks;
wenzelm
parents: 15964
diff changeset
   594
       bool_option show_question_marks))]),
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   595
   ("Tracing",
16534
wenzelm
parents: 16486
diff changeset
   596
    [("trace-simplifier",
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   597
      ("Trace simplification rules.",
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   598
       bool_option trace_simp)),
16534
wenzelm
parents: 16486
diff changeset
   599
     ("trace-rules",
wenzelm
parents: 16486
diff changeset
   600
      ("Trace application of the standard rules",
wenzelm
parents: 16486
diff changeset
   601
       bool_option trace_rules)),
wenzelm
parents: 16486
diff changeset
   602
     ("trace-unification",
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   603
      ("Output error diagnostics during unification",
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   604
       bool_option Pattern.trace_unify_fail)),
16534
wenzelm
parents: 16486
diff changeset
   605
     ("global-timing",
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   606
      ("Whether to enable timing in Isabelle.",
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   607
       bool_option Output.timing))]),
16534
wenzelm
parents: 16486
diff changeset
   608
   ("Proof",
wenzelm
parents: 16486
diff changeset
   609
    [("quick-and-dirty",
wenzelm
parents: 16486
diff changeset
   610
      ("Take a few short cuts",
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   611
       bool_option quick_and_dirty)),
16534
wenzelm
parents: 16486
diff changeset
   612
     ("full-proofs",
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   613
      ("Record full proof objects internally",
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   614
       proof_option)),
16534
wenzelm
parents: 16486
diff changeset
   615
     ("theorem-dependencies",
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   616
       ("Track theorem dependencies within Proof General",
16534
wenzelm
parents: 16486
diff changeset
   617
        thm_deps_option)),
wenzelm
parents: 16486
diff changeset
   618
     ("skip-proofs",
16816
ccf39b7ca3b7 tuned msg;
wenzelm
parents: 16798
diff changeset
   619
      ("Ignore proof scripts (interactive-only)",
15238
cb559bd0b03c Added entry in Settings menu for Toplevel.skip_proofs flag.
berghofe
parents: 15225
diff changeset
   620
       bool_option Toplevel.skip_proofs))])
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   621
   ];
16534
wenzelm
parents: 16486
diff changeset
   622
end;
wenzelm
parents: 16486
diff changeset
   623
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   624
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   625
(* Configuration: GUI config, proverinfo messages *)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   626
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   627
local
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   628
    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
   629
    val name_attr = pair "name"
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   630
    val version_attr = pair "version"
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   631
    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
   632
in
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   633
fun send_pgip_config () =
16534
wenzelm
parents: 16486
diff changeset
   634
    let
wenzelm
parents: 16486
diff changeset
   635
        val path = Path.unpack config_file
wenzelm
parents: 16486
diff changeset
   636
        val exists = File.exists path
wenzelm
parents: 16486
diff changeset
   637
        val proverinfo =
wenzelm
parents: 16486
diff changeset
   638
            XML.element "proverinfo"
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   639
              [("name",Session.name()), ("version", version),
16534
wenzelm
parents: 16486
diff changeset
   640
               ("url", isabelle_www), ("filenameextns", ".thy;")]
wenzelm
parents: 16486
diff changeset
   641
            [XML.element "welcomemsg" [] [XML.text (Session.welcome())],
wenzelm
parents: 16486
diff changeset
   642
             XML.element "helpdoc"
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   643
         (* 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
   644
          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
   645
          front end should be responsible for launching viewer, etc. *)
16534
wenzelm
parents: 16486
diff changeset
   646
                      [("name", "Isabelle/HOL Tutorial"),
wenzelm
parents: 16486
diff changeset
   647
                       ("descr", "A Gentle Introduction to Isabelle/HOL"),
wenzelm
parents: 16486
diff changeset
   648
                       ("url",  "http://isabelle.in.tum.de/dist/Isabelle2004/doc/tutorial.pdf")]
wenzelm
parents: 16486
diff changeset
   649
              []]
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   650
    in
16534
wenzelm
parents: 16486
diff changeset
   651
        if exists then
wenzelm
parents: 16486
diff changeset
   652
            (issue_pgips [proverinfo]; issue_pgips [File.read path])
wenzelm
parents: 16486
diff changeset
   653
        else panic ("PGIP configuration file " ^ config_file ^ " not found")
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   654
    end;
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   655
end
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   656
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   657
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
   658
(* 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
   659
fun send_informguise (openfile, opentheory, openproofpos) =
16534
wenzelm
parents: 16486
diff changeset
   660
    let val guisefile =
wenzelm
parents: 16486
diff changeset
   661
            case openfile of SOME f => [XML.element "guisefile"
wenzelm
parents: 16486
diff changeset
   662
                                                    [("url",Url.pack (Url.File (Path.unpack f)))] []]
wenzelm
parents: 16486
diff changeset
   663
                           | _ => []
wenzelm
parents: 16486
diff changeset
   664
        val guisetheory =
wenzelm
parents: 16486
diff changeset
   665
            case opentheory of SOME t => [XML.element "guisetheory" [("thyname", t)] []]
wenzelm
parents: 16486
diff changeset
   666
                             | _ => []
wenzelm
parents: 16486
diff changeset
   667
        val guiseproof =
wenzelm
parents: 16486
diff changeset
   668
            case openproofpos of SOME i => [XML.element "guiseproof" [("proofpos", string_of_int i)] []]
wenzelm
parents: 16486
diff changeset
   669
                               | _ => []
wenzelm
parents: 16486
diff changeset
   670
    in
wenzelm
parents: 16486
diff changeset
   671
        issue_pgips [XML.element "informguise" [] (guisefile @ guisetheory @ guiseproof)]
wenzelm
parents: 16486
diff changeset
   672
    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
   673
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
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   675
(* PGIP identifier tables (prover objects). [incomplete] *)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   676
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   677
local
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   678
    val objtype_thy  = "theory"
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   679
    val objtype_thm  = "theorem"
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   680
    val objtype_term = "term"
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   681
    val objtype_type = "type"
16534
wenzelm
parents: 16486
diff changeset
   682
wenzelm
parents: 16486
diff changeset
   683
    fun xml_idtable ty ctx ids =
wenzelm
parents: 16486
diff changeset
   684
        let
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15472
diff changeset
   685
            fun ctx_attr (SOME c)= [("context", c)]
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15472
diff changeset
   686
              | ctx_attr NONE    = []
16534
wenzelm
parents: 16486
diff changeset
   687
            fun xmlid x = XML.element "identifier" [] [XML.text x];
wenzelm
parents: 16486
diff changeset
   688
        in
wenzelm
parents: 16486
diff changeset
   689
            XML.element "idtable" (("objtype", ty)::ctx_attr ctx)
wenzelm
parents: 16486
diff changeset
   690
                                  (map xmlid ids)
wenzelm
parents: 16486
diff changeset
   691
        end
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   692
in
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   693
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   694
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
   695
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
   696
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
   697
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15472
diff changeset
   698
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
   699
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   700
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
   701
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
   702
16534
wenzelm
parents: 16486
diff changeset
   703
fun send_thm_idtable ctx thy =
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   704
    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
   705
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   706
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
   707
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   708
(* 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
   709
   & maybe not so useful anyway *)
16534
wenzelm
parents: 16486
diff changeset
   710
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   711
end
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   712
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   713
(* 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
   714
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   715
local
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   716
 val topthy = Toplevel.theory_of o Toplevel.get_state
16486
1a12cdb6ee6b get_thm(s): Name;
wenzelm
parents: 16440
diff changeset
   717
 fun pthm thy name = print_thm (get_thm thy (Name name))
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   718
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   719
 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
   720
in
16798
36d34186741b Add acceptedpgipelems message
aspinall
parents: 16791
diff changeset
   721
(* FIXME: add askids for "file" here, which returns single theory with same name *)
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15472
diff changeset
   722
fun askids (NONE, SOME "theory")  = send_thy_idtable NONE (ThyInfo.names())
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15472
diff changeset
   723
  | 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
   724
                           (* only theories known in top context *)
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15472
diff changeset
   725
  | askids (SOME thy, SOME "theory") = send_thy_idtable (SOME thy) (ThyInfo.get_preds thy)
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15472
diff changeset
   726
  | askids (SOME thy, SOME "theorem") = send_thm_idtable (SOME thy) (ThyInfo.get_theory thy)
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15472
diff changeset
   727
  | askids (SOME thy, NONE) = (send_thy_idtable (SOME thy) (ThyInfo.get_preds thy);
16534
wenzelm
parents: 16486
diff changeset
   728
                               send_thm_idtable (SOME thy) (ThyInfo.get_theory thy))
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15472
diff changeset
   729
  | 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
   730
16534
wenzelm
parents: 16486
diff changeset
   731
fun showid (_,        "theory", n) =
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   732
    with_displaywrap (idvalue "theory" n) (fn ()=>(print_theory (ThyInfo.get_theory n)))
16534
wenzelm
parents: 16486
diff changeset
   733
  | showid (SOME thy, "theorem", t) =
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   734
    with_displaywrap (idvalue "theorem" t) (fn ()=>(pthm (ThyInfo.get_theory thy) t))
16534
wenzelm
parents: 16486
diff changeset
   735
  | showid (NONE,     "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 (topthy()) t)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   737
  | 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
   738
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   739
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
   740
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
   741
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   742
(** Parsing proof scripts without execution **)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   743
15146
eab7de0d0a31 Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents: 15145
diff changeset
   744
(* Notes.
eab7de0d0a31 Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents: 15145
diff changeset
   745
   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
   746
   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
   747
   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
   748
   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
   749
   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
   750
   Markus June '04) helps do this, but the mechanism is still a bad mess.
16534
wenzelm
parents: 16486
diff changeset
   751
15254
10cfd6a14682 Simplification to symbol processing; put quotes around theory name in message.
aspinall
parents: 15253
diff changeset
   752
   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
   753
   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
   754
eab7de0d0a31 Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents: 15145
diff changeset
   755
   Probably the best solution is to produce the meta-information at
16534
wenzelm
parents: 16486
diff changeset
   756
   the same time as the parse, for each command, e.g. by recording a
wenzelm
parents: 16486
diff changeset
   757
   list of (name,objtype) pairs which record the bindings created by
wenzelm
parents: 16486
diff changeset
   758
   a command.  This would require changing the interfaces in
wenzelm
parents: 16486
diff changeset
   759
   outer_syntax.ML (or providing new ones),
15146
eab7de0d0a31 Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents: 15145
diff changeset
   760
eab7de0d0a31 Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents: 15145
diff changeset
   761
    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
   762
eab7de0d0a31 Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents: 15145
diff changeset
   763
    val command_withmetainfo: string -> string -> string ->
16534
wenzelm
parents: 16486
diff changeset
   764
      (token list ->
wenzelm
parents: 16486
diff changeset
   765
       ((Toplevel.transition -> Toplevel.transition) * metainfo list) *
15146
eab7de0d0a31 Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents: 15145
diff changeset
   766
       token list) -> parser
15254
10cfd6a14682 Simplification to symbol processing; put quotes around theory name in message.
aspinall
parents: 15253
diff changeset
   767
10cfd6a14682 Simplification to symbol processing; put quotes around theory name in message.
aspinall
parents: 15253
diff changeset
   768
   We'd also like to render terms as they appear in output, but this
16534
wenzelm
parents: 16486
diff changeset
   769
   will be difficult because inner syntax is extensible and we don't
15254
10cfd6a14682 Simplification to symbol processing; put quotes around theory name in message.
aspinall
parents: 15253
diff changeset
   770
   have the correct syntax to hand when just doing outer parsing
16534
wenzelm
parents: 16486
diff changeset
   771
   without execution.  A reasonable approximation could
15254
10cfd6a14682 Simplification to symbol processing; put quotes around theory name in message.
aspinall
parents: 15253
diff changeset
   772
   perhaps be obtained by using the syntax of the current context.
16534
wenzelm
parents: 16486
diff changeset
   773
   However, this would mean more mess trying to pick out terms,
15254
10cfd6a14682 Simplification to symbol processing; put quotes around theory name in message.
aspinall
parents: 15253
diff changeset
   774
   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
   775
   seems necessary.
15146
eab7de0d0a31 Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents: 15145
diff changeset
   776
*)
eab7de0d0a31 Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents: 15145
diff changeset
   777
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   778
local
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   779
    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
   780
    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
   781
    fun empty elt = [XML.element elt [] []]
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   782
15210
4ff917a91e16 Remove double escaping of backslash in PGML. Remove use of character refs in <whitespace>
aspinall
parents: 15208
diff changeset
   783
    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
   784
15146
eab7de0d0a31 Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents: 15145
diff changeset
   785
    (* 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
   786
    val sync = OuterSyntax.scan "\\<^sync>";
eab7de0d0a31 Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents: 15145
diff changeset
   787
16534
wenzelm
parents: 16486
diff changeset
   788
    fun named_item_elt_with nameattr toks str elt nameP objtyp =
wenzelm
parents: 16486
diff changeset
   789
        let
wenzelm
parents: 16486
diff changeset
   790
            val name = (fst (nameP (toks@sync)))
wenzelm
parents: 16486
diff changeset
   791
                        handle _ => (error ("Error occurred in name parser for " ^ elt ^
wenzelm
parents: 16486
diff changeset
   792
                                            "(objtype: " ^ objtyp ^ ")");
wenzelm
parents: 16486
diff changeset
   793
                                     "")
wenzelm
parents: 16486
diff changeset
   794
wenzelm
parents: 16486
diff changeset
   795
        in
wenzelm
parents: 16486
diff changeset
   796
            [XML.element elt
wenzelm
parents: 16486
diff changeset
   797
                         ((if name="" then [] else [(nameattr, name)])@
wenzelm
parents: 16486
diff changeset
   798
                          (if objtyp="" then [] else [("objtype", objtyp)]))
wenzelm
parents: 16486
diff changeset
   799
                         ([XML.text str])]
wenzelm
parents: 16486
diff changeset
   800
        end
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   801
15146
eab7de0d0a31 Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents: 15145
diff changeset
   802
    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
   803
    val thmnamed_item_elt = named_item_elt_with "thmname"
16534
wenzelm
parents: 16486
diff changeset
   804
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   805
    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
   806
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   807
    (* 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
   808
       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
   809
16534
wenzelm
parents: 16486
diff changeset
   810
    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
   811
16534
wenzelm
parents: 16486
diff changeset
   812
    fun get_keywords_classification_table () =
wenzelm
parents: 16486
diff changeset
   813
        case (!keywords_classification_table) of
wenzelm
parents: 16486
diff changeset
   814
            SOME t => t
wenzelm
parents: 16486
diff changeset
   815
          | NONE => (let
wenzelm
parents: 16486
diff changeset
   816
                         val tab = Library.foldl (fn (tab,(c,_,k,_))=>Symtab.update((c,k),tab))
wenzelm
parents: 16486
diff changeset
   817
                                         (Symtab.empty,OuterSyntax.dest_parsers())
wenzelm
parents: 16486
diff changeset
   818
                     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
   819
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   820
16534
wenzelm
parents: 16486
diff changeset
   821
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   822
    fun xmls_of_thy_begin (name,toks,str) = (* see isar_syn.ML/theoryP *)
16534
wenzelm
parents: 16486
diff changeset
   823
        let
wenzelm
parents: 16486
diff changeset
   824
            val ((thyname,imports,files),_) = ThyHeader.args (toks@sync)
wenzelm
parents: 16486
diff changeset
   825
        in
wenzelm
parents: 16486
diff changeset
   826
            markup_text_attrs str "opentheory"
wenzelm
parents: 16486
diff changeset
   827
                              ([("thyname",thyname)] @
wenzelm
parents: 16486
diff changeset
   828
                               (if imports=[] then [] else
wenzelm
parents: 16486
diff changeset
   829
                                [("parentnames", (space_implode ";" imports) ^ ";")]))
wenzelm
parents: 16486
diff changeset
   830
        end
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   831
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   832
    fun xmls_of_thy_decl (name,toks,str) = (* see isar_syn.ML/thy_decl cases  *)
16534
wenzelm
parents: 16486
diff changeset
   833
        let
wenzelm
parents: 16486
diff changeset
   834
            (* NB: PGIP only deals with single name bindings at the moment;
wenzelm
parents: 16486
diff changeset
   835
               potentially we could markup grouped definitions several times but
wenzelm
parents: 16486
diff changeset
   836
               that might suggest the wrong structure to the editor?
wenzelm
parents: 16486
diff changeset
   837
               Better alternative would be to put naming closer around text,
wenzelm
parents: 16486
diff changeset
   838
               but to do that we'd be much better off modifying the real parser
wenzelm
parents: 16486
diff changeset
   839
               instead of reconstructing it here. *)
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   840
16534
wenzelm
parents: 16486
diff changeset
   841
            val plain_items = (* no names, unimportant names, or too difficult *)
wenzelm
parents: 16486
diff changeset
   842
                ["defaultsort","arities","judgement","finalconsts",
wenzelm
parents: 16486
diff changeset
   843
                 "syntax", "nonterminals", "translations",
wenzelm
parents: 16486
diff changeset
   844
                 "global", "local", "hide",
wenzelm
parents: 16486
diff changeset
   845
                 "ML_setup", "setup", "method_setup",
wenzelm
parents: 16486
diff changeset
   846
                 "parse_ast_translation", "parse_translation", "print_translation",
wenzelm
parents: 16486
diff changeset
   847
                 "typed_print_translation", "print_ast_translation", "token_translation",
wenzelm
parents: 16486
diff changeset
   848
                 "oracle",
wenzelm
parents: 16486
diff changeset
   849
                 "declare"]
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   850
16534
wenzelm
parents: 16486
diff changeset
   851
            val plain_item   = markup_text str "theoryitem"
wenzelm
parents: 16486
diff changeset
   852
            val comment_item = markup_text str "litcomment"
wenzelm
parents: 16486
diff changeset
   853
            val named_item   = named_item_elt toks str "theoryitem"
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   854
16534
wenzelm
parents: 16486
diff changeset
   855
            val opt_overloaded = P.opt_keyword "overloaded";
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   856
16534
wenzelm
parents: 16486
diff changeset
   857
            val thmnameP = (* see isar_syn.ML/theoremsP *)
wenzelm
parents: 16486
diff changeset
   858
                let
wenzelm
parents: 16486
diff changeset
   859
                    val name_facts = P.and_list1 ((P.opt_thm_name "=" --| P.xthms1) >> #1)
16958
1b4a3110c64a P.opt_locale_target;
wenzelm
parents: 16896
diff changeset
   860
                    val theoremsP = P.opt_locale_target |-- name_facts >> (fn [] => "" | x::_ => x)
16534
wenzelm
parents: 16486
diff changeset
   861
                in
wenzelm
parents: 16486
diff changeset
   862
                    theoremsP
wenzelm
parents: 16486
diff changeset
   863
                end
wenzelm
parents: 16486
diff changeset
   864
        in
wenzelm
parents: 16486
diff changeset
   865
            (* TODO: ideally we would like to render terms properly, just as they are
wenzelm
parents: 16486
diff changeset
   866
               in output. This implies using PGML for symbols and variables/atoms.
wenzelm
parents: 16486
diff changeset
   867
               BUT it's rather tricky without having the correct concrete syntax to hand,
wenzelm
parents: 16486
diff changeset
   868
               and even if we did, we'd have to mess around here a whole lot more first
wenzelm
parents: 16486
diff changeset
   869
               to pick out the terms from the syntax. *)
15254
10cfd6a14682 Simplification to symbol processing; put quotes around theory name in message.
aspinall
parents: 15253
diff changeset
   870
16534
wenzelm
parents: 16486
diff changeset
   871
            if (name mem plain_items) then plain_item
wenzelm
parents: 16486
diff changeset
   872
            else case name of
wenzelm
parents: 16486
diff changeset
   873
                     "text"      => comment_item
wenzelm
parents: 16486
diff changeset
   874
                   | "text_raw"  => comment_item
wenzelm
parents: 16486
diff changeset
   875
                   | "typedecl"  => named_item (P.type_args |-- P.name) "type"
wenzelm
parents: 16486
diff changeset
   876
                   | "types"     => named_item (P.type_args |-- P.name) "type"
wenzelm
parents: 16486
diff changeset
   877
                   | "classes"   => named_item P.name "class"
wenzelm
parents: 16486
diff changeset
   878
                   | "classrel"  => named_item P.name "class"
wenzelm
parents: 16486
diff changeset
   879
                   | "consts"    => named_item (P.const >> #1) "term"
wenzelm
parents: 16486
diff changeset
   880
                   | "axioms"    => named_item (P.spec_name >> (#1 o #1)) "theorem"
wenzelm
parents: 16486
diff changeset
   881
                   | "defs"      => named_item (opt_overloaded |-- P.spec_name >> (#1 o #1)) "theorem"
wenzelm
parents: 16486
diff changeset
   882
                   | "constdefs" => named_item P.name (* FIXME: heavily simplified/wrong *) "term"
wenzelm
parents: 16486
diff changeset
   883
                   | "theorems"  => named_item thmnameP "thmset"
wenzelm
parents: 16486
diff changeset
   884
                   | "lemmas"    => named_item thmnameP "thmset"
wenzelm
parents: 16486
diff changeset
   885
                   | "oracle"    => named_item P.name "oracle"
wenzelm
parents: 16486
diff changeset
   886
                   | "locale"    => named_item ((P.opt_keyword "open" >> not) |-- P.name) "locale"
wenzelm
parents: 16486
diff changeset
   887
                   | _ => (parse_warning ("Unrecognized thy-decl command: " ^ name); plain_item)
wenzelm
parents: 16486
diff changeset
   888
        end
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   889
16534
wenzelm
parents: 16486
diff changeset
   890
    fun xmls_of_thy_goal (name,toks,str) =
wenzelm
parents: 16486
diff changeset
   891
        let
wenzelm
parents: 16486
diff changeset
   892
            (* 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
   893
         val statement = P.and_list1 (P.opt_thm_name ":" -- Scan.repeat1 P.propp);
16534
wenzelm
parents: 16486
diff changeset
   894
         val general_statement =
wenzelm
parents: 16486
diff changeset
   895
            statement >> pair [] || Scan.repeat P.locale_elem_or_expr -- (P.$$$ "shows" |-- statement);
wenzelm
parents: 16486
diff changeset
   896
wenzelm
parents: 16486
diff changeset
   897
            val gen_theoremP =
16958
1b4a3110c64a P.opt_locale_target;
wenzelm
parents: 16896
diff changeset
   898
                P.opt_locale_target -- Scan.optional (P.opt_thm_name ":" --|
15146
eab7de0d0a31 Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents: 15145
diff changeset
   899
                 Scan.ahead (P.locale_keyword || P.$$$ "shows")) ("", []) --
16534
wenzelm
parents: 16486
diff changeset
   900
                                 general_statement >> (fn ((locale, a), (elems, concl)) =>
wenzelm
parents: 16486
diff changeset
   901
                                                         fst a) (* a : (bstring * Args.src list) *)
15146
eab7de0d0a31 Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents: 15145
diff changeset
   902
16958
1b4a3110c64a P.opt_locale_target;
wenzelm
parents: 16896
diff changeset
   903
            val nameP = P.opt_locale_target |-- (Scan.optional ((P.opt_thm_name ":") >> #1) "")
16534
wenzelm
parents: 16486
diff changeset
   904
            (* TODO: add preference values for attributes
wenzelm
parents: 16486
diff changeset
   905
               val prefval = XML.element "prefval" [("name","thm-kind"),("value",name)]
wenzelm
parents: 16486
diff changeset
   906
            *)
wenzelm
parents: 16486
diff changeset
   907
        in
wenzelm
parents: 16486
diff changeset
   908
            (thmnamed_item_elt toks str "opengoal" nameP "") @
wenzelm
parents: 16486
diff changeset
   909
            (empty "openblock")
wenzelm
parents: 16486
diff changeset
   910
        end
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   911
17217
954c0f265203 added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents: 17057
diff changeset
   912
    fun xmls_of_qed (name,markup) =
954c0f265203 added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents: 17057
diff changeset
   913
        let val qedmarkup  =
954c0f265203 added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents: 17057
diff changeset
   914
                (case name of
954c0f265203 added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents: 17057
diff changeset
   915
                     "sorry" => markup "postponegoal"
954c0f265203 added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents: 17057
diff changeset
   916
                   | "oops"  => markup "giveupgoal"
954c0f265203 added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents: 17057
diff changeset
   917
                   | "done"  => markup "closegoal"
954c0f265203 added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents: 17057
diff changeset
   918
                   | "by"    => markup "closegoal"  (* nested or toplevel *)
954c0f265203 added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents: 17057
diff changeset
   919
                   | "qed"   => markup "closegoal"  (* nested or toplevel *)
954c0f265203 added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents: 17057
diff changeset
   920
                   | "."     => markup "closegoal"  (* nested or toplevel *)
954c0f265203 added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents: 17057
diff changeset
   921
                   | ".."    => markup "closegoal"  (* nested or toplevel *)
954c0f265203 added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents: 17057
diff changeset
   922
                   | other => (* default to closegoal: may be wrong for extns *)
954c0f265203 added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents: 17057
diff changeset
   923
                                  (parse_warning
954c0f265203 added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents: 17057
diff changeset
   924
                                       ("Unrecognized qed command: " ^ quote other);
954c0f265203 added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents: 17057
diff changeset
   925
                                       markup "closegoal"))
954c0f265203 added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents: 17057
diff changeset
   926
        in qedmarkup @ (empty "closeblock") end
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   927
16534
wenzelm
parents: 16486
diff changeset
   928
    fun xmls_of_kind kind (name,toks,str) =
wenzelm
parents: 16486
diff changeset
   929
    let val markup = markup_text str in
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   930
    case kind of
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   931
      "control"        => markup "badcmd"
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   932
    | "diag"           => markup "spuriouscmd"
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   933
    (* theory/files *)
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   934
    | "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
   935
    | "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
   936
    | "theory-heading" => markup "litcomment"
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   937
    | "theory-script"  => markup "theorystep"
15146
eab7de0d0a31 Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents: 15145
diff changeset
   938
    | "theory-end"     => markup "closetheory"
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   939
    (* proof control *)
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   940
    | "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
   941
    | "proof-heading"  => markup "litcomment"
15225
68ab0f4eb457 Add openblock/closeblock to other opengoal/closegoal elements
aspinall
parents: 15220
diff changeset
   942
    | "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
   943
    | "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
   944
    | "proof-open"     => (empty "openblock") @ (markup "proofstep")
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   945
    | "proof-close"    => (markup "proofstep") @ (empty "closeblock")
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   946
    | "proof-script"   => markup "proofstep"
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   947
    | "proof-chain"    => markup "proofstep"
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   948
    | "proof-decl"     => markup "proofstep"
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   949
    | "proof-asm"      => markup "proofstep"
15289
1d2dba93ef08 Markup obtain as introducing a nested goal.
aspinall
parents: 15286
diff changeset
   950
    | "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
   951
    | "qed"            => xmls_of_qed (name,markup)
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   952
    | "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
   953
    | "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
   954
    | 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
   955
      (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
   956
       markup "spuriouscmd")
16534
wenzelm
parents: 16486
diff changeset
   957
    end
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   958
in
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   959
16534
wenzelm
parents: 16486
diff changeset
   960
fun xmls_of_transition (name,str,toks) =
wenzelm
parents: 16486
diff changeset
   961
   let
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   962
       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
   963
   in case classification of
16534
wenzelm
parents: 16486
diff changeset
   964
          SOME k => (xmls_of_kind k (name,toks,str))
wenzelm
parents: 16486
diff changeset
   965
        | NONE => (* an uncategorized keyword ignored for undo (maybe wrong) *)
wenzelm
parents: 16486
diff changeset
   966
          (parse_warning ("Uncategorized command found: " ^ name ^ " -- using spuriouscmd");
wenzelm
parents: 16486
diff changeset
   967
           markup_text str "spuriouscmd")
wenzelm
parents: 16486
diff changeset
   968
   end
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   969
15191
5ca1fd9dec83 Support parsing of -- {* comments *}. Add extra output channels.
aspinall
parents: 15173
diff changeset
   970
fun markup_toks [] _ = []
5ca1fd9dec83 Support parsing of -- {* comments *}. Add extra output channels.
aspinall
parents: 15173
diff changeset
   971
  | 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
   972
5ca1fd9dec83 Support parsing of -- {* comments *}. Add extra output channels.
aspinall
parents: 15173
diff changeset
   973
fun markup_comment_whs [] = []
5ca1fd9dec83 Support parsing of -- {* comments *}. Add extra output channels.
aspinall
parents: 15173
diff changeset
   974
  | markup_comment_whs (toks as t::ts) = (* this would be a lot neater if we could match on toks! *)
16534
wenzelm
parents: 16486
diff changeset
   975
    let
wenzelm
parents: 16486
diff changeset
   976
        val (prewhs,rest) = take_prefix (OuterLex.is_kind OuterLex.Space) toks
wenzelm
parents: 16486
diff changeset
   977
    in
wenzelm
parents: 16486
diff changeset
   978
        if (prewhs <> []) then
wenzelm
parents: 16486
diff changeset
   979
            whitespace (implode (map OuterLex.unparse prewhs))
wenzelm
parents: 16486
diff changeset
   980
            :: (markup_comment_whs rest)
wenzelm
parents: 16486
diff changeset
   981
        else
wenzelm
parents: 16486
diff changeset
   982
            (markup_text (OuterLex.unparse t) "comment") @
wenzelm
parents: 16486
diff changeset
   983
            (markup_comment_whs ts)
15191
5ca1fd9dec83 Support parsing of -- {* comments *}. Add extra output channels.
aspinall
parents: 15173
diff changeset
   984
    end
5ca1fd9dec83 Support parsing of -- {* comments *}. Add extra output channels.
aspinall
parents: 15173
diff changeset
   985
5ca1fd9dec83 Support parsing of -- {* comments *}. Add extra output channels.
aspinall
parents: 15173
diff changeset
   986
fun xmls_pre_cmd [] = ([],[])
16534
wenzelm
parents: 16486
diff changeset
   987
  | xmls_pre_cmd toks =
wenzelm
parents: 16486
diff changeset
   988
    let
wenzelm
parents: 16486
diff changeset
   989
        (* an extra token is needed to terminate the command *)
wenzelm
parents: 16486
diff changeset
   990
        val sync = OuterSyntax.scan "\\<^sync>";
wenzelm
parents: 16486
diff changeset
   991
        val spaceP = Scan.bulk (Scan.one (fn t =>not (OuterLex.is_proper t)) >> OuterLex.val_of) >> implode
wenzelm
parents: 16486
diff changeset
   992
        val text_with_whs =
wenzelm
parents: 16486
diff changeset
   993
            ((spaceP || Scan.succeed "") --
wenzelm
parents: 16486
diff changeset
   994
             (P.short_ident || P.long_ident || P.sym_ident || P.string || P.number || P.verbatim) >> op^)
wenzelm
parents: 16486
diff changeset
   995
             -- (spaceP || Scan.succeed "") >> op^
wenzelm
parents: 16486
diff changeset
   996
        val (prewhs,rest1) = take_prefix (not o OuterLex.is_proper) (toks@sync)
15191
5ca1fd9dec83 Support parsing of -- {* comments *}. Add extra output channels.
aspinall
parents: 15173
diff changeset
   997
        (* NB: this collapses  litcomment,(litcomment|whitespace)* to a single litcomment *)
16534
wenzelm
parents: 16486
diff changeset
   998
        val (_,rest2) = (Scan.bulk (P.$$$ "--" |-- text_with_whs) >> implode || Scan.succeed "") rest1
wenzelm
parents: 16486
diff changeset
   999
        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
  1000
    in
16534
wenzelm
parents: 16486
diff changeset
  1001
        ((markup_comment_whs prewhs) @
wenzelm
parents: 16486
diff changeset
  1002
         (if (length rest2 = length rest1)  then []
wenzelm
parents: 16486
diff changeset
  1003
          else markup_text (implode
wenzelm
parents: 16486
diff changeset
  1004
                                (map OuterLex.unparse (Library.take (length rest1 - length rest2, rest1))))
wenzelm
parents: 16486
diff changeset
  1005
               "litcomment") @
wenzelm
parents: 16486
diff changeset
  1006
         (markup_comment_whs postwhs),
wenzelm
parents: 16486
diff changeset
  1007
         Library.take (length rest3 - 1,rest3))
15191
5ca1fd9dec83 Support parsing of -- {* comments *}. Add extra output channels.
aspinall
parents: 15173
diff changeset
  1008
    end
5ca1fd9dec83 Support parsing of -- {* comments *}. Add extra output channels.
aspinall
parents: 15173
diff changeset
  1009
16534
wenzelm
parents: 16486
diff changeset
  1010
fun xmls_of_impropers toks =
wenzelm
parents: 16486
diff changeset
  1011
    let
wenzelm
parents: 16486
diff changeset
  1012
        val (xmls,rest) = xmls_pre_cmd toks
15191
5ca1fd9dec83 Support parsing of -- {* comments *}. Add extra output channels.
aspinall
parents: 15173
diff changeset
  1013
    in
16534
wenzelm
parents: 16486
diff changeset
  1014
        xmls @ (markup_toks rest "unparseable")
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1015
    end
16534
wenzelm
parents: 16486
diff changeset
  1016
wenzelm
parents: 16486
diff changeset
  1017
fun markup_unparseable str = markup_text str "unparseable"
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
  1018
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1019
end
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1020
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1021
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1022
local
16534
wenzelm
parents: 16486
diff changeset
  1023
    (* we have to weave together the whitespace/comments with proper tokens
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1024
       to reconstruct the input. *)
15191
5ca1fd9dec83 Support parsing of -- {* comments *}. Add extra output channels.
aspinall
parents: 15173
diff changeset
  1025
    (* 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
  1026
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1027
    fun match_tokens ([],us,vs) = (rev vs,us)  (* used, unused *)
16534
wenzelm
parents: 16486
diff changeset
  1028
      | match_tokens (t::ts,w::ws,vs) =
wenzelm
parents: 16486
diff changeset
  1029
        if (t = w) then match_tokens (ts,ws,w::vs)
wenzelm
parents: 16486
diff changeset
  1030
        else match_tokens (t::ts,ws,w::vs)
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1031
      | 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
  1032
in
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1033
    fun xmls_of_str str =
16534
wenzelm
parents: 16486
diff changeset
  1034
    let
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1035
       (* 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
  1036
       fun parse_loop ([],[],xmls) = xmls
16534
wenzelm
parents: 16486
diff changeset
  1037
         | parse_loop ([],itoks,xmls) = xmls @ (xmls_of_impropers itoks)
wenzelm
parents: 16486
diff changeset
  1038
         | parse_loop ((nm,toks,_)::trs,itoks,xmls) =
wenzelm
parents: 16486
diff changeset
  1039
           let
wenzelm
parents: 16486
diff changeset
  1040
               (* first proper token after whitespace/litcomment/whitespace is command *)
wenzelm
parents: 16486
diff changeset
  1041
               val (xmls_pre_cmd,cmditoks') = xmls_pre_cmd itoks
wenzelm
parents: 16486
diff changeset
  1042
               val (cmdtok,itoks') = case cmditoks' of x::xs => (x,xs)
wenzelm
parents: 16486
diff changeset
  1043
                                                     | _ => error("proof_general/parse_loop impossible")
wenzelm
parents: 16486
diff changeset
  1044
               val (utoks,itoks'') = match_tokens (toks,itoks',[])
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1045
               (* 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
  1046
16534
wenzelm
parents: 16486
diff changeset
  1047
               val str = implode (map OuterLex.unparse (cmdtok::utoks))
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1048
16534
wenzelm
parents: 16486
diff changeset
  1049
               val xmls_tr  = xmls_of_transition (nm,str,toks)
wenzelm
parents: 16486
diff changeset
  1050
           in
wenzelm
parents: 16486
diff changeset
  1051
               parse_loop(trs,itoks'',xmls @ xmls_pre_cmd @ xmls_tr)
wenzelm
parents: 16486
diff changeset
  1052
           end
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1053
    in
16534
wenzelm
parents: 16486
diff changeset
  1054
        (let val toks = OuterSyntax.scan str
wenzelm
parents: 16486
diff changeset
  1055
         in
wenzelm
parents: 16486
diff changeset
  1056
             parse_loop (OuterSyntax.read toks, toks, [])
wenzelm
parents: 16486
diff changeset
  1057
         end)
wenzelm
parents: 16486
diff changeset
  1058
           handle _ => markup_unparseable str
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1059
    end
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1060
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1061
16534
wenzelm
parents: 16486
diff changeset
  1062
fun parsescript str attrs =
wenzelm
parents: 16486
diff changeset
  1063
    let
wenzelm
parents: 16486
diff changeset
  1064
        val _ = start_delay_msgs ()  (* accumulate error messages to put inside parseresult *)
wenzelm
parents: 16486
diff changeset
  1065
        val xmls = xmls_of_str str
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
  1066
        val errs = end_delayed_msgs ()
16534
wenzelm
parents: 16486
diff changeset
  1067
     in
wenzelm
parents: 16486
diff changeset
  1068
        issue_pgips [XML.element "parseresult" attrs (errs@xmls)]
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
  1069
    end
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1070
end
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
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
(**** PGIP:  Isabelle -> Interface ****)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1075
16534
wenzelm
parents: 16486
diff changeset
  1076
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
  1077
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
  1078
16798
36d34186741b Add acceptedpgipelems message
aspinall
parents: 16791
diff changeset
  1079
(* TODO: would be cleaner to define a datatype here for the accepted elements,
36d34186741b Add acceptedpgipelems message
aspinall
parents: 16791
diff changeset
  1080
   and mapping functions to/from strings.  At the moment this list must
36d34186741b Add acceptedpgipelems message
aspinall
parents: 16791
diff changeset
  1081
   coincide with the strings in the function process_pgip_element. *)
17217
954c0f265203 added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents: 17057
diff changeset
  1082
val isabelle_acceptedpgipelems =
16798
36d34186741b Add acceptedpgipelems message
aspinall
parents: 16791
diff changeset
  1083
    ["askpgip","askpgml","askprefs","getpref","setpref",
36d34186741b Add acceptedpgipelems message
aspinall
parents: 16791
diff changeset
  1084
     "proverinit","proverexit","startquiet","stopquiet",
36d34186741b Add acceptedpgipelems message
aspinall
parents: 16791
diff changeset
  1085
     "pgmlsymbolson", "pgmlsymbolsoff",
36d34186741b Add acceptedpgipelems message
aspinall
parents: 16791
diff changeset
  1086
     "dostep", "undostep", "redostep", "abortgoal", "forget", "restoregoal",
36d34186741b Add acceptedpgipelems message
aspinall
parents: 16791
diff changeset
  1087
     "askids", "showid", "askguise",
36d34186741b Add acceptedpgipelems message
aspinall
parents: 16791
diff changeset
  1088
     "parsescript",
36d34186741b Add acceptedpgipelems message
aspinall
parents: 16791
diff changeset
  1089
     "showproofstate", "showctxt", "searchtheorems", "setlinewidth", "viewdoc",
36d34186741b Add acceptedpgipelems message
aspinall
parents: 16791
diff changeset
  1090
     "doitem", "undoitem", "redoitem", "abortheory",
36d34186741b Add acceptedpgipelems message
aspinall
parents: 16791
diff changeset
  1091
     "retracttheory", "loadfile", "openfile", "closefile",
36d34186741b Add acceptedpgipelems message
aspinall
parents: 16791
diff changeset
  1092
     "abortfile", "changecwd", "systemcmd"];
36d34186741b Add acceptedpgipelems message
aspinall
parents: 16791
diff changeset
  1093
16534
wenzelm
parents: 16486
diff changeset
  1094
fun usespgip () =
17217
954c0f265203 added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents: 17057
diff changeset
  1095
    issue_pgip
954c0f265203 added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents: 17057
diff changeset
  1096
        "usespgip"
954c0f265203 added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents: 17057
diff changeset
  1097
        [("version", isabelle_pgip_version_supported)]
954c0f265203 added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents: 17057
diff changeset
  1098
        (XML.element "acceptedpgipelems" []
954c0f265203 added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents: 17057
diff changeset
  1099
                     (map (fn s=>XML.element "pgipelem"
954c0f265203 added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents: 17057
diff changeset
  1100
                                             [] (* if threads: possibility to add async here *)
954c0f265203 added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents: 17057
diff changeset
  1101
                                             [s])
954c0f265203 added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents: 17057
diff changeset
  1102
                          isabelle_acceptedpgipelems))
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1103
16534
wenzelm
parents: 16486
diff changeset
  1104
fun usespgml () =
16798
36d34186741b Add acceptedpgipelems message
aspinall
parents: 16791
diff changeset
  1105
    issue_pgipe "usespgml" [("version", isabelle_pgml_version_supported)]
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1106
16534
wenzelm
parents: 16486
diff changeset
  1107
fun hasprefs () =
15570
8d8c70b41bab Move towards standard functions.
skalberg
parents: 15531
diff changeset
  1108
    List.app (fn (prefcat, prefs) =>
16534
wenzelm
parents: 16486
diff changeset
  1109
            issue_pgips [XML.element "hasprefs" [("prefcategory",prefcat)]
wenzelm
parents: 16486
diff changeset
  1110
                 (map (fn (name, (descr, (ty, (default,_),_))) =>
wenzelm
parents: 16486
diff changeset
  1111
                       XML.element "haspref" [("name", name),
wenzelm
parents: 16486
diff changeset
  1112
                                              ("descr", descr),
wenzelm
parents: 16486
diff changeset
  1113
                                              ("default", default)]
16798
36d34186741b Add acceptedpgipelems message
aspinall
parents: 16791
diff changeset
  1114
                       [ty]) prefs)]) (!preferences)
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1115
15570
8d8c70b41bab Move towards standard functions.
skalberg
parents: 15531
diff changeset
  1116
fun allprefs () = Library.foldl (op @) ([], map snd (!preferences))
16534
wenzelm
parents: 16486
diff changeset
  1117
wenzelm
parents: 16486
diff changeset
  1118
fun setpref name value =
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1119
    (case assoc (allprefs(), name) of
16534
wenzelm
parents: 16486
diff changeset
  1120
         NONE => warning ("Unknown pref: " ^ quote name)
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15472
diff changeset
  1121
       | SOME (_, (_, _, set)) => set value);
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1122
16534
wenzelm
parents: 16486
diff changeset
  1123
fun getpref name =
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1124
    (case assoc (allprefs(), name) of
16534
wenzelm
parents: 16486
diff changeset
  1125
         NONE => warning ("Unknown pref: " ^ quote name)
wenzelm
parents: 16486
diff changeset
  1126
       | SOME (_, (_, (_,get), _)) =>
wenzelm
parents: 16486
diff changeset
  1127
           issue_pgip "prefval" [("name", name)] (get ()));
15134
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
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1130
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1131
(**** PGIP:  Interface -> Isabelle/Isar ****)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1132
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1133
exception PGIP of string;
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1134
exception PGIP_QUIT;
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1135
16534
wenzelm
parents: 16486
diff changeset
  1136
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1137
(* Sending commands to Isar *)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1138
16534
wenzelm
parents: 16486
diff changeset
  1139
fun isarcmd s =
wenzelm
parents: 16486
diff changeset
  1140
    s |> OuterSyntax.scan |> OuterSyntax.read
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1141
      |> 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
  1142
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1143
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
  1144
  | xmltext [] = ""
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1145
  | xmltext _ = raise PGIP "Expected text (PCDATA/CDATA)"
16534
wenzelm
parents: 16486
diff changeset
  1146
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1147
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
  1148
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1149
16791
31678cf364b1 Add management for current working directory
aspinall
parents: 16789
diff changeset
  1150
(* load an arbitrary file (must be .thy or .ML) *)
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1151
16534
wenzelm
parents: 16486
diff changeset
  1152
fun use_thy_or_ml_file file =
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1153
    let
16534
wenzelm
parents: 16486
diff changeset
  1154
        val (path,extn) = Path.split_ext (Path.unpack file)
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1155
    in
16534
wenzelm
parents: 16486
diff changeset
  1156
        case extn of
wenzelm
parents: 16486
diff changeset
  1157
            "" => isarcmd ("use_thy " ^ (quote (Path.pack path)))
wenzelm
parents: 16486
diff changeset
  1158
          | "thy" => isarcmd ("use_thy " ^ (quote (Path.pack path)))
wenzelm
parents: 16486
diff changeset
  1159
          | "ML" => isarcmd ("use " ^ quote file)
wenzelm
parents: 16486
diff changeset
  1160
          | other => error ("Don't know how to read a file with extension " ^ other)
wenzelm
parents: 16486
diff changeset
  1161
    end
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1162
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1163
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
  1164
(* Proof control commands *)
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1165
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
  1166
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
  1167
  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
  1168
16534
wenzelm
parents: 16486
diff changeset
  1169
  fun xmlattr attr attrs =
wenzelm
parents: 16486
diff changeset
  1170
      (case xmlattro attr attrs of
wenzelm
parents: 16486
diff changeset
  1171
           SOME value => value
wenzelm
parents: 16486
diff changeset
  1172
         | 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
  1173
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
  1174
  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
  1175
  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
  1176
  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
  1177
  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
  1178
  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
  1179
  val dirname_attr = xmlattr "dir"
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1180
  fun comment x = "(* " ^ x ^ " *)"
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1181
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
  1182
  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
  1183
      case Url.unpack url of
16534
wenzelm
parents: 16486
diff changeset
  1184
          (Url.File path) => File.platform_path path
wenzelm
parents: 16486
diff changeset
  1185
        | _ => 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
  1186
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
  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
  1188
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1189
  val topthy = Toplevel.theory_of o Toplevel.get_state
16440
9b6e6d5fba05 Context.theory_name;
wenzelm
parents: 16259
diff changeset
  1190
  val topthy_name = Context.theory_name o topthy
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1191
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15472
diff changeset
  1192
  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
  1193
16791
31678cf364b1 Add management for current working directory
aspinall
parents: 16789
diff changeset
  1194
  (* Path management: we allow theory files to have dependencies
31678cf364b1 Add management for current working directory
aspinall
parents: 16789
diff changeset
  1195
     in their own directory, but when we change directory for a new
31678cf364b1 Add management for current working directory
aspinall
parents: 16789
diff changeset
  1196
     file we remove the path.  Leaving it there can cause confusion
31678cf364b1 Add management for current working directory
aspinall
parents: 16789
diff changeset
  1197
     with difference in batch mode.a  NB: PGIP does not assume
31678cf364b1 Add management for current working directory
aspinall
parents: 16789
diff changeset
  1198
     that the prover has a load path. *)
17217
954c0f265203 added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents: 17057
diff changeset
  1199
  local
16791
31678cf364b1 Add management for current working directory
aspinall
parents: 16789
diff changeset
  1200
      val current_working_dir = ref (NONE : string option)
31678cf364b1 Add management for current working directory
aspinall
parents: 16789
diff changeset
  1201
  in
17217
954c0f265203 added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents: 17057
diff changeset
  1202
      fun changecwd dir =
954c0f265203 added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents: 17057
diff changeset
  1203
          (case (!current_working_dir) of
954c0f265203 added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents: 17057
diff changeset
  1204
               NONE => ()
16791
31678cf364b1 Add management for current working directory
aspinall
parents: 16789
diff changeset
  1205
             | SOME dir => ThyLoad.del_path dir;
17217
954c0f265203 added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents: 17057
diff changeset
  1206
           ThyLoad.add_path dir;
954c0f265203 added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents: 17057
diff changeset
  1207
           current_working_dir := SOME dir)
16791
31678cf364b1 Add management for current working directory
aspinall
parents: 16789
diff changeset
  1208
  end
31678cf364b1 Add management for current working directory
aspinall
parents: 16789
diff changeset
  1209
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
  1210
  val topnode = Toplevel.node_of o Toplevel.get_state
16534
wenzelm
parents: 16486
diff changeset
  1211
  fun topproofpos () = (case topnode() of Toplevel.Proof ph => SOME(ProofHistory.position ph)
wenzelm
parents: 16486
diff changeset
  1212
                                        | _ => NONE) handle Toplevel.UNDEF => NONE
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1213
in
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1214
16534
wenzelm
parents: 16486
diff changeset
  1215
fun process_pgip_element pgipxml = (case pgipxml of
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1216
  (XML.Text t) => warning ("Ignored text in PGIP packet: \n" ^ t)
16534
wenzelm
parents: 16486
diff changeset
  1217
| (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
  1218
  (case elem of
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1219
       (* protocol config *)
16534
wenzelm
parents: 16486
diff changeset
  1220
       "askpgip"        => (pgip_emacs_compatibility_flag:=false; (* PG>=3.6 or other PGIP interface *)
wenzelm
parents: 16486
diff changeset
  1221
                            usespgip (); send_pgip_config ())
wenzelm
parents: 16486
diff changeset
  1222
     | "askpgml"        => usespgml ()
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1223
     (* proverconfig *)
16534
wenzelm
parents: 16486
diff changeset
  1224
     | "askprefs"       => hasprefs ()
wenzelm
parents: 16486
diff changeset
  1225
     | "getpref"        => getpref (name_attr attrs)
wenzelm
parents: 16486
diff changeset
  1226
     | "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
  1227
     (* provercontrol *)
16534
wenzelm
parents: 16486
diff changeset
  1228
     | "proverinit"     => isar_restart ()
wenzelm
parents: 16486
diff changeset
  1229
     | "proverexit"     => isarcmd "quit"
wenzelm
parents: 16486
diff changeset
  1230
     | "startquiet"     => isarcmd "disable_pr"
wenzelm
parents: 16486
diff changeset
  1231
     | "stopquiet"      => isarcmd "enable_pr"
17217
954c0f265203 added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents: 17057
diff changeset
  1232
     | "pgmlsymbolson"   => change print_mode (insert (op =) Symbol.xsymbolsN)
954c0f265203 added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents: 17057
diff changeset
  1233
     | "pgmlsymbolsoff"  => change print_mode (remove (op =) Symbol.xsymbolsN)
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1234
     (* properproofcmd: proper commands which belong in script *)
15401
ba28d103bada Support PGIP <whitespace>, <dostep>, <doitem> elements as input
aspinall
parents: 15400
diff changeset
  1235
     (* 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
  1236
     (* 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
  1237
     | "opengoal"       => isarscript data
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1238
     | "proofstep"      => isarscript data
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1239
     | "closegoal"      => isarscript data
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1240
     | "giveupgoal"     => isarscript data
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1241
     | "postponegoal"   => isarscript data
16534
wenzelm
parents: 16486
diff changeset
  1242
     | "comment"        => isarscript data  (* NB: should be ignored, but process anyway *)
wenzelm
parents: 16486
diff changeset
  1243
     | "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
  1244
     | "litcomment"     => isarscript data
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1245
     | "spuriouscmd"    => isarscript data
16534
wenzelm
parents: 16486
diff changeset
  1246
     | "badcmd"         => isarscript data
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1247
     (* improperproofcmd: improper commands which *do not* belong in script *)
15401
ba28d103bada Support PGIP <whitespace>, <dostep>, <doitem> elements as input
aspinall
parents: 15400
diff changeset
  1248
     | "dostep"         => isarscript data
15286
b084384960d1 Add <undoitem> for theory-state undos.
aspinall
parents: 15268
diff changeset
  1249
     | "undostep"       => isarcmd "undos_proof 1"
15626
a8f718939500 Support new PGIP commands redostep, redoitem
aspinall
parents: 15570
diff changeset
  1250
     | "redostep"       => isarcmd "redo"
16534
wenzelm
parents: 16486
diff changeset
  1251
     | "abortgoal"      => isarcmd "ProofGeneral.kill_proof"
wenzelm
parents: 16486
diff changeset
  1252
     | "forget"         => error "Not implemented"
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1253
     | "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
  1254
     (* 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
  1255
     | "askids"         => askids (thyname_attro attrs, objtype_attro attrs)
16534
wenzelm
parents: 16486
diff changeset
  1256
     | "showid"         => showid (thyname_attro attrs, objtype_attr attrs, name_attr attrs)
wenzelm
parents: 16486
diff changeset
  1257
     | "askguise"       => send_informguise (!currently_open_file,
wenzelm
parents: 16486
diff changeset
  1258
                                             SOME (topthy_name()) handle Toplevel.UNDEF => NONE,
wenzelm
parents: 16486
diff changeset
  1259
                                             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
  1260
     | "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
  1261
     | "showproofstate" => isarcmd "pr"
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1262
     | "showctxt"       => isarcmd "print_theory"   (* more useful than print_context *)
17217
954c0f265203 added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents: 17057
diff changeset
  1263
     | "searchtheorems" => isarcmd ("thms_containing " ^ xmltext data)
954c0f265203 added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents: 17057
diff changeset
  1264
     | "setlinewidth"   => isarcmd ("pretty_setmargin " ^ xmltext data)
954c0f265203 added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents: 17057
diff changeset
  1265
     | "viewdoc"        => isarcmd ("print_" ^ xmltext data) (* FIXME: isatool doc? *)
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1266
     (* properfilecmd: proper theory-level script commands *)
15401
ba28d103bada Support PGIP <whitespace>, <dostep>, <doitem> elements as input
aspinall
parents: 15400
diff changeset
  1267
     (* 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
  1268
     | "opentheory"     => isarscript data
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1269
     | "theoryitem"     => isarscript data
16534
wenzelm
parents: 16486