src/Pure/ProofGeneral/proof_general_pgip.ML
changeset 22337 d4599c206446
parent 22249 5460a5e4caa2
child 22397 ec7ecf706955
     1.1 --- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Sat Feb 17 17:22:53 2007 +0100
     1.2 +++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Sat Feb 17 18:00:59 2007 +0100
     1.3 @@ -32,7 +32,6 @@
     1.4  
     1.5  val proof_generalN = "ProofGeneral";  (*token markup (colouring vars, etc.)*)
     1.6  val pgmlN = "PGML";                   (*XML escapes and PGML symbol elements*)
     1.7 -val pgmlatomsN = "PGMLatoms";         (*variable kind decorations*)
     1.8  val thm_depsN = "thm_deps";           (*meta-information about theorem deps*)
     1.9  
    1.10  
    1.11 @@ -55,7 +54,7 @@
    1.12      Symbol.Char s => XML.text s
    1.13    | Symbol.Sym sn => XML.element "sym" [("name", sn)] [XML.text s]
    1.14    | Symbol.Ctrl sn => XML.element "ctrl" [("name", sn)] [XML.text s] (* FIXME: no such PGML! *)
    1.15 -  | Symbol.Raw s => s);
    1.16 +  | Symbol.Raw s => Symbol.decode_raw s);
    1.17  
    1.18  fun pgml_output str =
    1.19    let val syms = Symbol.explode str
    1.20 @@ -69,7 +68,7 @@
    1.21  
    1.22  fun setup_pgml_output () =
    1.23    Output.add_mode pgmlN
    1.24 -    (pgml_output, K pgml_output, Symbol.default_indent, Symbol.encode_raw);
    1.25 +    (pgml_output, K pgml_output, Symbol.default_indent, I); (* Symbol.encode_raw); *)
    1.26  
    1.27  end;
    1.28  
    1.29 @@ -680,40 +679,46 @@
    1.30  
    1.31  
    1.32  
    1.33 -local
    1.34 -  (* accumulate printed output in a single PGIP response (inside <pgmltext>) *)
    1.35 -  fun with_displaywrap pgipfn dispfn =
    1.36 -      let
    1.37 -          val lines = ref ([]: string list);
    1.38 -          fun wlgrablines s = lines := s :: ! lines;
    1.39 -      in
    1.40 -          setmp writeln_fn wlgrablines dispfn ();
    1.41 -          issue_pgip (pgipfn (!lines))
    1.42 -      end;
    1.43 -in
    1.44  fun showid (Showid vs) =
    1.45      let
    1.46          val thyname = #thyname vs
    1.47          val objtype = #objtype vs
    1.48          val name = #name vs
    1.49 +
    1.50          val topthy = Toplevel.theory_of o Toplevel.get_state
    1.51  
    1.52 -        fun idvalue objtype name strings =
    1.53 -            Idvalue { name=name, objtype=objtype,
    1.54 -                      text=[XML.Elem("pgmltext",[],map XML.Text strings)] }
    1.55 +        (* Decompose qualified name.  FIXME: Should be a better way of doing this *)
    1.56 +	fun splitthy id =
    1.57 +	    let 
    1.58 +		val comps = scanwords (not o (curry op= ".")) (explode id)
    1.59 +	    in case comps of
    1.60 +		   (thy::(rest as _::_)) => (ThyInfo.get_theory thy, space_implode "." rest)
    1.61 +		 | [plainid] => (topthy(),plainid)
    1.62 +		 | _ => raise Toplevel.UNDEF (* assert false *)
    1.63 +	    end 
    1.64 +					    
    1.65  
    1.66 -        fun pthm thy name = map print_thm (get_thms thy (Name name))
    1.67 +        fun idvalue strings =
    1.68 +            issue_pgip (Idvalue { thyname=thyname, objtype=objtype, name=name, 
    1.69 +				  text=[XML.Elem("pgmltext",[],
    1.70 +						 map XML.Rawtext strings)] })
    1.71 +
    1.72 +	fun string_of_thm th = Pretty.string_of
    1.73 +				   (Display.pretty_thm_aux
    1.74 +					(Sign.pp (Thm.theory_of_thm th))
    1.75 +					false (* quote *)
    1.76 +					false (* show hyps *)
    1.77 +					[] (* asms *)
    1.78 +					th)
    1.79 +
    1.80 +        fun strings_of_thm (thy, name) = map string_of_thm (get_thms thy (Name name))
    1.81 +
    1.82 +	val string_of_thy = Pretty.string_of o (ProofDisplay.pretty_full_theory false)
    1.83      in
    1.84          case (thyname, objtype) of
    1.85 -            (_,ObjTheory) =>
    1.86 -            with_displaywrap (idvalue ObjTheory name)
    1.87 -                             (fn ()=>(print_theory (ThyInfo.get_theory name)))
    1.88 -          | (SOME thy, ObjTheorem) =>
    1.89 -            with_displaywrap (idvalue ObjTheorem name)
    1.90 -                             (fn ()=>(pthm (ThyInfo.get_theory thy) name))
    1.91 -          | (NONE, ObjTheorem) =>
    1.92 -            with_displaywrap (idvalue ObjTheorem name)
    1.93 -                             (fn ()=>pthm (topthy()) name)
    1.94 +            (_,ObjTheory) => idvalue [string_of_thy (ThyInfo.get_theory name)]
    1.95 +          | (SOME thy, ObjTheorem) => idvalue (strings_of_thm (ThyInfo.get_theory thy, name))
    1.96 +          | (NONE, ObjTheorem) => idvalue (strings_of_thm (splitthy name))
    1.97            | (_, ot) => error ("Cannot show objects of type "^(PgipTypes.name_of_objtype ot))
    1.98      end
    1.99  
   1.100 @@ -1018,9 +1023,6 @@
   1.101  
   1.102  val process_pgip_plain = K () o process_pgip_tree o XML.tree_of_string
   1.103  
   1.104 -end
   1.105 -
   1.106 -
   1.107  (* PGIP loop: process PGIP input only *)
   1.108  
   1.109  local
   1.110 @@ -1040,7 +1042,8 @@
   1.111             | SOME (pgip,src') =>
   1.112               let
   1.113                   val ready' = (process_pgip_tree pgip)
   1.114 -                                handle e => (handler (e,SOME src'); true)
   1.115 +                                handle PGIP_QUIT => raise PGIP_QUIT
   1.116 +				     | e => (handler (e,SOME src'); true)
   1.117               in
   1.118                   loop ready' src'
   1.119               end
   1.120 @@ -1049,14 +1052,14 @@
   1.121  and handler (e,srco) =
   1.122      case (e,srco) of
   1.123          (XML_PARSE,SOME src) =>
   1.124 -        Output.panic "Invalid XML input, aborting"
   1.125 -      | (PGIP_QUIT,_) => ()
   1.126 +        Output.panic "Invalid XML input, aborting" (* TODO: attempt recovery  *)
   1.127        | (Interrupt,SOME src) =>
   1.128          (Output.error_msg "Interrupt during PGIP processing"; loop true src)
   1.129        | (Toplevel.UNDEF,SOME src) =>
   1.130          (Output.error_msg "No working context defined"; loop true src)
   1.131        | (e,SOME src) =>
   1.132          (Output.error_msg (Toplevel.exn_message e); loop true src)
   1.133 +      | (PGIP_QUIT,_) => ()
   1.134        | (_,NONE) => ()
   1.135  in
   1.136    (* TODO: add socket interface *)
   1.137 @@ -1107,7 +1110,7 @@
   1.138            set initialized);
   1.139          sync_thy_loader ();
   1.140         change print_mode (cons proof_generalN o remove (op =) proof_generalN);
   1.141 -       change print_mode (append [pgmlN, pgmlatomsN] o subtract (op =) [pgmlN, pgmlatomsN]);
   1.142 +       change print_mode (append [pgmlN] o subtract (op =) [pgmlN]);
   1.143         pgip_toplevel tty_src);
   1.144  
   1.145