1(* Title: Pure/Tools/print_operation.ML 2 Author: Makarius 3 4Print operations as asynchronous query. 5*) 6 7 8signature PRINT_OPERATION = 9sig 10 val register: string -> string -> (Toplevel.state -> Pretty.T list) -> unit 11end; 12 13structure Print_Operation: PRINT_OPERATION = 14struct 15 16(* maintain print operations *) 17 18local 19 20val print_operations = 21 Synchronized.var "print_operations" 22 ([]: (string * (string * (Toplevel.state -> Pretty.T list))) list); 23 24fun report () = 25 Output.try_protocol_message Markup.print_operations 26 let 27 val yxml = 28 Synchronized.value print_operations 29 |> map (fn (x, (y, _)) => (x, y)) |> rev 30 |> let open XML.Encode in list (pair string string) end 31 |> YXML.string_of_body; 32 in [yxml] end; 33 34val _ = Isabelle_Process.protocol_command "print_operations" (fn [] => report ()); 35 36val _ = Session.protocol_handler "isabelle.Print_Operation$Handler"; 37 38in 39 40fun register name description pr = 41 (Synchronized.change print_operations (fn tab => 42 (if not (AList.defined (op =) tab name) then () 43 else warning ("Redefining print operation: " ^ quote name); 44 AList.update (op =) (name, (description, pr)) tab)); 45 report ()); 46 47val _ = 48 Query_Operation.register {name = "print_operation", pri = Task_Queue.urgent_pri} 49 (fn {state, args, writeln_result, ...} => 50 let 51 val _ = Toplevel.context_of state handle Toplevel.UNDEF => error "Unknown context"; 52 fun err s = Pretty.mark_str (Markup.bad (), s); 53 fun print name = 54 (case AList.lookup (op =) (Synchronized.value print_operations) name of 55 SOME (_, pr) => (pr state handle Toplevel.UNDEF => [err "Unknown context"]) 56 | NONE => [err ("Unknown print operation: " ^ quote name)]); 57 in writeln_result (Pretty.string_of (Pretty.chunks (maps print args))) end); 58 59end; 60 61 62(* common print operations *) 63 64val _ = 65 register "context" "context of local theory target" Toplevel.pretty_context; 66 67val _ = 68 register "cases" "cases of proof context" 69 (Proof_Context.pretty_cases o Toplevel.context_of); 70 71val _ = 72 register "terms" "term bindings of proof context" 73 (Proof_Context.pretty_term_bindings o Toplevel.context_of); 74 75val _ = 76 register "theorems" "theorems of local theory or proof context" 77 (Isar_Cmd.pretty_theorems false); 78 79end; 80