added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
authorwenzelm
Thu Sep 01 15:58:08 2005 +0200 (2005-09-01)
changeset 17217954c0f265203
parent 17216 df66d8feec63
child 17218 64242b791c19
added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
tuned;
src/Pure/proof_general.ML
     1.1 --- a/src/Pure/proof_general.ML	Thu Sep 01 11:45:54 2005 +0200
     1.2 +++ b/src/Pure/proof_general.ML	Thu Sep 01 15:58:08 2005 +0200
     1.3 @@ -63,6 +63,7 @@
     1.4  (* print modes *)
     1.5  
     1.6  val proof_generalN = "ProofGeneral";  (*token markup (colouring vars, etc.)*)
     1.7 +val pgasciiN = "PGASCII";             (*plain 7-bit ASCII communication*)
     1.8  val xsymbolsN = Symbol.xsymbolsN;     (*X-Symbol symbols*)
     1.9  val pgmlN = "PGML";                   (*XML escapes and PGML symbol elements*)
    1.10  val pgmlatomsN = "PGMLatoms";         (*variable kind decorations*)
    1.11 @@ -70,6 +71,10 @@
    1.12  
    1.13  fun pgml () = Output.has_mode pgmlN;
    1.14  
    1.15 +fun special oct =
    1.16 +  if Output.has_mode pgasciiN then chr 1 ^ chr (ord (oct_char oct) - 167)
    1.17 +  else oct_char oct;
    1.18 +
    1.19  
    1.20  (* text output: print modes for xsymbol and PGML *)
    1.21  
    1.22 @@ -114,20 +119,20 @@
    1.23  
    1.24  local
    1.25  
    1.26 -val end_tag = oct_char "350";
    1.27 -val class_tag = ("class", oct_char "351");
    1.28 -val tfree_tag = ("tfree", oct_char "352");
    1.29 -val tvar_tag = ("tvar", oct_char "353");
    1.30 -val free_tag = ("free", oct_char "354");
    1.31 -val bound_tag = ("bound", oct_char "355");
    1.32 -val var_tag = ("var", oct_char "356");
    1.33 -val skolem_tag = ("skolem", oct_char "357");
    1.34 +fun end_tag () = special "350";
    1.35 +val class_tag = ("class", fn () => special "351");
    1.36 +val tfree_tag = ("tfree", fn () => special "352");
    1.37 +val tvar_tag = ("tvar", fn () => special "353");
    1.38 +val free_tag = ("free", fn () => special "354");
    1.39 +val bound_tag = ("bound", fn () => special "355");
    1.40 +val var_tag = ("var", fn () => special "356");
    1.41 +val skolem_tag = ("skolem", fn () => special "357");
    1.42  
    1.43  fun xml_atom kind x = XML.element "atom" [("kind", kind)] [XML.text x];
    1.44  
    1.45  fun tagit (kind, bg_tag) x =
    1.46   (if Output.has_mode pgmlatomsN then xml_atom kind x
    1.47 -  else bg_tag ^ x ^ end_tag, real (Symbol.length (Symbol.explode x)));
    1.48 +  else bg_tag () ^ x ^ end_tag (), real (Symbol.length (Symbol.explode x)));
    1.49  
    1.50  fun free_or_skolem x =
    1.51    (case try Syntax.dest_skolem x of
    1.52 @@ -161,7 +166,7 @@
    1.53  
    1.54  (* assembling PGIP packets *)
    1.55  
    1.56 -val pgip_refid  = ref NONE: string option ref;  
    1.57 +val pgip_refid  = ref NONE: string option ref;
    1.58  val pgip_refseq = ref NONE: string option ref;
    1.59  
    1.60  local
    1.61 @@ -176,7 +181,7 @@
    1.62        "pgip"
    1.63        ([("tag",    pgip_tag),
    1.64          ("class",  pgip_class),
    1.65 -	("seq",    string_of_int (pgip_serial())),
    1.66 +        ("seq",    string_of_int (pgip_serial())),
    1.67          ("id",     !pgip_id)] @
    1.68         if_none (Option.map (single o (pair "destid")) (! pgip_refid)) [] @
    1.69         (* destid=refid since Isabelle only communicates back to sender,
    1.70 @@ -188,10 +193,10 @@
    1.71  
    1.72  in
    1.73  
    1.74 -fun init_pgip_session_id () = 
    1.75 +fun init_pgip_session_id () =
    1.76      pgip_id := getenv "HOSTNAME" ^ "/" ^ getenv "USER" ^ "/" ^
    1.77                 getenv "ISABELLE_PID" ^ "/" ^ Time.toString (Time.now ())
    1.78 -						       
    1.79 +
    1.80  
    1.81  fun matching_pgip_id id = (id = !pgip_id)
    1.82  
    1.83 @@ -203,7 +208,7 @@
    1.84  fun issue_pgips ps =
    1.85    if pgip_emacs_compatibility() then
    1.86      decorated_output (*add urgent message annotation*)
    1.87 -      (oct_char "360") (oct_char "361") ""
    1.88 +      (special "360") (special "361") ""
    1.89        (assemble_pgips ps)
    1.90    else
    1.91      writeln_default (assemble_pgips ps);
    1.92 @@ -215,7 +220,7 @@
    1.93  fun issue_pgip resp attrs txt =
    1.94    if pgip_emacs_compatibility () then
    1.95      decorated_output (*add urgent message annotation*)
    1.96 -      (oct_char "360") (oct_char "361") ""
    1.97 +      (special "360") (special "361") ""
    1.98        (assemble_pgip resp attrs txt)
    1.99    else
   1.100      writeln_default (assemble_pgip resp attrs txt);
   1.101 @@ -274,28 +279,21 @@
   1.102  in
   1.103  
   1.104  fun setup_messages () =
   1.105 - (writeln_fn  := message "normalresponse" [message_area] "" "" "";
   1.106 -
   1.107 -  priority_fn := message "normalresponse" [message_area, urgent_indication]
   1.108 -                         (oct_char "360") (oct_char "361") "";
   1.109 -
   1.110 -  tracing_fn := message "normalresponse"  [message_area, tracing_category]
   1.111 -                        (oct_char "360" ^ oct_char "375") (oct_char "361") "";
   1.112 -
   1.113 -  info_fn := message "normalresponse" [message_area, info_category]
   1.114 -                     (oct_char "362") (oct_char "363") "+++ ";
   1.115 -
   1.116 -  debug_fn := message "normalresponse" [message_area, internal_category]
   1.117 -                      (oct_char "362") (oct_char "363") "+++ ";
   1.118 -
   1.119 -  warning_fn := message "errorresponse" [nonfatal]
   1.120 -                        (oct_char "362") (oct_char "363") "### ";
   1.121 -
   1.122 -  error_fn := message "errorresponse" [fatal]
   1.123 -                      (oct_char "364") (oct_char "365") "*** ";
   1.124 -
   1.125 -  panic_fn := message "errorresponse" [panic]
   1.126 -                      (oct_char "364") (oct_char "365") "!!! ");
   1.127 + (writeln_fn := (fn s => message "normalresponse" [message_area] "" "" "" s);
   1.128 +  priority_fn := (fn s => message "normalresponse" [message_area, urgent_indication]
   1.129 +    (special "360") (special "361") "" s);
   1.130 +  tracing_fn := (fn s => message "normalresponse"  [message_area, tracing_category]
   1.131 +    (special "360" ^ special "375") (special "361") "" s);
   1.132 +  info_fn := (fn s => message "normalresponse" [message_area, info_category]
   1.133 +    (special "362") (special "363") "+++ " s);
   1.134 +  debug_fn := (fn s => message "normalresponse" [message_area, internal_category]
   1.135 +    (special "362") (special "363") "+++ " s);
   1.136 +  warning_fn := (fn s => message "errorresponse" [nonfatal]
   1.137 +    (special "362") (special "363") "### " s);
   1.138 +  error_fn := (fn s => message "errorresponse" [fatal]
   1.139 +    (special "364") (special "365") "*** " s);
   1.140 +  panic_fn := (fn s => message "errorresponse" [panic]
   1.141 +    (special "364") (special "365") "!!! " s));
   1.142  
   1.143  
   1.144  (* accumulate printed output in a single PGIP response (inside <pgmltext>) *)
   1.145 @@ -310,7 +308,7 @@
   1.146      issue_pgip elt attrs (XML.element "pgmltext" [] (! lines))
   1.147    end;
   1.148  
   1.149 -val emacs_notify = decorated_output (oct_char "360") (oct_char "361") "";
   1.150 +fun emacs_notify s = decorated_output (special "360") (special "361") "" s;
   1.151  
   1.152  fun tell_clear_goals () =
   1.153    if pgip () then
   1.154 @@ -344,13 +342,13 @@
   1.155  local
   1.156  
   1.157  fun tmp_markers f =
   1.158 -  setmp Display.current_goals_markers (oct_char "366", oct_char "367", "") f ();
   1.159 +  setmp Display.current_goals_markers (special "366", special "367", "") f ();
   1.160  
   1.161  fun statedisplay prts =
   1.162    issue_pgip "proofstate" []
   1.163      (XML.element "pgml" []
   1.164        [XML.element "statedisplay" [] [Pretty.output (Pretty.chunks prts)]]);
   1.165 -     
   1.166 +
   1.167  fun print_current_goals n m st =
   1.168    if pgml () then statedisplay (Display.pretty_current_goals n m st)
   1.169    else tmp_markers (fn () => Display.print_current_goals_default n m st);
   1.170 @@ -365,7 +363,8 @@
   1.171    (Display.print_current_goals_fn := print_current_goals;
   1.172     Toplevel.print_state_fn := print_state;
   1.173     (* FIXME: check next octal char won't appear in pgip? *)
   1.174 -   Toplevel.prompt_state_fn := (suffix (oct_char "372") o Toplevel.prompt_state_default));
   1.175 +   Toplevel.prompt_state_fn := (fn s => suffix (special "372")
   1.176 +     (Toplevel.prompt_state_default s)));
   1.177  
   1.178  end;
   1.179  
   1.180 @@ -541,8 +540,8 @@
   1.181  
   1.182  val thm_deps_option = (pgipbool,
   1.183    with_default (fn () => Bool.toString (Output.has_mode thm_depsN)),
   1.184 -  (fn "false" => print_mode := (! print_mode \ thm_depsN)
   1.185 -    | "true" => print_mode := (thm_depsN ins ! print_mode)
   1.186 +  (fn "false" => change print_mode (remove (op =) thm_depsN)
   1.187 +    | "true" => change print_mode (insert (op =) thm_depsN)
   1.188      | x => error ("thm_deps_option: illegal value: " ^ x)));
   1.189  
   1.190  local
   1.191 @@ -910,21 +909,21 @@
   1.192              (empty "openblock")
   1.193          end
   1.194  
   1.195 -    fun xmls_of_qed (name,markup) = 
   1.196 -	let val qedmarkup  = 
   1.197 -		(case name of
   1.198 -		     "sorry" => markup "postponegoal"
   1.199 -		   | "oops"  => markup "giveupgoal"
   1.200 -		   | "done"  => markup "closegoal" 
   1.201 -		   | "by"    => markup "closegoal"  (* nested or toplevel *)
   1.202 -		   | "qed"   => markup "closegoal"  (* nested or toplevel *)
   1.203 -		   | "."     => markup "closegoal"  (* nested or toplevel *)
   1.204 -		   | ".."    => markup "closegoal"  (* nested or toplevel *)
   1.205 -		   | other => (* default to closegoal: may be wrong for extns *)
   1.206 -				  (parse_warning 
   1.207 -				       ("Unrecognized qed command: " ^ quote other); 
   1.208 -				       markup "closegoal"))
   1.209 -	in qedmarkup @ (empty "closeblock") end
   1.210 +    fun xmls_of_qed (name,markup) =
   1.211 +        let val qedmarkup  =
   1.212 +                (case name of
   1.213 +                     "sorry" => markup "postponegoal"
   1.214 +                   | "oops"  => markup "giveupgoal"
   1.215 +                   | "done"  => markup "closegoal"
   1.216 +                   | "by"    => markup "closegoal"  (* nested or toplevel *)
   1.217 +                   | "qed"   => markup "closegoal"  (* nested or toplevel *)
   1.218 +                   | "."     => markup "closegoal"  (* nested or toplevel *)
   1.219 +                   | ".."    => markup "closegoal"  (* nested or toplevel *)
   1.220 +                   | other => (* default to closegoal: may be wrong for extns *)
   1.221 +                                  (parse_warning
   1.222 +                                       ("Unrecognized qed command: " ^ quote other);
   1.223 +                                       markup "closegoal"))
   1.224 +        in qedmarkup @ (empty "closeblock") end
   1.225  
   1.226      fun xmls_of_kind kind (name,toks,str) =
   1.227      let val markup = markup_text str in
   1.228 @@ -1080,7 +1079,7 @@
   1.229  (* TODO: would be cleaner to define a datatype here for the accepted elements,
   1.230     and mapping functions to/from strings.  At the moment this list must
   1.231     coincide with the strings in the function process_pgip_element. *)
   1.232 -val isabelle_acceptedpgipelems = 
   1.233 +val isabelle_acceptedpgipelems =
   1.234      ["askpgip","askpgml","askprefs","getpref","setpref",
   1.235       "proverinit","proverexit","startquiet","stopquiet",
   1.236       "pgmlsymbolson", "pgmlsymbolsoff",
   1.237 @@ -1093,14 +1092,14 @@
   1.238       "abortfile", "changecwd", "systemcmd"];
   1.239  
   1.240  fun usespgip () =
   1.241 -    issue_pgip 
   1.242 -	"usespgip" 
   1.243 -	[("version", isabelle_pgip_version_supported)]
   1.244 -	(XML.element "acceptedpgipelems" []
   1.245 -		     (map (fn s=>XML.element "pgipelem" 
   1.246 -					     [] (* if threads: possibility to add async here *)
   1.247 -					     [s])
   1.248 -			  isabelle_acceptedpgipelems))
   1.249 +    issue_pgip
   1.250 +        "usespgip"
   1.251 +        [("version", isabelle_pgip_version_supported)]
   1.252 +        (XML.element "acceptedpgipelems" []
   1.253 +                     (map (fn s=>XML.element "pgipelem"
   1.254 +                                             [] (* if threads: possibility to add async here *)
   1.255 +                                             [s])
   1.256 +                          isabelle_acceptedpgipelems))
   1.257  
   1.258  fun usespgml () =
   1.259      issue_pgipe "usespgml" [("version", isabelle_pgml_version_supported)]
   1.260 @@ -1197,15 +1196,15 @@
   1.261       file we remove the path.  Leaving it there can cause confusion
   1.262       with difference in batch mode.a  NB: PGIP does not assume
   1.263       that the prover has a load path. *)
   1.264 -  local 
   1.265 +  local
   1.266        val current_working_dir = ref (NONE : string option)
   1.267    in
   1.268 -      fun changecwd dir = 
   1.269 -	  (case (!current_working_dir) of
   1.270 -	       NONE => ()
   1.271 +      fun changecwd dir =
   1.272 +          (case (!current_working_dir) of
   1.273 +               NONE => ()
   1.274               | SOME dir => ThyLoad.del_path dir;
   1.275 -	   ThyLoad.add_path dir;
   1.276 -	   current_working_dir := SOME dir)
   1.277 +           ThyLoad.add_path dir;
   1.278 +           current_working_dir := SOME dir)
   1.279    end
   1.280  
   1.281    val topnode = Toplevel.node_of o Toplevel.get_state
   1.282 @@ -1230,8 +1229,8 @@
   1.283       | "proverexit"     => isarcmd "quit"
   1.284       | "startquiet"     => isarcmd "disable_pr"
   1.285       | "stopquiet"      => isarcmd "enable_pr"
   1.286 -     | "pgmlsymbolson"   => (print_mode := !print_mode @ ["xsymbols"])
   1.287 -     | "pgmlsymbolsoff"  => (print_mode := (!print_mode \ "xsymbols"))
   1.288 +     | "pgmlsymbolson"   => change print_mode (insert (op =) Symbol.xsymbolsN)
   1.289 +     | "pgmlsymbolsoff"  => change print_mode (remove (op =) Symbol.xsymbolsN)
   1.290       (* properproofcmd: proper commands which belong in script *)
   1.291       (* FIXME: next ten are by Eclipse interface, can be removed in favour of dostep *)
   1.292       (* NB: Isar doesn't make lemma name of goal accessible during proof *)
   1.293 @@ -1261,9 +1260,9 @@
   1.294       | "parsescript"    => parsescript (xmltext data) attrs (* just pass back attrs unchanged *)
   1.295       | "showproofstate" => isarcmd "pr"
   1.296       | "showctxt"       => isarcmd "print_theory"   (* more useful than print_context *)
   1.297 -     | "searchtheorems" => isarcmd ("thms_containing " ^ (xmltext data))
   1.298 -     | "setlinewidth"   => isarcmd ("pretty_setmargin " ^ (xmltext data))
   1.299 -     | "viewdoc"        => isarcmd ("print_" ^ (xmltext data)) (* FIXME: isatool doc? *)
   1.300 +     | "searchtheorems" => isarcmd ("thms_containing " ^ xmltext data)
   1.301 +     | "setlinewidth"   => isarcmd ("pretty_setmargin " ^ xmltext data)
   1.302 +     | "viewdoc"        => isarcmd ("print_" ^ xmltext data) (* FIXME: isatool doc? *)
   1.303       (* properfilecmd: proper theory-level script commands *)
   1.304       (* FIXME: next three are sent by Eclipse, can be removed in favour of doitem *)
   1.305       | "opentheory"     => isarscript data
   1.306 @@ -1271,14 +1270,14 @@
   1.307       | "closetheory"    => let
   1.308                                val thyname = topthy_name()
   1.309                             in (isarscript data;
   1.310 -                               writeln ("Theory \""^thyname^"\" completed."))
   1.311 +                               writeln ("Theory " ^ quote thyname ^ " completed."))
   1.312                             end
   1.313       (* improperfilecmd: theory-level commands not in script *)
   1.314       | "doitem"         => isarscript data
   1.315       | "undoitem"       => isarcmd "ProofGeneral.undo"
   1.316       | "redoitem"       => isarcmd "ProofGeneral.redo"
   1.317       | "aborttheory"    => isarcmd ("init_toplevel")
   1.318 -     | "retracttheory"  => isarcmd ("kill_thy " ^ (quote (thyname_attr attrs)))
   1.319 +     | "retracttheory"  => isarcmd ("kill_thy " ^ quote (thyname_attr attrs))
   1.320       | "loadfile"       => use_thy_or_ml_file (fileurl_of attrs)
   1.321       | "openfile"       => (openfile_retract (fileurl_of attrs);
   1.322                              currently_open_file := SOME (fileurl_of attrs))
   1.323 @@ -1300,19 +1299,19 @@
   1.324            XML.Elem ("pgip", attrs, pgips) =>
   1.325            (let
   1.326                 val class = xmlattr "class" attrs
   1.327 -	       val dest  = xmlattro "destid" attrs
   1.328 +               val dest  = xmlattro "destid" attrs
   1.329                 val _ = (pgip_refid :=  xmlattro "id" attrs;
   1.330 -			pgip_refseq := xmlattro "seq" attrs)
   1.331 +                        pgip_refseq := xmlattro "seq" attrs)
   1.332             in
   1.333 -	       (* We respond to broadcast messages to provers, or 
   1.334 +               (* We respond to broadcast messages to provers, or
   1.335                    messages intended uniquely for us.  Silently ignore rest. *)
   1.336                 case dest of
   1.337 -		   NONE => if (class = "pa") then
   1.338 -			       (List.app process_pgip_element pgips; true)
   1.339 -			   else false
   1.340 -		 | SOME id => if (matching_pgip_id id) then
   1.341 -				  (List.app process_pgip_element pgips; true)
   1.342 -			      else false
   1.343 +                   NONE => if (class = "pa") then
   1.344 +                               (List.app process_pgip_element pgips; true)
   1.345 +                           else false
   1.346 +                 | SOME id => if (matching_pgip_id id) then
   1.347 +                                  (List.app process_pgip_element pgips; true)
   1.348 +                              else false
   1.349             end)
   1.350          | _ => raise PGIP "Invalid PGIP packet received")
   1.351       handle (PGIP msg) =>
   1.352 @@ -1339,11 +1338,11 @@
   1.353          case pgipo of
   1.354               NONE  => ()
   1.355             | SOME (pgip,src') =>
   1.356 -	     let 
   1.357 -		 val ready' = (process_pgip_tree pgip) handle e => (handler (e,SOME src'); true)
   1.358 -	     in 
   1.359 -		 loop ready' src'
   1.360 -	     end 
   1.361 +             let
   1.362 +                 val ready' = (process_pgip_tree pgip) handle e => (handler (e,SOME src'); true)
   1.363 +             in
   1.364 +                 loop ready' src'
   1.365 +             end
   1.366      end handle e => handler (e,SOME src)  (* i.e. error in ready/XML parse *)
   1.367  
   1.368  and handler (e,srco) =
   1.369 @@ -1426,7 +1425,7 @@
   1.370  
   1.371  fun set_prompts true _ = ml_prompts "ML> " "ML# "
   1.372    | set_prompts false true = ml_prompts "PGIP-ML>" "PGIP-ML# "
   1.373 -  | set_prompts false false = ml_prompts ("> " ^ oct_char "372") ("- " ^ oct_char "373");
   1.374 +  | set_prompts false false = ml_prompts ("> " ^ special "372") ("- " ^ special "373");
   1.375  
   1.376  fun init_setup isar pgip =
   1.377    (conditional (not (! initialized)) (fn () =>
   1.378 @@ -1439,10 +1438,10 @@
   1.379      setup_present_hook ();
   1.380      set initialized; ()));
   1.381    sync_thy_loader ();
   1.382 -  print_mode := proof_generalN :: (! print_mode \ proof_generalN);
   1.383 +  change print_mode (cons proof_generalN o remove (op =) proof_generalN);
   1.384    if pgip then
   1.385        (init_pgip_session_id();
   1.386 -       print_mode := pgmlN :: (pgmlatomsN :: (! print_mode \ pgmlN \ pgmlatomsN)))
   1.387 +       change print_mode (append [pgmlN, pgmlatomsN] o fold (remove (op =)) [pgmlN, pgmlatomsN]))
   1.388    else
   1.389      pgip_emacs_compatibility_flag := true;  (* assume this for PG <3.6 compatibility *)
   1.390    set quick_and_dirty;