# HG changeset patch # User wenzelm # Date 1125583088 -7200 # Node ID 954c0f26520322acdf48bb46d66a34845a979956 # Parent df66d8feec63b2e4e4d445eaa857dad9efca2612 added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z; tuned; diff -r df66d8feec63 -r 954c0f265203 src/Pure/proof_general.ML --- a/src/Pure/proof_general.ML Thu Sep 01 11:45:54 2005 +0200 +++ b/src/Pure/proof_general.ML Thu Sep 01 15:58:08 2005 +0200 @@ -63,6 +63,7 @@ (* print modes *) val proof_generalN = "ProofGeneral"; (*token markup (colouring vars, etc.)*) +val pgasciiN = "PGASCII"; (*plain 7-bit ASCII communication*) val xsymbolsN = Symbol.xsymbolsN; (*X-Symbol symbols*) val pgmlN = "PGML"; (*XML escapes and PGML symbol elements*) val pgmlatomsN = "PGMLatoms"; (*variable kind decorations*) @@ -70,6 +71,10 @@ fun pgml () = Output.has_mode pgmlN; +fun special oct = + if Output.has_mode pgasciiN then chr 1 ^ chr (ord (oct_char oct) - 167) + else oct_char oct; + (* text output: print modes for xsymbol and PGML *) @@ -114,20 +119,20 @@ local -val end_tag = oct_char "350"; -val class_tag = ("class", oct_char "351"); -val tfree_tag = ("tfree", oct_char "352"); -val tvar_tag = ("tvar", oct_char "353"); -val free_tag = ("free", oct_char "354"); -val bound_tag = ("bound", oct_char "355"); -val var_tag = ("var", oct_char "356"); -val skolem_tag = ("skolem", oct_char "357"); +fun end_tag () = special "350"; +val class_tag = ("class", fn () => special "351"); +val tfree_tag = ("tfree", fn () => special "352"); +val tvar_tag = ("tvar", fn () => special "353"); +val free_tag = ("free", fn () => special "354"); +val bound_tag = ("bound", fn () => special "355"); +val var_tag = ("var", fn () => special "356"); +val skolem_tag = ("skolem", fn () => special "357"); fun xml_atom kind x = XML.element "atom" [("kind", kind)] [XML.text x]; fun tagit (kind, bg_tag) x = (if Output.has_mode pgmlatomsN then xml_atom kind x - else bg_tag ^ x ^ end_tag, real (Symbol.length (Symbol.explode x))); + else bg_tag () ^ x ^ end_tag (), real (Symbol.length (Symbol.explode x))); fun free_or_skolem x = (case try Syntax.dest_skolem x of @@ -161,7 +166,7 @@ (* assembling PGIP packets *) -val pgip_refid = ref NONE: string option ref; +val pgip_refid = ref NONE: string option ref; val pgip_refseq = ref NONE: string option ref; local @@ -176,7 +181,7 @@ "pgip" ([("tag", pgip_tag), ("class", pgip_class), - ("seq", string_of_int (pgip_serial())), + ("seq", string_of_int (pgip_serial())), ("id", !pgip_id)] @ if_none (Option.map (single o (pair "destid")) (! pgip_refid)) [] @ (* destid=refid since Isabelle only communicates back to sender, @@ -188,10 +193,10 @@ in -fun init_pgip_session_id () = +fun init_pgip_session_id () = pgip_id := getenv "HOSTNAME" ^ "/" ^ getenv "USER" ^ "/" ^ getenv "ISABELLE_PID" ^ "/" ^ Time.toString (Time.now ()) - + fun matching_pgip_id id = (id = !pgip_id) @@ -203,7 +208,7 @@ fun issue_pgips ps = if pgip_emacs_compatibility() then decorated_output (*add urgent message annotation*) - (oct_char "360") (oct_char "361") "" + (special "360") (special "361") "" (assemble_pgips ps) else writeln_default (assemble_pgips ps); @@ -215,7 +220,7 @@ fun issue_pgip resp attrs txt = if pgip_emacs_compatibility () then decorated_output (*add urgent message annotation*) - (oct_char "360") (oct_char "361") "" + (special "360") (special "361") "" (assemble_pgip resp attrs txt) else writeln_default (assemble_pgip resp attrs txt); @@ -274,28 +279,21 @@ in fun setup_messages () = - (writeln_fn := message "normalresponse" [message_area] "" "" ""; - - priority_fn := message "normalresponse" [message_area, urgent_indication] - (oct_char "360") (oct_char "361") ""; - - tracing_fn := message "normalresponse" [message_area, tracing_category] - (oct_char "360" ^ oct_char "375") (oct_char "361") ""; - - info_fn := message "normalresponse" [message_area, info_category] - (oct_char "362") (oct_char "363") "+++ "; - - debug_fn := message "normalresponse" [message_area, internal_category] - (oct_char "362") (oct_char "363") "+++ "; - - warning_fn := message "errorresponse" [nonfatal] - (oct_char "362") (oct_char "363") "### "; - - error_fn := message "errorresponse" [fatal] - (oct_char "364") (oct_char "365") "*** "; - - panic_fn := message "errorresponse" [panic] - (oct_char "364") (oct_char "365") "!!! "); + (writeln_fn := (fn s => message "normalresponse" [message_area] "" "" "" s); + priority_fn := (fn s => message "normalresponse" [message_area, urgent_indication] + (special "360") (special "361") "" s); + tracing_fn := (fn s => message "normalresponse" [message_area, tracing_category] + (special "360" ^ special "375") (special "361") "" s); + info_fn := (fn s => message "normalresponse" [message_area, info_category] + (special "362") (special "363") "+++ " s); + debug_fn := (fn s => message "normalresponse" [message_area, internal_category] + (special "362") (special "363") "+++ " s); + warning_fn := (fn s => message "errorresponse" [nonfatal] + (special "362") (special "363") "### " s); + error_fn := (fn s => message "errorresponse" [fatal] + (special "364") (special "365") "*** " s); + panic_fn := (fn s => message "errorresponse" [panic] + (special "364") (special "365") "!!! " s)); (* accumulate printed output in a single PGIP response (inside ) *) @@ -310,7 +308,7 @@ issue_pgip elt attrs (XML.element "pgmltext" [] (! lines)) end; -val emacs_notify = decorated_output (oct_char "360") (oct_char "361") ""; +fun emacs_notify s = decorated_output (special "360") (special "361") "" s; fun tell_clear_goals () = if pgip () then @@ -344,13 +342,13 @@ local fun tmp_markers f = - setmp Display.current_goals_markers (oct_char "366", oct_char "367", "") f (); + setmp Display.current_goals_markers (special "366", special "367", "") f (); fun statedisplay prts = issue_pgip "proofstate" [] (XML.element "pgml" [] [XML.element "statedisplay" [] [Pretty.output (Pretty.chunks prts)]]); - + fun print_current_goals n m st = if pgml () then statedisplay (Display.pretty_current_goals n m st) else tmp_markers (fn () => Display.print_current_goals_default n m st); @@ -365,7 +363,8 @@ (Display.print_current_goals_fn := print_current_goals; Toplevel.print_state_fn := print_state; (* FIXME: check next octal char won't appear in pgip? *) - Toplevel.prompt_state_fn := (suffix (oct_char "372") o Toplevel.prompt_state_default)); + Toplevel.prompt_state_fn := (fn s => suffix (special "372") + (Toplevel.prompt_state_default s))); end; @@ -541,8 +540,8 @@ val thm_deps_option = (pgipbool, with_default (fn () => Bool.toString (Output.has_mode thm_depsN)), - (fn "false" => print_mode := (! print_mode \ thm_depsN) - | "true" => print_mode := (thm_depsN ins ! print_mode) + (fn "false" => change print_mode (remove (op =) thm_depsN) + | "true" => change print_mode (insert (op =) thm_depsN) | x => error ("thm_deps_option: illegal value: " ^ x))); local @@ -910,21 +909,21 @@ (empty "openblock") end - fun xmls_of_qed (name,markup) = - let val qedmarkup = - (case name of - "sorry" => markup "postponegoal" - | "oops" => markup "giveupgoal" - | "done" => markup "closegoal" - | "by" => markup "closegoal" (* nested or toplevel *) - | "qed" => markup "closegoal" (* nested or toplevel *) - | "." => markup "closegoal" (* nested or toplevel *) - | ".." => markup "closegoal" (* nested or toplevel *) - | other => (* default to closegoal: may be wrong for extns *) - (parse_warning - ("Unrecognized qed command: " ^ quote other); - markup "closegoal")) - in qedmarkup @ (empty "closeblock") end + fun xmls_of_qed (name,markup) = + let val qedmarkup = + (case name of + "sorry" => markup "postponegoal" + | "oops" => markup "giveupgoal" + | "done" => markup "closegoal" + | "by" => markup "closegoal" (* nested or toplevel *) + | "qed" => markup "closegoal" (* nested or toplevel *) + | "." => markup "closegoal" (* nested or toplevel *) + | ".." => markup "closegoal" (* nested or toplevel *) + | other => (* default to closegoal: may be wrong for extns *) + (parse_warning + ("Unrecognized qed command: " ^ quote other); + markup "closegoal")) + in qedmarkup @ (empty "closeblock") end fun xmls_of_kind kind (name,toks,str) = let val markup = markup_text str in @@ -1080,7 +1079,7 @@ (* TODO: would be cleaner to define a datatype here for the accepted elements, and mapping functions to/from strings. At the moment this list must coincide with the strings in the function process_pgip_element. *) -val isabelle_acceptedpgipelems = +val isabelle_acceptedpgipelems = ["askpgip","askpgml","askprefs","getpref","setpref", "proverinit","proverexit","startquiet","stopquiet", "pgmlsymbolson", "pgmlsymbolsoff", @@ -1093,14 +1092,14 @@ "abortfile", "changecwd", "systemcmd"]; fun usespgip () = - issue_pgip - "usespgip" - [("version", isabelle_pgip_version_supported)] - (XML.element "acceptedpgipelems" [] - (map (fn s=>XML.element "pgipelem" - [] (* if threads: possibility to add async here *) - [s]) - isabelle_acceptedpgipelems)) + issue_pgip + "usespgip" + [("version", isabelle_pgip_version_supported)] + (XML.element "acceptedpgipelems" [] + (map (fn s=>XML.element "pgipelem" + [] (* if threads: possibility to add async here *) + [s]) + isabelle_acceptedpgipelems)) fun usespgml () = issue_pgipe "usespgml" [("version", isabelle_pgml_version_supported)] @@ -1197,15 +1196,15 @@ file we remove the path. Leaving it there can cause confusion with difference in batch mode.a NB: PGIP does not assume that the prover has a load path. *) - local + local val current_working_dir = ref (NONE : string option) in - fun changecwd dir = - (case (!current_working_dir) of - NONE => () + fun changecwd dir = + (case (!current_working_dir) of + NONE => () | SOME dir => ThyLoad.del_path dir; - ThyLoad.add_path dir; - current_working_dir := SOME dir) + ThyLoad.add_path dir; + current_working_dir := SOME dir) end val topnode = Toplevel.node_of o Toplevel.get_state @@ -1230,8 +1229,8 @@ | "proverexit" => isarcmd "quit" | "startquiet" => isarcmd "disable_pr" | "stopquiet" => isarcmd "enable_pr" - | "pgmlsymbolson" => (print_mode := !print_mode @ ["xsymbols"]) - | "pgmlsymbolsoff" => (print_mode := (!print_mode \ "xsymbols")) + | "pgmlsymbolson" => change print_mode (insert (op =) Symbol.xsymbolsN) + | "pgmlsymbolsoff" => change print_mode (remove (op =) Symbol.xsymbolsN) (* properproofcmd: proper commands which belong in script *) (* FIXME: next ten are by Eclipse interface, can be removed in favour of dostep *) (* NB: Isar doesn't make lemma name of goal accessible during proof *) @@ -1261,9 +1260,9 @@ | "parsescript" => parsescript (xmltext data) attrs (* just pass back attrs unchanged *) | "showproofstate" => isarcmd "pr" | "showctxt" => isarcmd "print_theory" (* more useful than print_context *) - | "searchtheorems" => isarcmd ("thms_containing " ^ (xmltext data)) - | "setlinewidth" => isarcmd ("pretty_setmargin " ^ (xmltext data)) - | "viewdoc" => isarcmd ("print_" ^ (xmltext data)) (* FIXME: isatool doc? *) + | "searchtheorems" => isarcmd ("thms_containing " ^ xmltext data) + | "setlinewidth" => isarcmd ("pretty_setmargin " ^ xmltext data) + | "viewdoc" => isarcmd ("print_" ^ xmltext data) (* FIXME: isatool doc? *) (* properfilecmd: proper theory-level script commands *) (* FIXME: next three are sent by Eclipse, can be removed in favour of doitem *) | "opentheory" => isarscript data @@ -1271,14 +1270,14 @@ | "closetheory" => let val thyname = topthy_name() in (isarscript data; - writeln ("Theory \""^thyname^"\" completed.")) + writeln ("Theory " ^ quote thyname ^ " completed.")) end (* improperfilecmd: theory-level commands not in script *) | "doitem" => isarscript data | "undoitem" => isarcmd "ProofGeneral.undo" | "redoitem" => isarcmd "ProofGeneral.redo" | "aborttheory" => isarcmd ("init_toplevel") - | "retracttheory" => isarcmd ("kill_thy " ^ (quote (thyname_attr attrs))) + | "retracttheory" => isarcmd ("kill_thy " ^ quote (thyname_attr attrs)) | "loadfile" => use_thy_or_ml_file (fileurl_of attrs) | "openfile" => (openfile_retract (fileurl_of attrs); currently_open_file := SOME (fileurl_of attrs)) @@ -1300,19 +1299,19 @@ XML.Elem ("pgip", attrs, pgips) => (let val class = xmlattr "class" attrs - val dest = xmlattro "destid" attrs + val dest = xmlattro "destid" attrs val _ = (pgip_refid := xmlattro "id" attrs; - pgip_refseq := xmlattro "seq" attrs) + pgip_refseq := xmlattro "seq" attrs) in - (* We respond to broadcast messages to provers, or + (* We respond to broadcast messages to provers, or messages intended uniquely for us. Silently ignore rest. *) case dest of - NONE => if (class = "pa") then - (List.app process_pgip_element pgips; true) - else false - | SOME id => if (matching_pgip_id id) then - (List.app process_pgip_element pgips; true) - else false + NONE => if (class = "pa") then + (List.app process_pgip_element pgips; true) + else false + | SOME id => if (matching_pgip_id id) then + (List.app process_pgip_element pgips; true) + else false end) | _ => raise PGIP "Invalid PGIP packet received") handle (PGIP msg) => @@ -1339,11 +1338,11 @@ case pgipo of NONE => () | SOME (pgip,src') => - let - val ready' = (process_pgip_tree pgip) handle e => (handler (e,SOME src'); true) - in - loop ready' src' - end + let + val ready' = (process_pgip_tree pgip) handle e => (handler (e,SOME src'); true) + in + loop ready' src' + end end handle e => handler (e,SOME src) (* i.e. error in ready/XML parse *) and handler (e,srco) = @@ -1426,7 +1425,7 @@ fun set_prompts true _ = ml_prompts "ML> " "ML# " | set_prompts false true = ml_prompts "PGIP-ML>" "PGIP-ML# " - | set_prompts false false = ml_prompts ("> " ^ oct_char "372") ("- " ^ oct_char "373"); + | set_prompts false false = ml_prompts ("> " ^ special "372") ("- " ^ special "373"); fun init_setup isar pgip = (conditional (not (! initialized)) (fn () => @@ -1439,10 +1438,10 @@ setup_present_hook (); set initialized; ())); sync_thy_loader (); - print_mode := proof_generalN :: (! print_mode \ proof_generalN); + change print_mode (cons proof_generalN o remove (op =) proof_generalN); if pgip then (init_pgip_session_id(); - print_mode := pgmlN :: (pgmlatomsN :: (! print_mode \ pgmlN \ pgmlatomsN))) + change print_mode (append [pgmlN, pgmlatomsN] o fold (remove (op =)) [pgmlN, pgmlatomsN])) else pgip_emacs_compatibility_flag := true; (* assume this for PG <3.6 compatibility *) set quick_and_dirty;