equal
deleted
inserted
replaced
619 fun decl phi = |
619 fun decl phi = |
620 Context.mapping I init #> |
620 Context.mapping I init #> |
621 Attrib.generic_notes "" (Attrib.transform_facts phi facts) #> snd; |
621 Attrib.generic_notes "" (Attrib.transform_facts phi facts) #> snd; |
622 |
622 |
623 val modifier_report = |
623 val modifier_report = |
624 (Position.set_range (Token.range_of modifier_toks), |
624 (#1 (Token.range_of modifier_toks), |
625 Markup.properties (Position.def_properties_of pos) |
625 Markup.properties (Position.def_properties_of pos) |
626 (Markup.entity Markup.method_modifierN "")); |
626 (Markup.entity Markup.method_modifierN "")); |
627 val _ = |
627 val _ = |
628 Context_Position.reports ctxt (modifier_report :: Token.reports_of_value tok0); |
628 Context_Position.reports ctxt (modifier_report :: Token.reports_of_value tok0); |
629 val _ = Token.assign (SOME (Token.Declaration decl)) tok0; |
629 val _ = Token.assign (SOME (Token.Declaration decl)) tok0; |
745 [] => NONE |
745 [] => NONE |
746 | bad => |
746 | bad => |
747 if detect_closure_state st then NONE |
747 if detect_closure_state st then NONE |
748 else |
748 else |
749 SOME (fn () => ("Excessive case name(s): " ^ commas_quote (map Token.content_of bad) ^ |
749 SOME (fn () => ("Excessive case name(s): " ^ commas_quote (map Token.content_of bad) ^ |
750 Position.here (Position.set_range (Token.range_of bad))))) |
750 Position.here (#1 (Token.range_of bad))))) |
751 |> (fn SOME msg => Seq.single (Seq.Error msg) |
751 |> (fn SOME msg => Seq.single (Seq.Error msg) |
752 | NONE => goal_cases_tac (map Token.content_of names) (ctxt, st))))) |
752 | NONE => goal_cases_tac (map Token.content_of names) (ctxt, st))))) |
753 "bind cases for goals" #> |
753 "bind cases for goals" #> |
754 setup @{binding insert} (Attrib.thms >> (K o insert)) |
754 setup @{binding insert} (Attrib.thms >> (K o insert)) |
755 "insert theorems, ignoring facts" #> |
755 "insert theorems, ignoring facts" #> |