# HG changeset patch # User wenzelm # Date 1208442652 -7200 # Node ID 4ea64590d28b738e837d7fdd28b6b73879559702 # Parent 334d3fa649eab8d20c649962a1a44366440c6ad4 replaced token translations by common markup; diff -r 334d3fa649ea -r 4ea64590d28b src/Pure/ProofGeneral/proof_general_emacs.ML --- a/src/Pure/ProofGeneral/proof_general_emacs.ML Thu Apr 17 16:30:51 2008 +0200 +++ b/src/Pure/ProofGeneral/proof_general_emacs.ML Thu Apr 17 16:30:52 2008 +0200 @@ -53,70 +53,27 @@ end; -(* token translations *) - -local - -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 = - (bg_tag () ^ x ^ end_tag (), Symbol.length (Symbol.explode x)); - -fun free_or_skolem x = - (case try Name.dest_skolem x of - NONE => tagit free_tag x - | SOME x' => tagit skolem_tag x'); - -fun var_or_skolem s = - (case Lexicon.read_variable s of - SOME (x, i) => - (case try Name.dest_skolem x of - NONE => tagit var_tag s - | SOME x' => tagit skolem_tag - (setmp show_question_marks true Term.string_of_vname (x', i))) - | NONE => tagit var_tag s); - -val proof_general_trans = - Syntax.tokentrans_mode proof_generalN - [("class", tagit class_tag), - ("tfree", tagit tfree_tag), - ("tvar", tagit tvar_tag), - ("free", free_or_skolem), - ("bound", tagit bound_tag), - ("var", var_or_skolem)]; - -in - -val _ = Context.>> (Context.map_theory (Sign.add_tokentrfuns proof_general_trans)); - -end; - - (* common markup *) -fun proof_general_markup (name, props) = +val _ = Markup.add_mode proof_generalN (fn (name, props) => let val (bg1, en1) = if name = Markup.stateN then (special "366" ^ "\n", "\n" ^ special "367") else if name = Markup.sendbackN then (special "376", special "377") else if name = Markup.hiliteN then (special "327", special "330") + else if name = Markup.classN then (special "351", special "350") + else if name = Markup.tfreeN then (special "352", special "350") + else if name = Markup.tvarN then (special "353", special "350") + else if name = Markup.freeN then (special "354", special "350") + else if name = Markup.boundN then (special "355", special "350") + else if name = Markup.varN then (special "356", special "350") + else if name = Markup.skolemN then (special "357", special "350") else ("", ""); val (bg2, en2) = if print_mode_active test_markupN then XML.output_markup (name, props) else ("", ""); - in (bg1 ^ bg2, en2 ^ en1) end; - -val _ = Markup.add_mode proof_generalN proof_general_markup; + in (bg1 ^ bg2, en2 ^ en1) end); (* messages and notification *) diff -r 334d3fa649ea -r 4ea64590d28b src/Pure/ProofGeneral/proof_general_pgip.ML --- a/src/Pure/ProofGeneral/proof_general_pgip.ML Thu Apr 17 16:30:51 2008 +0200 +++ b/src/Pure/ProofGeneral/proof_general_pgip.ML Thu Apr 17 16:30:52 2008 +0200 @@ -44,7 +44,7 @@ fun pgml_sym s = (case Symbol.decode s of Symbol.Char s => XML.text s - | Symbol.Sym sn => + | Symbol.Sym sn => let val ascii = implode (map xsym_output (Symbol.explode s)) in if !pgmlsymbols_flag then XML.element "sym" [("name", sn)] [XML.text ascii] else ascii end @@ -63,53 +63,6 @@ end; -(* token translations *) - -local - -val class_tag = "class" -val tfree_tag = "tfree" -val tvar_tag = "tvar" -val free_tag = "free" -val bound_tag = "bound" -val var_tag = "var" -val skolem_tag = "skolem" - -fun xml_atom kind x = XML.element "atom" [("kind", kind)] [XML.text x]; - -fun tagit kind x = - (xml_atom kind x, Symbol.length (Symbol.explode x)); - -fun free_or_skolem x = - (case try Name.dest_skolem x of - NONE => tagit free_tag x - | SOME x' => tagit skolem_tag x'); - -fun var_or_skolem s = - (case Lexicon.read_variable s of - SOME (x, i) => - (case try Name.dest_skolem x of - NONE => tagit var_tag s - | SOME x' => tagit skolem_tag - (setmp show_question_marks true Term.string_of_vname (x', i))) - | NONE => tagit var_tag s); - -val proof_general_trans = - Syntax.tokentrans_mode proof_generalN - [("class", tagit class_tag), - ("tfree", tagit tfree_tag), - ("tvar", tagit tvar_tag), - ("free", free_or_skolem), - ("bound", tagit bound_tag), - ("var", var_or_skolem)]; - -in - -val _ = Context.>> (Context.map_theory (Sign.add_tokentrfuns proof_general_trans)); - -end; - - (* assembling and issuing PGIP packets *) val pgip_refid = ref NONE: string option ref; @@ -146,10 +99,10 @@ val output_pgips = XML.string_of o PgipOutput.output o assemble_pgips o map PgipOutput.output; -val output_pgmlterm = +val output_pgmlterm = XML.string_of o Pgml.pgmlterm_to_xml; -val output_pgmltext = +val output_pgmltext = XML.string_of o Pgml.pgml_to_xml; @@ -179,10 +132,10 @@ delayed_msgs := pgip :: ! delayed_msgs else issue_pgip pgip - fun wrap_pgml area s = - if String.isPrefix " + if name = Markup.blockN then block_markup markup + else if name = Markup.breakN then break_markup markup + else if name = Markup.fbreakN then fbreak_markup markup + else if name = Markup.stateN then state_markup + else if member (op =) token_markups name then XML.output_markup ("atom", [("kind", name)]) + else ("", "")); end; @@ -562,13 +508,13 @@ fun proverexit _ = isarcmd "quit" -fun set_proverflag_quiet b = +fun set_proverflag_quiet b = isarcmd (if b then "disable_pr" else "enable_pr") fun set_proverflag_pgmlsymbols b = (pgmlsymbols_flag := b; NAMED_CRITICAL "print_mode" (fn () => - change print_mode + change print_mode (fn mode => remove (op =) Symbol.xsymbolsN mode @ (if b then [Symbol.xsymbolsN] else [])))) @@ -577,17 +523,17 @@ Proofterm.proofs := (if b then 1 else 2)) fun setproverflag (Setproverflag vs) = - let + let val flagname = #flagname vs val value = #value vs in (case flagname of "quiet" => set_proverflag_quiet value | "pgmlsymbols" => set_proverflag_pgmlsymbols value - | "metainfo:thmdeps" => set_proverflag_thmdeps value - | _ => log_msg ("Unrecognised prover control flag: " ^ + | "metainfo:thmdeps" => set_proverflag_thmdeps value + | _ => log_msg ("Unrecognised prover control flag: " ^ (quote flagname) ^ " ignored.")) - end + end fun dostep (Dostep vs) = @@ -643,13 +589,13 @@ | SOME prf => filter (String.isPrefix (unprefix (prf ^ NameSpace.separator) thy)) (thms_of_thy prf)) val qualified_thms_of_thy = (* for global query with single response *) - (map fst) o NameSpace.dest_table o PureThy.theorems_of o ThyInfo.get_theory; + (map fst) o NameSpace.dest_table o PureThy.theorems_of o ThyInfo.get_theory; (* da: this version is equivalent to my previous, but splits up theorem sets with names that I can't get to access later with get_thm. Anyway, would rather use sets. Is above right way to get qualified names in that case? Filtering required again? map PureThy.get_name_hint o filter PureThy.has_name_hint o map snd o PureThy.thms_of o ThyInfo.get_theory; *) - in + in case (thyname,objtype) of (NONE, NONE) => setids (idtable ObjFile NONE (ThyInfo.get_names())) (*FIXME: uris*) @@ -743,11 +689,11 @@ (thy::(rest as _::_)) => (ThyInfo.get_theory thy, space_implode "." rest) | [plainid] => (topthy(),plainid) | _ => raise Toplevel.UNDEF (* assert false *) - end - + end + fun idvalue strings = - issue_pgip (Idvalue { thyname=thyname, objtype=objtype, name=name, + issue_pgip (Idvalue { thyname=thyname, objtype=objtype, name=name, text=[XML.Elem("pgml",[], map XML.Output strings)] }) @@ -1169,3 +1115,4 @@ end end; + diff -r 334d3fa649ea -r 4ea64590d28b src/Pure/Tools/isabelle_process.ML --- a/src/Pure/Tools/isabelle_process.ML Thu Apr 17 16:30:51 2008 +0200 +++ b/src/Pure/Tools/isabelle_process.ML Thu Apr 17 16:30:52 2008 +0200 @@ -112,43 +112,6 @@ Output.prompt_fn := message "G"); -(* token translations *) - -local - -fun markup kind x = - ((YXML.output_markup (kind, []) |-> enclose) (Output.output x), Symbol.length (Symbol.explode x)); - -fun free_or_skolem x = - (case try Name.dest_skolem x of - NONE => markup Markup.freeN x - | SOME x' => markup Markup.skolemN x'); - -fun var_or_skolem s = - (case Lexicon.read_variable s of - SOME (x, i) => - (case try Name.dest_skolem x of - NONE => markup Markup.varN s - | SOME x' => markup Markup.skolemN - (setmp show_question_marks true Term.string_of_vname (x', i))) - | NONE => markup Markup.varN s); - -val token_trans = - Syntax.tokentrans_mode full_markupN - [("class", markup Markup.classN), - ("tfree", markup Markup.tfreeN), - ("tvar", markup Markup.tvarN), - ("free", free_or_skolem), - ("bound", markup Markup.boundN), - ("var", var_or_skolem)]; - -in - -val _ = Context.>> (Context.map_theory (Sign.add_tokentrfuns token_trans)); - -end; - - (* init *) fun init () =