# HG changeset patch # User wenzelm # Date 1183826361 -7200 # Node ID d6f9d3acffaa66df43ca8b638cda6a5ddd06aec7 # Parent baec2e6744611d356a244923b8391dae93bb3a8e toplevel prompt/print_state: proper markup, removed hooks; diff -r baec2e674461 -r d6f9d3acffaa src/Pure/ProofGeneral/proof_general_emacs.ML --- 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); diff -r baec2e674461 -r d6f9d3acffaa src/Pure/ProofGeneral/proof_general_pgip.ML --- 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 ();