1(* 2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) 3 * 4 * SPDX-License-Identifier: BSD-2-Clause 5 *) 6 7theory Local_Method 8imports Main 9keywords "supply_local_method" :: prf_script % "proof" 10begin 11 12text \<open>See documentation in @{path Local_Method_Tests.thy}.\<close> 13 14ML \<open> 15 structure MethodData = Proof_Data( 16 type T = Method.method Symtab.table 17 val init = K Symtab.empty); 18\<close> 19 20method_setup local_method = \<open> 21 Scan.lift Parse.liberal_name >> 22 (fn name => fn _ => fn facts => fn (ctxt, st) => 23 case (ctxt |> MethodData.get |> Symtab.lookup) name of 24 SOME method => method facts (ctxt, st) 25 | NONE => Seq.succeed (Seq.Error (K ("Couldn't find method text named " ^ quote name)))) 26\<close> 27 28ML \<open> 29local 30 31val parse_name_text_ranges = 32 Scan.repeat1 (Parse.liberal_name --| Parse.!!! @{keyword "="} -- Method.parse) 33 34fun supply_method_cmd name_text_ranges ctxt = 35 let 36 fun add_method ((name, (text, range)), ctxt) = 37 let 38 val _ = Method.report (text, range) 39 val method = Method.evaluate text ctxt 40 in 41 MethodData.map (Symtab.update (name, method)) ctxt 42 end 43 in 44 List.foldr add_method ctxt name_text_ranges 45 end 46 47val _ = 48 Outer_Syntax.command @{command_keyword\<open>supply_local_method\<close>} 49 "Add a local method alias to the current proof context" 50 (parse_name_text_ranges >> (Toplevel.proof o Proof.map_context o supply_method_cmd)) 51 52in end 53\<close> 54 55end