# HG changeset patch # User aspinall # Date 1094672890 -7200 # Node ID 5ca1fd9dec83784a9c6b607e04dde0f323559f7a # Parent b6788dbd2ef9b4bb30a2b8ff8c27059ef14277da Support parsing of -- {* comments *}. Add extra output channels. diff -r b6788dbd2ef9 -r 5ca1fd9dec83 src/Pure/proof_general.ML --- a/src/Pure/proof_general.ML Wed Sep 08 19:37:07 2004 +0200 +++ b/src/Pure/proof_general.ML Wed Sep 08 21:48:10 2004 +0200 @@ -52,6 +52,7 @@ structure P = OuterParse + (* PGIP messaging mode (independent of PGML output) *) val pgip_active = ref false; @@ -248,7 +249,9 @@ local val display_area = ("area", "display") val message_area = ("area", "message") - val tracing_category = ("category", "tracing") + val internal_category = ("messagecategory", "internal") + val info_category = ("messagecategory", "information") + val tracing_category = ("messagecategory", "tracing") val urgent_indication = ("urgent", "y") val nonfatal = ("fatality", "nonfatal") val fatal = ("fatality", "fatal") @@ -268,6 +271,12 @@ 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") "### "; @@ -898,14 +907,51 @@ markup_text str "spuriouscmd") end -fun xmls_of_impropers [] = [] - | xmls_of_impropers toks = +fun markup_toks [] _ = [] + | markup_toks toks x = markup_text (implode (map OuterLex.unparse toks)) x + +fun markup_comment_whs [] = [] + | markup_comment_whs (toks as t::ts) = (* this would be a lot neater if we could match on toks! *) + let + val (prewhs,rest) = take_prefix (OuterLex.is_kind OuterLex.Space) toks + in + if (prewhs <> []) then + XML.text (implode (map OuterLex.unparse prewhs)) + :: (markup_comment_whs rest) + else + (markup_text (OuterLex.unparse t) "comment") @ + (markup_comment_whs ts) + end + +fun xmls_pre_cmd [] = ([],[]) + | xmls_pre_cmd toks = let - val (whs,rest) = take_prefix (not o OuterLex.is_proper) toks - fun markup [] _ = [] - | markup toks x = markup_text (implode (map OuterLex.unparse toks)) x + (* an extra token is needed to terminate the command *) + val sync = OuterSyntax.scan "\\<^sync>"; + val spaceP = Scan.bulk (Scan.one (fn t =>not (OuterLex.is_proper t)) >> OuterLex.val_of) >> implode + val text_with_whs = + ((spaceP || Scan.succeed "") -- + (P.short_ident || P.long_ident || P.sym_ident || P.string || P.number || P.verbatim) >> op^) + -- (spaceP || Scan.succeed "") >> op^ + val (prewhs,rest1) = take_prefix (not o OuterLex.is_proper) (toks@sync) + (* NB: this collapses litcomment,(litcomment|whitespace)* to a single litcomment *) + val (_,rest2) = (Scan.bulk (P.$$$ "--" |-- text_with_whs) >> implode || Scan.succeed "") rest1 + val (postwhs,rest3) = take_prefix (not o OuterLex.is_proper) rest2 in - (markup whs "comment") @ (markup rest "unparseable") + ((markup_comment_whs prewhs) @ + (if (length rest2 = length rest1) then [] + else markup_text (implode + (map OuterLex.unparse (take (length rest1 - length rest2, rest1)))) + "litcomment") @ + (markup_comment_whs postwhs), + take (length rest3 - 1,rest3)) + end + +fun xmls_of_impropers toks = + let + val (xmls,rest) = xmls_pre_cmd toks + in + xmls @ (markup_toks rest "unparseable") end fun markup_unparseable str = markup_text str "unparseable" @@ -916,6 +962,7 @@ local (* we have to weave together the whitespace/comments with proper tokens to reconstruct the input. *) + (* TODO: see if duplicating isar_output/parse_thy can help here *) fun match_tokens ([],us,vs) = (rev vs,us) (* used, unused *) | match_tokens (t::ts,w::ws,vs) = @@ -930,19 +977,18 @@ | parse_loop ([],itoks,xmls) = xmls @ (xmls_of_impropers itoks) | parse_loop ((nm,toks,_)::trs,itoks,xmls) = let - (* first proper token is command, except FIXME for -- *) - val (prewhs,cmditoks') = take_prefix (not o OuterLex.is_proper) itoks + (* first proper token after whitespace/litcomment/whitespace is command *) + val (xmls_pre_cmd,cmditoks') = xmls_pre_cmd itoks val (cmdtok,itoks') = case cmditoks' of x::xs => (x,xs) - | _ => error("proof_general/parse_loop impossible") + | _ => error("proof_general/parse_loop impossible") val (utoks,itoks'') = match_tokens (toks,itoks',[]) (* FIXME: should take trailing [w/s+] semicolon too in utoks *) val str = implode (map OuterLex.unparse (cmdtok::utoks)) - val xmls_whs = xmls_of_impropers prewhs val xmls_tr = xmls_of_transition (nm,str,toks) in - parse_loop(trs,itoks'',xmls @ xmls_whs @ xmls_tr) + parse_loop(trs,itoks'',xmls @ xmls_pre_cmd @ xmls_tr) end in (let val toks = OuterSyntax.scan str @@ -1071,7 +1117,8 @@ | (xml as (XML.Elem (elem, attrs, data))) => (case elem of (* protocol config *) - "askpgip" => (usespgip (); send_pgip_config ()) + "askpgip" => (pgip_emacs_compatibility_flag:=false; (* PG>=3.6 or other PGIP interface *) + usespgip (); send_pgip_config ()) | "askpgml" => usespgml () (* proverconfig *) | "askprefs" => hasprefs () @@ -1092,7 +1139,7 @@ | "closegoal" => isarscript data | "giveupgoal" => isarscript data | "postponegoal" => isarscript data - | "comment" => isarscript data + | "comment" => isarscript data (* NB: should be ignored, but process anyway *) | "litcomment" => isarscript data | "spuriouscmd" => isarscript data | "badcmd" => isarscript data @@ -1152,14 +1199,8 @@ (error (msg ^ "\nPGIP error occured in XML text below:\n" ^ (XML.string_of_tree xml)))) -(* for export to Emacs *) -(* val process_pgip = process_pgip_tree o XML.tree_of_string; *) -(* FIXME: for temporary compatibility with PG 3.4, we engage special characters - during output *) -fun process_pgip s = - (pgip_emacs_compatibility_flag := true; - process_pgip_tree (XML.tree_of_string s); - pgip_emacs_compatibility_flag := false) +val process_pgip = process_pgip_tree o XML.tree_of_string; + end @@ -1277,7 +1318,8 @@ print_mode := proof_generalN :: (! print_mode \ proof_generalN); if pgip then print_mode := pgmlN :: (pgmlatomsN :: (! print_mode \ pgmlN \ pgmlatomsN)) - else (); + else + pgip_emacs_compatibility_flag := true; (* assume this for PG <3.6 compatibility *) set quick_and_dirty; ThmDeps.enable (); set_prompts isar pgip; @@ -1291,7 +1333,8 @@ Isar.sync_main ()) else isa_restart ()); fun init_pgip false = panic "Sorry, PGIP not supported for Isabelle/classic mode." - | init_pgip true = (init_setup true true; pgip_toplevel tty_src); + | init_pgip true = (init_setup true true; + pgip_toplevel tty_src);