99 |
99 |
100 fun explode_interval _ (Facts.FromTo (i, j)) = i upto j |
100 fun explode_interval _ (Facts.FromTo (i, j)) = i upto j |
101 | explode_interval max (Facts.From i) = i upto i + max - 1 |
101 | explode_interval max (Facts.From i) = i upto i + max - 1 |
102 | explode_interval _ (Facts.Single i) = [i] |
102 | explode_interval _ (Facts.Single i) = [i] |
103 |
103 |
|
104 val backquote = |
|
105 raw_explode #> map (fn "`" => "\\`" | s => s) #> implode #> enclose "`" "`" |
104 fun fact_from_ref ctxt reserved chained_ths (xthm as (xref, args)) = |
106 fun fact_from_ref ctxt reserved chained_ths (xthm as (xref, args)) = |
105 let |
107 let |
106 val ths = Attrib.eval_thms ctxt [xthm] |
108 val ths = Attrib.eval_thms ctxt [xthm] |
107 val bracket = |
109 val bracket = |
108 implode (map (fn arg => "[" ^ Pretty.str_of (Args.pretty_src ctxt arg) |
110 implode (map (fn arg => "[" ^ Pretty.str_of (Args.pretty_src ctxt arg) |
109 ^ "]") args) |
111 ^ "]") args) |
110 fun nth_name j = |
112 fun nth_name j = |
111 case xref of |
113 case xref of |
112 Facts.Fact s => "`" ^ s ^ "`" ^ bracket |
114 Facts.Fact s => backquote s ^ bracket |
113 | Facts.Named (("", _), _) => "[" ^ bracket ^ "]" |
115 | Facts.Named (("", _), _) => "[" ^ bracket ^ "]" |
114 | Facts.Named ((name, _), NONE) => |
116 | Facts.Named ((name, _), NONE) => |
115 make_name reserved (length ths > 1) (j + 1) name ^ bracket |
117 make_name reserved (length ths > 1) (j + 1) name ^ bracket |
116 | Facts.Named ((name, _), SOME intervals) => |
118 | Facts.Named ((name, _), SOME intervals) => |
117 make_name reserved true |
119 make_name reserved true |
802 String.isSuffix "_def_raw" (* FIXME: crude hack *) name0) then |
804 String.isSuffix "_def_raw" (* FIXME: crude hack *) name0) then |
803 I |
805 I |
804 else |
806 else |
805 let |
807 let |
806 val multi = length ths > 1 |
808 val multi = length ths > 1 |
807 val backquotify = |
809 val backquote_thm = |
808 enclose "`" "`" o string_for_term ctxt o close_form o prop_of |
810 backquote o string_for_term ctxt o close_form o prop_of |
809 fun check_thms a = |
811 fun check_thms a = |
810 case try (ProofContext.get_thms ctxt) a of |
812 case try (ProofContext.get_thms ctxt) a of |
811 NONE => false |
813 NONE => false |
812 | SOME ths' => Thm.eq_thms (ths, ths') |
814 | SOME ths' => Thm.eq_thms (ths, ths') |
813 in |
815 in |