# HG changeset patch # User wenzelm # Date 1310324344 -7200 # Node ID 70072780e095a7d7ab4aefc4471282de71668546 # Parent a0ed7bc688b5b17bc5db2e8b09de776df1c214da inner syntax supports inlined YXML according to Term_XML (particularly useful for producing text under program control); tuned signature; diff -r a0ed7bc688b5 -r 70072780e095 NEWS --- a/NEWS Sun Jul 10 17:58:11 2011 +0200 +++ b/NEWS Sun Jul 10 20:59:04 2011 +0200 @@ -146,6 +146,12 @@ *** ML *** +* The inner syntax of sort/type/term/prop supports inlined YXML +representations within quoted string tokens. By encoding logical +entities via Term_XML (in ML or Scala) concrete syntax can be +bypassed, which is particularly useful for producing bits of text +under external program control. + * Antiquotations for ML and document preparation are managed as theory data, which requires explicit setup. diff -r a0ed7bc688b5 -r 70072780e095 src/Pure/General/xml_data.ML --- a/src/Pure/General/xml_data.ML Sun Jul 10 17:58:11 2011 +0200 +++ b/src/Pure/General/xml_data.ML Sun Jul 10 20:59:04 2011 +0200 @@ -21,18 +21,18 @@ signature XML_DATA = sig - structure Make: XML_DATA_OPS where type 'a T = 'a -> XML.body + structure Encode: XML_DATA_OPS where type 'a T = 'a -> XML.body exception XML_ATOM of string exception XML_BODY of XML.body - structure Dest: XML_DATA_OPS where type 'a T = XML.body -> 'a + structure Decode: XML_DATA_OPS where type 'a T = XML.body -> 'a end; structure XML_Data: XML_DATA = struct -(** make **) +(** encode **) -structure Make = +structure Encode = struct type 'a T = 'a -> XML.body; @@ -83,12 +83,12 @@ -(** dest **) +(** decode **) exception XML_ATOM of string; exception XML_BODY of XML.tree list; -structure Dest = +structure Decode = struct type 'a T = XML.body -> 'a; diff -r a0ed7bc688b5 -r 70072780e095 src/Pure/General/xml_data.scala --- a/src/Pure/General/xml_data.scala Sun Jul 10 17:58:11 2011 +0200 +++ b/src/Pure/General/xml_data.scala Sun Jul 10 20:59:04 2011 +0200 @@ -10,9 +10,9 @@ object XML_Data { - /** make **/ + /** encode **/ - object Make + object Encode { type T[A] = A => XML.Body @@ -76,12 +76,12 @@ - /** dest **/ + /** decode **/ class XML_Atom(s: String) extends Exception(s) class XML_Body(body: XML.Body) extends Exception - object Dest + object Decode { type T[A] = XML.Body => A diff -r a0ed7bc688b5 -r 70072780e095 src/Pure/General/yxml.ML --- a/src/Pure/General/yxml.ML Sun Jul 10 17:58:11 2011 +0200 +++ b/src/Pure/General/yxml.ML Sun Jul 10 20:59:04 2011 +0200 @@ -16,6 +16,7 @@ signature YXML = sig val escape_controls: string -> string + val detect: string -> bool val output_markup: Markup.T -> string * string val element: string -> XML.attributes -> string list -> string val string_of_body: XML.body -> string @@ -49,6 +50,8 @@ val XY = X ^ Y; val XYX = XY ^ X; +val detect = exists_string (fn s => s = X); + (* output *) diff -r a0ed7bc688b5 -r 70072780e095 src/Pure/Isar/token.ML --- a/src/Pure/Isar/token.ML Sun Jul 10 17:58:11 2011 +0200 +++ b/src/Pure/Isar/token.ML Sun Jul 10 20:59:04 2011 +0200 @@ -180,8 +180,9 @@ (* token content *) -fun source_of (Token ((source, (pos, _)), _, _)) = - YXML.string_of (XML.Elem (Markup.token (Position.properties_of pos), [XML.Text source])); +fun source_of (Token ((source, (pos, _)), (_, x), _)) = + if YXML.detect x then x + else YXML.string_of (XML.Elem (Markup.token (Position.properties_of pos), [XML.Text source])); fun source_position_of (Token ((source, (pos, _)), _, _)) = (source, pos); diff -r a0ed7bc688b5 -r 70072780e095 src/Pure/PIDE/isar_document.ML --- a/src/Pure/PIDE/isar_document.ML Sun Jul 10 17:58:11 2011 +0200 +++ b/src/Pure/PIDE/isar_document.ML Sun Jul 10 20:59:04 2011 +0200 @@ -18,10 +18,10 @@ val old_id = Document.parse_id old_id_string; val new_id = Document.parse_id new_id_string; val edits = YXML.parse_body edits_yxml |> - let open XML_Data.Dest + let open XML_Data.Decode in list (pair string (option (list (pair (option int) (option int))))) end; val headers = YXML.parse_body headers_yxml |> - let open XML_Data.Dest + let open XML_Data.Decode in list (pair string (triple string (list string) (list string))) end; val await_cancellation = Document.cancel_execution state; diff -r a0ed7bc688b5 -r 70072780e095 src/Pure/PIDE/isar_document.scala --- a/src/Pure/PIDE/isar_document.scala Sun Jul 10 17:58:11 2011 +0200 +++ b/src/Pure/PIDE/isar_document.scala Sun Jul 10 20:59:04 2011 +0200 @@ -143,12 +143,12 @@ edits: List[Document.Edit_Command_ID], headers: List[(String, Thy_Header.Header)]) { val arg1 = - { import XML_Data.Make._ + { import XML_Data.Encode._ list(pair(string, option(list(pair(option(long), option(long))))))(edits) } val arg2 = - { import XML_Data.Make._ - list(pair(string, Thy_Header.make_xml_data))(headers) } + { import XML_Data.Encode._ + list(pair(string, Thy_Header.encode_xml_data))(headers) } input("Isar_Document.edit_version", Document.ID(old_id), Document.ID(new_id), diff -r a0ed7bc688b5 -r 70072780e095 src/Pure/Syntax/syntax.ML --- a/src/Pure/Syntax/syntax.ML Sun Jul 10 17:58:11 2011 +0200 +++ b/src/Pure/Syntax/syntax.ML Sun Jul 10 20:59:04 2011 +0200 @@ -17,7 +17,8 @@ val ambiguity_level: int Config.T val ambiguity_limit: int Config.T val read_token: string -> Symbol_Pos.T list * Position.T - val parse_token: Proof.context -> Markup.T -> string -> Symbol_Pos.T list * Position.T + val parse_token: Proof.context -> (XML.tree list -> 'a) -> + Markup.T -> (Symbol_Pos.T list * Position.T -> 'a) -> string -> 'a val parse_sort: Proof.context -> string -> sort val parse_typ: Proof.context -> string -> typ val parse_term: Proof.context -> string -> term @@ -193,11 +194,10 @@ Config.int (Config.declare "syntax_ambiguity_limit" (fn _ => Config.Int 10)); -(* read token -- with optional YXML encoding of position *) +(* outer syntax token -- with optional YXML content *) -fun read_token str = +fun explode_token tree = let - val tree = YXML.parse str handle Fail msg => error msg; val text = XML.content_of [tree]; val pos = (case tree of @@ -207,15 +207,26 @@ | XML.Text _ => Position.none); in (Symbol_Pos.explode (text, pos), pos) end; +fun read_token str = explode_token (YXML.parse str handle Fail msg => error msg); + +fun parse_token ctxt decode markup parse str = + let + fun parse_tree tree = + let + val (syms, pos) = explode_token tree; + val _ = Context_Position.report ctxt pos markup; + in parse (syms, pos) end; + in + (case YXML.parse_body str handle Fail msg => error msg of + body as [tree as XML.Elem ((name, _), _)] => + if name = Markup.tokenN then parse_tree tree else decode body + | [tree as XML.Text _] => parse_tree tree + | body => decode body) + end; + (* (un)parsing *) -fun parse_token ctxt markup str = - let - val (syms, pos) = read_token str; - val _ = Context_Position.report ctxt pos markup; - in (syms, pos) end; - val parse_sort = operation #parse_sort; val parse_typ = operation #parse_typ; val parse_term = operation #parse_term; diff -r a0ed7bc688b5 -r 70072780e095 src/Pure/Syntax/syntax_phases.ML --- a/src/Pure/Syntax/syntax_phases.ML Sun Jul 10 17:58:11 2011 +0200 +++ b/src/Pure/Syntax/syntax_phases.ML Sun Jul 10 20:59:04 2011 +0200 @@ -320,80 +320,79 @@ cat_error msg ("Failed to parse " ^ kind ^ Markup.markup Markup.report (Context_Position.reported_text ctxt pos Markup.bad "")); -fun parse_sort ctxt text = - let - val (syms, pos) = Syntax.parse_token ctxt Markup.sort text; - val S = +fun parse_sort ctxt = + Syntax.parse_token ctxt Term_XML.Decode.sort Markup.sort + (fn (syms, pos) => parse_raw ctxt "sort" (syms, pos) |> report_result ctxt pos |> sort_of_term - handle ERROR msg => parse_failed ctxt pos msg "sort"; - in Type.minimize_sort (Proof_Context.tsig_of ctxt) S end; + |> Type.minimize_sort (Proof_Context.tsig_of ctxt) + handle ERROR msg => parse_failed ctxt pos msg "sort"); -fun parse_typ ctxt text = - let - val (syms, pos) = Syntax.parse_token ctxt Markup.typ text; - val T = +fun parse_typ ctxt = + Syntax.parse_token ctxt Term_XML.Decode.typ Markup.typ + (fn (syms, pos) => parse_raw ctxt "type" (syms, pos) |> report_result ctxt pos |> (fn t => typ_of_term (Proof_Context.get_sort ctxt (term_sorts t)) t) - handle ERROR msg => parse_failed ctxt pos msg "type"; - in T end; + handle ERROR msg => parse_failed ctxt pos msg "type"); -fun parse_term is_prop ctxt text = +fun parse_term is_prop ctxt = let val (markup, kind, root, constrain) = if is_prop then (Markup.prop, "proposition", "prop", Type.constraint propT) else (Markup.term, "term", Config.get ctxt Syntax.root, I); - val (syms, pos) = Syntax.parse_token ctxt markup text; + val decode = constrain o Term_XML.Decode.term; in - let - val results = parse_raw ctxt root (syms, pos) |> map (decode_term ctxt); - val ambiguity = length (proper_results results); - - val level = Config.get ctxt Syntax.ambiguity_level; - val limit = Config.get ctxt Syntax.ambiguity_limit; + Syntax.parse_token ctxt decode markup + (fn (syms, pos) => + let + val results = parse_raw ctxt root (syms, pos) |> map (decode_term ctxt); + val ambiguity = length (proper_results results); - val ambig_msg = - if ambiguity > 1 andalso ambiguity <= level then - ["Got more than one parse tree.\n\ - \Retry with smaller syntax_ambiguity_level for more information."] - else []; + val level = Config.get ctxt Syntax.ambiguity_level; + val limit = Config.get ctxt Syntax.ambiguity_limit; - (*brute-force disambiguation via type-inference*) - fun check t = (Syntax.check_term ctxt (constrain t); Exn.Result t) - handle exn as ERROR _ => Exn.Exn exn; + val ambig_msg = + if ambiguity > 1 andalso ambiguity <= level then + ["Got more than one parse tree.\n\ + \Retry with smaller syntax_ambiguity_level for more information."] + else []; + + (*brute-force disambiguation via type-inference*) + fun check t = (Syntax.check_term ctxt (constrain t); Exn.Result t) + handle exn as ERROR _ => Exn.Exn exn; - val results' = - if ambiguity > 1 then - (Par_List.map_name "Syntax_Phases.parse_term" o apsnd o Exn.maps_result) - check results - else results; - val reports' = fst (hd results'); + val results' = + if ambiguity > 1 then + (Par_List.map_name "Syntax_Phases.parse_term" o apsnd o Exn.maps_result) + check results + else results; + val reports' = fst (hd results'); - val errs = map snd (failed_results results'); - val checked = map snd (proper_results results'); - val len = length checked; + val errs = map snd (failed_results results'); + val checked = map snd (proper_results results'); + val len = length checked; - val show_term = Syntax.string_of_term (Config.put Printer.show_brackets true ctxt); - in - if len = 0 then - report_result ctxt pos - [(reports', Exn.Exn (Exn.EXCEPTIONS (map ERROR ambig_msg @ errs)))] - else if len = 1 then - (if ambiguity > level then - Context_Position.if_visible ctxt warning - "Fortunately, only one parse tree is type correct.\n\ - \You may still want to disambiguate your grammar or your input." - else (); report_result ctxt pos results') - else - report_result ctxt pos - [(reports', Exn.Exn (ERROR (cat_lines (ambig_msg @ - (("Ambiguous input, " ^ string_of_int len ^ " terms are type correct" ^ - (if len <= limit then "" else " (" ^ string_of_int limit ^ " displayed)") ^ ":") :: - map show_term (take limit checked))))))] - end handle ERROR msg => parse_failed ctxt pos msg kind + val show_term = Syntax.string_of_term (Config.put Printer.show_brackets true ctxt); + in + if len = 0 then + report_result ctxt pos + [(reports', Exn.Exn (Exn.EXCEPTIONS (map ERROR ambig_msg @ errs)))] + else if len = 1 then + (if ambiguity > level then + Context_Position.if_visible ctxt warning + "Fortunately, only one parse tree is type correct.\n\ + \You may still want to disambiguate your grammar or your input." + else (); report_result ctxt pos results') + else + report_result ctxt pos + [(reports', Exn.Exn (ERROR (cat_lines (ambig_msg @ + (("Ambiguous input, " ^ string_of_int len ^ " terms are type correct" ^ + (if len <= limit then "" else " (" ^ string_of_int limit ^ " displayed)") ^ ":") :: + map show_term (take limit checked))))))] + end handle ERROR msg => parse_failed ctxt pos msg kind) end; diff -r a0ed7bc688b5 -r 70072780e095 src/Pure/Thy/thy_header.scala --- a/src/Pure/Thy/thy_header.scala Sun Jul 10 17:58:11 2011 +0200 +++ b/src/Pure/Thy/thy_header.scala Sun Jul 10 20:59:04 2011 +0200 @@ -31,10 +31,10 @@ Header(f(name), imports.map(f), uses.map(f)) } - val make_xml_data: XML_Data.Make.T[Header] = + val encode_xml_data: XML_Data.Encode.T[Header] = { case Header(name, imports, uses) => - import XML_Data.Make._ + import XML_Data.Encode._ triple(string, list(string), list(string))(name, imports, uses) } diff -r a0ed7bc688b5 -r 70072780e095 src/Pure/Tools/find_theorems.ML --- a/src/Pure/Tools/find_theorems.ML Sun Jul 10 17:58:11 2011 +0200 +++ b/src/Pure/Tools/find_theorems.ML Sun Jul 10 20:59:04 2011 +0200 @@ -139,8 +139,8 @@ |> (if rem_dups then cons ("rem_dups", "") else I) |> (if is_some limit then cons ("limit", Markup.print_int (the limit)) else I); in - XML.Elem (("Query", properties), XML_Data.Make.list - (XML_Data.Make.pair XML_Data.Make.bool (single o xml_of_criterion)) criteria) + XML.Elem (("Query", properties), XML_Data.Encode.list + (XML_Data.Encode.pair XML_Data.Encode.bool (single o xml_of_criterion)) criteria) end | xml_of_query _ = raise Fail "cannot serialize goal"; @@ -149,7 +149,7 @@ val rem_dups = Properties.defined properties "rem_dups"; val limit = Properties.get properties "limit" |> Option.map Markup.parse_int; val criteria = - XML_Data.Dest.list (XML_Data.Dest.pair XML_Data.Dest.bool + XML_Data.Decode.list (XML_Data.Decode.pair XML_Data.Decode.bool (criterion_of_xml o the_single)) body; in {goal=NONE, limit=limit, rem_dups=rem_dups, criteria=criteria} @@ -190,12 +190,12 @@ val properties = if is_some opt_found then [("found", Markup.print_int (the opt_found))] else []; in - XML.Elem (("Result", properties), XML_Data.Make.list (single o xml_of_theorem) theorems) + XML.Elem (("Result", properties), XML_Data.Encode.list (single o xml_of_theorem) theorems) end; fun result_of_xml (XML.Elem (("Result", properties), body)) = (Properties.get properties "found" |> Option.map Markup.parse_int, - XML_Data.Dest.list (theorem_of_xml o the_single) body) + XML_Data.Decode.list (theorem_of_xml o the_single) body) | result_of_xml tree = raise XML_Syntax.XML ("result_of_xml: bad tree", tree); fun prop_of (Internal (_, thm)) = Thm.full_prop_of thm diff -r a0ed7bc688b5 -r 70072780e095 src/Pure/term.scala --- a/src/Pure/term.scala Sun Jul 10 17:58:11 2011 +0200 +++ b/src/Pure/term.scala Sun Jul 10 20:59:04 2011 +0200 @@ -31,58 +31,61 @@ case class Bound(index: Int) extends Term case class Abs(name: String, typ: Typ = dummyT, body: Term) extends Term case class App(fun: Term, arg: Term) extends Term +} + + +object Term_XML +{ + import Term._ /* XML data representation */ - object XML + object Encode { - object Make - { - import XML_Data.Make._ + import XML_Data.Encode._ - val indexname: T[Indexname] = pair(string, int) + val indexname: T[Indexname] = pair(string, int) - val sort: T[Sort] = list(string) + val sort: T[Sort] = list(string) - def typ: T[Typ] = - variant[Typ](List( - { case Type(a, b) => pair(string, list(typ))((a, b)) }, - { case TFree(a, b) => pair(string, sort)((a, b)) }, - { case TVar(a, b) => pair(indexname, sort)((a, b)) })) + def typ: T[Typ] = + variant[Typ](List( + { case Type(a, b) => pair(string, list(typ))((a, b)) }, + { case TFree(a, b) => pair(string, sort)((a, b)) }, + { case TVar(a, b) => pair(indexname, sort)((a, b)) })) - def term: T[Term] = - variant[Term](List( - { case Const(a, b) => pair(string, typ)((a, b)) }, - { case Free(a, b) => pair(string, typ)((a, b)) }, - { case Var(a, b) => pair(indexname, typ)((a, b)) }, - { case Bound(a) => int(a) }, - { case Abs(a, b, c) => triple(string, typ, term)((a, b, c)) }, - { case App(a, b) => pair(term, term)((a, b)) })) - } + def term: T[Term] = + variant[Term](List( + { case Const(a, b) => pair(string, typ)((a, b)) }, + { case Free(a, b) => pair(string, typ)((a, b)) }, + { case Var(a, b) => pair(indexname, typ)((a, b)) }, + { case Bound(a) => int(a) }, + { case Abs(a, b, c) => triple(string, typ, term)((a, b, c)) }, + { case App(a, b) => pair(term, term)((a, b)) })) + } - object Dest - { - import XML_Data.Dest._ + object Decode + { + import XML_Data.Decode._ - val indexname: T[Indexname] = pair(string, int) + val indexname: T[Indexname] = pair(string, int) - val sort: T[Sort] = list(string) + val sort: T[Sort] = list(string) - def typ: T[Typ] = - variant[Typ](List( - (x => { val (a, b) = pair(string, list(typ))(x); Type(a, b) }), - (x => { val (a, b) = pair(string, sort)(x); TFree(a, b) }), - (x => { val (a, b) = pair(indexname, sort)(x); TVar(a, b) }))) + def typ: T[Typ] = + variant[Typ](List( + (x => { val (a, b) = pair(string, list(typ))(x); Type(a, b) }), + (x => { val (a, b) = pair(string, sort)(x); TFree(a, b) }), + (x => { val (a, b) = pair(indexname, sort)(x); TVar(a, b) }))) - def term: T[Term] = - variant[Term](List( - (x => { val (a, b) = pair(string, typ)(x); Const(a, b) }), - (x => { val (a, b) = pair(string, typ)(x); Free(a, b) }), - (x => { val (a, b) = pair(indexname, typ)(x); Var(a, b) }), - (x => Bound(int(x))), - (x => { val (a, b, c) = triple(string, typ, term)(x); Abs(a, b, c) }), - (x => { val (a, b) = pair(term, term)(x); App(a, b) }))) - } + def term: T[Term] = + variant[Term](List( + (x => { val (a, b) = pair(string, typ)(x); Const(a, b) }), + (x => { val (a, b) = pair(string, typ)(x); Free(a, b) }), + (x => { val (a, b) = pair(indexname, typ)(x); Var(a, b) }), + (x => Bound(int(x))), + (x => { val (a, b, c) = triple(string, typ, term)(x); Abs(a, b, c) }), + (x => { val (a, b) = pair(term, term)(x); App(a, b) }))) } } diff -r a0ed7bc688b5 -r 70072780e095 src/Pure/term_xml.ML --- a/src/Pure/term_xml.ML Sun Jul 10 17:58:11 2011 +0200 +++ b/src/Pure/term_xml.ML Sun Jul 10 20:59:04 2011 +0200 @@ -15,19 +15,19 @@ signature TERM_XML = sig - structure Make: TERM_XML_OPS where type 'a T = 'a XML_Data.Make.T - structure Dest: TERM_XML_OPS where type 'a T = 'a XML_Data.Dest.T + structure Encode: TERM_XML_OPS where type 'a T = 'a XML_Data.Encode.T + structure Decode: TERM_XML_OPS where type 'a T = 'a XML_Data.Decode.T end; structure Term_XML: TERM_XML = struct -(* make *) +(* encode *) -structure Make = +structure Encode = struct -open XML_Data.Make; +open XML_Data.Encode; val indexname = pair string int; @@ -49,12 +49,12 @@ end; -(* dest *) +(* decode *) -structure Dest = +structure Decode = struct -open XML_Data.Dest; +open XML_Data.Decode; val indexname = pair string int;