1.1 --- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Thu Aug 28 00:33:15 2008 +0200
     1.2 +++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Thu Aug 28 00:33:17 2008 +0200
     1.3 @@ -22,7 +22,7 @@
     1.4    val get_currently_open_file : unit -> Path.T option  (* interface focus *)
     1.5  end
     1.6  
     1.7 -structure ProofGeneralPgip : PROOF_GENERAL_PGIP  =
     1.8 +structure ProofGeneralPgip : PROOF_GENERAL_PGIP =
     1.9  struct
    1.10  
    1.11  open Pgip;
    1.12 @@ -34,38 +34,9 @@
    1.13  val pgmlsymbols_flag = ref true;
    1.14  
    1.15  
    1.16 -(* symbol output *)
    1.17 -
    1.18 -local
    1.19 -
    1.20 -fun xsym_output "\\" = "\\\\"
    1.21 -  | xsym_output s = if Symbol.is_raw s then Symbol.decode_raw s else s;
    1.22 -
    1.23 -fun pgml_sym s =
    1.24 -  (case Symbol.decode s of
    1.25 -    Symbol.Char s => XML.text s
    1.26 -  | Symbol.Sym sn =>
    1.27 -    let val ascii = implode (map xsym_output (Symbol.explode s))
    1.28 -    in if !pgmlsymbols_flag then XML.element "sym" [("name", sn)] [XML.text ascii]
    1.29 -       else  ascii end
    1.30 -  | Symbol.Ctrl sn => XML.element "ctrl" [("name", sn)] [XML.text sn] (* FIXME: no such PGML *)
    1.31 -  | Symbol.Raw raw => raw);
    1.32 -
    1.33 -fun pgml_output str =
    1.34 -  let val syms = Symbol.explode str
    1.35 -  in (implode (map pgml_sym syms), Symbol.length syms) end;
    1.36 -
    1.37 -in
    1.38 -
    1.39 -fun setup_proofgeneral_output () =
    1.40 -  Output.add_mode proof_generalN pgml_output Symbol.encode_raw;
    1.41 -
    1.42 -end;
    1.43 -
    1.44 -
    1.45  (* assembling and issuing PGIP packets *)
    1.46  
    1.47 -val pgip_refid  = ref NONE: string option ref;
    1.48 +val pgip_refid = ref NONE: string option ref;
    1.49  val pgip_refseq = ref NONE: int option ref;
    1.50  
    1.51  local
    1.52 @@ -78,12 +49,12 @@
    1.53    fun assemble_pgips pgips =
    1.54      Pgip { tag = SOME pgip_tag,
    1.55             class = pgip_class,
    1.56 -           seq = pgip_serial(),
    1.57 -           id = !pgip_id,
    1.58 -           destid = !pgip_refid,
    1.59 +           seq = pgip_serial (),
    1.60 +           id = ! pgip_id,
    1.61 +           destid = ! pgip_refid,
    1.62             (* destid=refid since Isabelle only communicates back to sender *)
    1.63 -           refid  = !pgip_refid,
    1.64 -           refseq = !pgip_refseq,
    1.65 +           refid = ! pgip_refid,
    1.66 +           refseq = ! pgip_refseq,
    1.67             content = pgips }
    1.68  in
    1.69  
    1.70 @@ -91,108 +62,112 @@
    1.71      pgip_id := getenv "HOSTNAME" ^ "/" ^ getenv "USER" ^ "/" ^
    1.72                 getenv "ISABELLE_PID" ^ "/" ^ Time.toString (Time.now ())
    1.73  
    1.74 -fun matching_pgip_id id = (id = !pgip_id)
    1.75 +fun matching_pgip_id id = (id = ! pgip_id)
    1.76  
    1.77  val output_xml_fn = ref Output.writeln_default
    1.78 -fun output_xml s = (!output_xml_fn) (XML.string_of s);  (* TODO: string buffer *)
    1.79 +fun output_xml s = ! output_xml_fn (XML.string_of s);
    1.80  
    1.81 -val output_pgips =
    1.82 -  XML.string_of o PgipOutput.output o assemble_pgips o map PgipOutput.output;
    1.83 +val output_pgips = XML.string_of o PgipOutput.output o assemble_pgips o map PgipOutput.output;
    1.84  
    1.85 -val output_pgmlterm =
    1.86 -  XML.string_of o Pgml.pgmlterm_to_xml;
    1.87 -
    1.88 -val output_pgmltext =
    1.89 -  XML.string_of o Pgml.pgml_to_xml;
    1.90 +val output_pgmlterm = XML.string_of o Pgml.pgmlterm_to_xml;
    1.91 +val output_pgmltext = XML.string_of o Pgml.pgml_to_xml;
    1.92  
    1.93  
    1.94  fun issue_pgip_rawtext str =
    1.95 -    output_xml (PgipOutput.output (assemble_pgips [XML.Output str]))
    1.96 -
    1.97 -fun issue_pgips pgipops =
    1.98 -    output_xml (PgipOutput.output (assemble_pgips (map PgipOutput.output pgipops)));
    1.99 +  output_xml (PgipOutput.output (assemble_pgips (YXML.parse_body str)));
   1.100  
   1.101  fun issue_pgip pgipop =
   1.102 -    output_xml (PgipOutput.output (assemble_pgips [PgipOutput.output pgipop]));
   1.103 +  output_xml (PgipOutput.output (assemble_pgips [PgipOutput.output pgipop]));
   1.104  
   1.105  end;
   1.106  
   1.107  
   1.108 -fun pgml area terms = Pgml.Pgml { version=NONE,systemid=NONE,
   1.109 -                                  area=SOME area, content=terms }
   1.110  
   1.111  (** messages and notification **)
   1.112  
   1.113 +(* PGML terms *)
   1.114 +
   1.115  local
   1.116 -    val delay_msgs = ref false   (*true: accumulate messages*)
   1.117 -    val delayed_msgs = ref []
   1.118  
   1.119 -    fun queue_or_issue pgip =
   1.120 -        if ! delay_msgs then
   1.121 -            delayed_msgs := pgip :: ! delayed_msgs
   1.122 -        else issue_pgip pgip
   1.123 +fun pgml_sym s =
   1.124 +  if ! pgmlsymbols_flag then
   1.125 +    (case Symbol.decode s of
   1.126 +      Symbol.Sym name => Pgml.Sym {name = name, content = s}
   1.127 +    | _ => Pgml.Str s)
   1.128 +  else Pgml.Str s;
   1.129  
   1.130 -    fun wrap_pgml area s =
   1.131 -        if String.isPrefix "<pgml" s then
   1.132 -            XML.Output s  (* already pgml outermost *)
   1.133 -        else
   1.134 -            Pgml.pgml_to_xml (pgml area [Pgml.Raw (XML.Output s)]) (* mixed *)
   1.135 +val pgml_syms = map pgml_sym o Symbol.explode;
   1.136 +
   1.137 +val token_markups =
   1.138 + [Markup.tclassN, Markup.tfreeN, Markup.tvarN, Markup.freeN,
   1.139 +  Markup.boundN, Markup.varN, Markup.skolemN];
   1.140  
   1.141  in
   1.142 -    fun normalmsg area s =
   1.143 -        let
   1.144 -            val content = wrap_pgml area s
   1.145 -            val pgip = Normalresponse { content=[content] }
   1.146 -        in
   1.147 -            queue_or_issue pgip
   1.148 +
   1.149 +fun pgml_terms (XML.Elem (name, atts, body)) =
   1.150 +      if member (op =) token_markups name then
   1.151 +        let val content = pgml_syms (Buffer.content (fold XML.add_content body Buffer.empty))
   1.152 +        in [Pgml.Atoms {kind = SOME name, content = content}] end
   1.153 +      else
   1.154 +        let val content = maps pgml_terms body in
   1.155 +          if name = Markup.blockN then
   1.156 +            [Pgml.Box {orient = NONE, indent = Properties.get_int atts Markup.indentN, content = content}]
   1.157 +          else if name = Markup.breakN then
   1.158 +            [Pgml.Break {mandatory = NONE, indent = Properties.get_int atts Markup.widthN}]
   1.159 +          else if name = Markup.fbreakN then
   1.160 +            [Pgml.Break {mandatory = SOME true, indent = NONE}]
   1.161 +          else content
   1.162          end
   1.163 +  | pgml_terms (XML.Text text) = map (Pgml.Raw o Pgml.atom_to_xml) (pgml_syms text);
   1.164  
   1.165 -    fun errormsg area fatality s =
   1.166 -        let
   1.167 -            val content = wrap_pgml area s
   1.168 -            val pgip = Errorresponse { fatality=fatality,
   1.169 -                                       location=NONE,
   1.170 -                                       content=[content] }
   1.171 -        in
   1.172 -            queue_or_issue pgip
   1.173 -        end
   1.174 -
   1.175 -    (* Error responses with useful locations *)
   1.176 -    fun error_with_pos area fatality pos s =
   1.177 -        let
   1.178 -              val content = wrap_pgml area s
   1.179 -              val pgip = Errorresponse { fatality=fatality,
   1.180 -                                         location=SOME (PgipIsabelle.location_of_position pos),
   1.181 -                                         content=[content] }
   1.182 -        in
   1.183 -            queue_or_issue pgip
   1.184 -        end
   1.185 -
   1.186 -    fun start_delay_msgs () = (set delay_msgs; delayed_msgs := [])
   1.187 -    fun end_delayed_msgs () = (reset delay_msgs; ! delayed_msgs)
   1.188  end;
   1.189  
   1.190 -(* NB: all of the standard error/message functions now expect already-escaped text.
   1.191 -   FIXME: this may cause us problems now we're generating trees; on the other
   1.192 -   hand the output functions were tuned some time ago, so it ought to be
   1.193 -   enough to use XML.Output always above. *)
   1.194 -(* NB 2: all of standard functions print strings terminated with new lines, but we don't
   1.195 +
   1.196 +(* messages *)
   1.197 +
   1.198 +fun pgml area content =
   1.199 +  Pgml.Pgml {version = NONE, systemid = NONE, area = SOME area, content = content};
   1.200 +
   1.201 +fun message_content default_area s =
   1.202 +  let
   1.203 +    val body = YXML.parse_body s;
   1.204 +    val area =
   1.205 +      (case body of
   1.206 +        [XML.Elem (name, _, _)] =>
   1.207 +          if name = Markup.stateN then PgipTypes.Display else default_area
   1.208 +      | _ => default_area);
   1.209 +  in Pgml.pgml_to_xml (pgml area (maps pgml_terms body)) end;
   1.210 +
   1.211 +
   1.212 +fun normalmsg area s = issue_pgip
   1.213 +  (Normalresponse {content = [message_content area s]});
   1.214 +
   1.215 +fun errormsg area fatality s = issue_pgip
   1.216 +  (Errorresponse {fatality = fatality, location = NONE, content = [message_content area s]});
   1.217 +
   1.218 +(*error responses with useful locations*)
   1.219 +fun error_with_pos area fatality pos s = issue_pgip
   1.220 +  (Errorresponse {
   1.221 +    fatality = fatality,
   1.222 +    location = SOME (PgipIsabelle.location_of_position pos),
   1.223 +    content = [message_content area s]});
   1.224 +
   1.225 +fun panic s = (errormsg Message Panic ("## SYSTEM EXIT ##\n" ^ s); exit 1);
   1.226 +fun nonfatal_error s = errormsg Message Nonfatal s;
   1.227 +fun log_msg s = errormsg Message Log s;
   1.228 +
   1.229 +(* NB: all of standard functions print strings terminated with new lines, but we don't
   1.230     add new lines explicitly in PGIP: they are left implicit.  It means that PGIP messages
   1.231     can't be written without newlines. *)
   1.232 -
   1.233  fun setup_messages () =
   1.234   (Output.writeln_fn := (fn s => normalmsg Message s);
   1.235    Output.status_fn := (fn _ => ());
   1.236    Output.priority_fn := (fn s => normalmsg Status s);
   1.237 -  Output.tracing_fn := (fn s => normalmsg  Tracing s);
   1.238 +  Output.tracing_fn := (fn s => normalmsg Tracing s);
   1.239    Output.warning_fn := (fn s => errormsg Message Warning s);
   1.240    Output.error_fn := (fn s => errormsg Message Fatal s);
   1.241    Output.debug_fn := (fn s => errormsg Message Debug s));
   1.242  
   1.243 -fun panic s = (errormsg Message Panic ("## SYSTEM EXIT ##\n" ^ s); exit 1);
   1.244 -fun nonfatal_error s = errormsg Message Nonfatal s;
   1.245 -fun log_msg s = errormsg Message Log s;
   1.246 -
   1.247  
   1.248  (* immediate messages *)
   1.249  
   1.250 @@ -212,58 +187,6 @@
   1.251                                       completed=completed})
   1.252  
   1.253  
   1.254 -(* common markup *)
   1.255 -
   1.256 -local
   1.257 -
   1.258 -val no_text = chr 0;
   1.259 -
   1.260 -val pgmlterms_no_text= [Pgml.Raw (XML.Output no_text)]
   1.261 -
   1.262 -fun split_markup text =
   1.263 -  (case space_explode no_text text of
   1.264 -    [bg, en] => (bg, en)
   1.265 -  | _ => (error ("Internal error: failed to split XML markup:\n" ^ text); ("", "")));
   1.266 -
   1.267 -
   1.268 -fun block_markup markup =
   1.269 -    let
   1.270 -      val pgml = Pgml.Box { orient = NONE,
   1.271 -                            indent = Markup.get_int markup Markup.indentN,
   1.272 -                            content = pgmlterms_no_text }
   1.273 -    in split_markup (output_pgmlterm pgml) end;
   1.274 -
   1.275 -fun break_markup markup =
   1.276 -    let
   1.277 -      val pgml = Pgml.Break { mandatory = NONE,
   1.278 -                              indent = Markup.get_int markup Markup.widthN }
   1.279 -    in (output_pgmlterm pgml, "") end;
   1.280 -
   1.281 -fun fbreak_markup markup =
   1.282 -    let
   1.283 -      val pgml = Pgml.Break { mandatory = SOME true, indent = NONE }
   1.284 -    in (output_pgmlterm pgml, "") end;
   1.285 -
   1.286 -val state_markup =
   1.287 -    split_markup (output_pgmltext (pgml PgipTypes.Display pgmlterms_no_text))
   1.288 -
   1.289 -val token_markups =
   1.290 - [Markup.tclassN, Markup.tfreeN, Markup.tvarN, Markup.freeN,
   1.291 -  Markup.boundN, Markup.varN, Markup.skolemN];
   1.292 -
   1.293 -in
   1.294 -
   1.295 -val _ = Markup.add_mode proof_generalN (fn (markup as (name, _)) =>
   1.296 -   if name = Markup.blockN then block_markup markup
   1.297 -   else if name = Markup.breakN then break_markup markup
   1.298 -   else if name = Markup.fbreakN then fbreak_markup markup
   1.299 -   else if name = Markup.stateN then state_markup
   1.300 -   else if member (op =) token_markups name then XML.output_markup ("atom", [("kind", name)])
   1.301 -   else ("", ""));
   1.302 -
   1.303 -end;
   1.304 -
   1.305 -
   1.306  (* theory loader actions *)
   1.307  
   1.308  local
   1.309 @@ -698,24 +621,22 @@
   1.310          fun idvalue strings =
   1.311              issue_pgip (Idvalue { thyname=thyname, objtype=objtype, name=name,
   1.312                                    text=[XML.Elem("pgml",[],
   1.313 -                                                 map XML.Output strings)] })
   1.314 +                                                 maps YXML.parse_body strings)] })
   1.315  
   1.316 -        fun string_of_thm th = Output.output
   1.317 -                               (Pretty.string_of
   1.318 +        fun string_of_thm th = Pretty.string_of
   1.319                                     (Display.pretty_thm_aux
   1.320                                          (Syntax.pp_global (Thm.theory_of_thm th))
   1.321                                          false (* quote *)
   1.322                                          false (* show hyps *)
   1.323                                          [] (* asms *)
   1.324 -                                        th))
   1.325 +                                        th)
   1.326  
   1.327          fun strings_of_thm (thy, name) = map string_of_thm (PureThy.get_thms thy name)
   1.328  
   1.329 -        val string_of_thy = Output.output o
   1.330 -                                Pretty.string_of o (ProofDisplay.pretty_full_theory false)
   1.331 +        val string_of_thy = Pretty.string_of o ProofDisplay.pretty_full_theory false
   1.332      in
   1.333          case (thyname, objtype) of
   1.334 -            (_,ObjTheory) => idvalue [string_of_thy (ThyInfo.get_theory name)]
   1.335 +            (_, ObjTheory) => idvalue [string_of_thy (ThyInfo.get_theory name)]
   1.336            | (SOME thy, ObjTheorem) => idvalue (strings_of_thm (ThyInfo.get_theory thy, name))
   1.337            | (NONE, ObjTheorem) => idvalue (strings_of_thm (splitthy name))
   1.338            | (_, ot) => error ("Cannot show objects of type "^(PgipTypes.name_of_objtype ot))
   1.339 @@ -762,16 +683,14 @@
   1.340          val systemdata = #systemdata vs
   1.341          val location = #location vs   (* TODO: extract position *)
   1.342  
   1.343 -        val _ = start_delay_msgs ()   (* gather parsing errs/warns *)
   1.344          val doc = PgipParser.pgip_parser Position.none text
   1.345 -        val errs = end_delayed_msgs ()
   1.346  
   1.347          val sysattrs = PgipTypes.opt_attr "systemdata" systemdata
   1.348          val locattrs = PgipTypes.attrs_of_location location
   1.349       in
   1.350          issue_pgip (Parseresult { attrs= sysattrs@locattrs,
   1.351                                    doc = doc,
   1.352 -                                  errs = map PgipOutput.output errs })
   1.353 +                                  errs = [] })
   1.354      end
   1.355  
   1.356  fun showproofstate _ = isarcmd "pr"
   1.357 @@ -979,7 +898,6 @@
   1.358                                (XML.string_of xml))
   1.359             | SOME inp => (process_input inp)) (* errors later; packet discarded *)
   1.360        | XML.Text t => ignored_text_warning t
   1.361 -      | XML.Output t => ignored_text_warning t
   1.362  and ignored_text_warning t =
   1.363      if size (Symbol.strip_blanks t) > 0 then
   1.364             warning ("Ignored text in PGIP packet: \n" ^ t)
   1.365 @@ -1084,7 +1002,8 @@
   1.366    | init_pgip true =
   1.367        (! initialized orelse
   1.368          (setup_preferences_tweak ();
   1.369 -         setup_proofgeneral_output ();
   1.370 +         Output.add_mode proof_generalN Output.default_output Output.default_escape;
   1.371 +         Markup.add_mode proof_generalN YXML.output_markup;
   1.372           setup_messages ();
   1.373           Output.no_warnings init_outer_syntax ();
   1.374           setup_thy_loader ();
   1.375 @@ -1093,7 +1012,7 @@
   1.376           welcome ();
   1.377           set initialized);
   1.378          sync_thy_loader ();
   1.379 -       change print_mode (cons proof_generalN o remove (op =) proof_generalN);
   1.380 +       change print_mode (update (op =) proof_generalN);
   1.381         pgip_toplevel tty_src);
   1.382  
   1.383