--- a/src/Pure/ProofGeneral/proof_general_emacs.ML Sat Jul 07 18:39:20 2007 +0200
+++ b/src/Pure/ProofGeneral/proof_general_emacs.ML Sat Jul 07 18:39:21 2007 +0200
@@ -43,8 +43,7 @@
in
fun setup_xsymbols_output () =
- (Output.add_mode Symbol.xsymbolsN xsymbols_output Symbol.encode_raw;
- Pretty.add_mode Symbol.xsymbolsN Pretty.default_indent Pretty.default_markup);
+ Output.add_mode Symbol.xsymbolsN xsymbols_output Symbol.encode_raw;
end;
@@ -97,6 +96,21 @@
end;
+(* common markup *)
+
+fun proof_general_markup (name, props) =
+ (if name = Markup.promptN then ("", special "372")
+ else if name = Markup.no_stateN orelse name = Markup.stateN
+ then (special "366" ^ "\n", "\n" ^ special "367")
+ else ("", ""))
+ |> (name <> Markup.promptN andalso print_mode_active "test_markup") ?
+ (fn (bg, en) =>
+ (bg ^ enclose "<" ">" (space_implode " " (name :: map XML.attribute props)),
+ enclose "</" ">" name ^ en));
+
+val _ = Pretty.add_mode proof_generalN Pretty.default_indent proof_general_markup;
+
+
(* messages and notification *)
fun decorate bg en prfx =
@@ -128,30 +142,6 @@
emacs_notify ("Proof General, you can unlock the file " ^ quote (File.platform_path path));
-(* theory / proof state output *)
-
-local
-
-fun tmp_markers f =
- setmp Display.current_goals_markers (special "366", special "367", "") f ();
-
-fun print_current_goals n m st =
- tmp_markers (fn () => Display.print_current_goals_default n m st);
-
-fun print_state b st =
- tmp_markers (fn () => Toplevel.print_state_default b st);
-
-in
-
-fun setup_state () =
- (Display.print_current_goals_fn := print_current_goals;
- Toplevel.print_state_fn := print_state;
- Toplevel.prompt_state_fn :=
- (fn s => suffix (special "372") (Toplevel.prompt_state_default s)));
-
-end;
-
-
(* theory loader actions *)
local
@@ -282,7 +272,6 @@
setup_xsymbols_output ();
setup_messages ();
ProofGeneralPgip.init_pgip_channel (! Output.priority_fn);
- setup_state ();
setup_thy_loader ();
setup_present_hook ();
set initialized);
--- a/src/Pure/ProofGeneral/proof_general_pgip.ML Sat Jul 07 18:39:20 2007 +0200
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML Sat Jul 07 18:39:21 2007 +0200
@@ -28,11 +28,14 @@
open Pgip;
-(* print mode *)
+(** print mode **)
val proof_generalN = "ProofGeneral";
val pgmlsymbols_flag = ref true;
+
+(* symbol output *)
+
local
fun xsym_output "\\" = "\\\\"
@@ -52,13 +55,10 @@
let val syms = Symbol.explode str
in (implode (map pgml_sym syms), Symbol.length syms) end;
-fun pgml_markup (name, props) = ("", ""); (* FIXME *)
-
in
fun setup_proofgeneral_output () =
- (Output.add_mode proof_generalN pgml_output Symbol.encode_raw;
- Pretty.add_mode proof_generalN Pretty.default_indent pgml_markup);
+ Output.add_mode proof_generalN pgml_output Symbol.encode_raw;
end;
@@ -110,7 +110,7 @@
end;
-(** assembling and issuing PGIP packets **)
+(* assembling and issuing PGIP packets *)
val pgip_refid = ref NONE: string option ref;
val pgip_refseq = ref NONE: int option ref;
@@ -143,6 +143,9 @@
val output_xml_fn = ref Output.writeln_default
fun output_xml s = (!output_xml_fn) (XML.string_of_tree s); (* TODO: string buffer *)
+val output_pgips =
+ XML.string_of_tree o PgipOutput.output o assemble_pgips o map PgipOutput.output;
+
fun issue_pgip_rawtext str =
output_xml (PgipOutput.output (assemble_pgips [XML.Rawtext str]))
@@ -155,6 +158,7 @@
end;
+
(** messages and notification **)
local
@@ -239,44 +243,40 @@
completed=completed})
-
-(** theory / proof state output **)
+(* common markup *)
local
-fun statedisplay prts =
- let
- val display = Pretty.chunks prts
- val pgml = Pgml.Pgml
- { version=SOME PgipIsabelle.isabelle_pgml_version_supported,
- systemid=SOME PgipIsabelle.systemid,
- content = Pgml.Subterm
- { kind=SOME "statedisplay",
- param=NONE,place=NONE,name=NONE,decoration=NONE,
- action=NONE,pos=NONE,xref=NONE,
- content=[Pgml.Atoms { kind = NONE,
- content = [Pgml.Str (Pretty.output display)] }] }
+val no_text = chr 0;
+
+fun split_markup text =
+ (case space_explode no_text text of
+ [bg, en] => (bg, en)
+ | _ => (panic ("Failed to split XML markup:\n" ^ text); ("", "")));
+
+fun statedisplay_markup () =
+ let
+ val pgml = Pgml.Pgml
+ { version=SOME PgipIsabelle.isabelle_pgml_version_supported,
+ systemid=SOME PgipIsabelle.systemid,
+ content = Pgml.Subterm
+ { kind=SOME "statedisplay",
+ param=NONE,place=NONE,name=NONE,decoration=NONE,
+ action=NONE,pos=NONE,xref=NONE,
+ content=[Pgml.Atoms { kind = NONE,
+ content = [Pgml.Str no_text] }] }
(* [PgmlIsabelle.pgml_of_prettyT display] *) }
(* TODO: PGML markup for proof state navigation *)
- in
- issue_pgip (Proofstate {pgml=pgml})
- end
+ in split_markup (output_pgips [Proofstate {pgml=pgml}]) end;
-fun print_current_goals n m st =
- case (Display.pretty_current_goals n m st) of
- [] => tell_clear_goals()
- | prts => statedisplay prts
-
-fun print_state b st =
- case (Toplevel.pretty_state b st) of
- [] => tell_clear_goals()
- | prts => statedisplay prts
+fun proof_general_markup (name, props) =
+ (if name = Markup.no_stateN then (output_pgips [Cleardisplay {area=Display}], "")
+ else if name = Markup.stateN then statedisplay_markup ()
+ else ("", ""));
in
-fun setup_state () =
- (Display.print_current_goals_fn := print_current_goals;
- Toplevel.print_state_fn := print_state);
+val _ = Pretty.add_mode proof_generalN Pretty.default_indent proof_general_markup;
end;
@@ -1115,7 +1115,6 @@
setup_preferences_tweak ();
setup_proofgeneral_output ();
setup_messages ();
- setup_state ();
setup_thy_loader ();
setup_present_hook ();
init_pgip_session_id ();