removed conditional combinator;
authorwenzelm
Sat Dec 30 16:08:10 2006 +0100 (2006-12-30)
changeset 21969a8bf1106cb7c
parent 21968 883cd697112e
child 21970 1845e43aee93
removed conditional combinator;
avoid handle _;
showctxt: print_context (cf. local theory context);
searchtheorems: proper find_theorems;
refrain from setting ml_prompts again;
tuned init_pgip;
src/Pure/ProofGeneral/proof_general_pgip.ML
     1.1 --- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Sat Dec 30 16:08:09 2006 +0100
     1.2 +++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Sat Dec 30 16:08:10 2006 +0100
     1.3 @@ -316,16 +316,18 @@
     1.4      end
     1.5  
     1.6  (* FIXME: check this uses non-transitive closure function here *)
     1.7 -fun tell_thm_deps ths = conditional (Output.has_mode thm_depsN) (fn () =>
     1.8 -  let
     1.9 -    val names = filter_out (equal "") (map PureThy.get_name_hint ths);
    1.10 -    val deps = filter_out (equal "")
    1.11 -      (Symtab.keys (fold Proofterm.thms_of_proof
    1.12 -        (map Thm.proof_of ths) Symtab.empty));
    1.13 -  in
    1.14 -    if null names orelse null deps then ()
    1.15 -    else thm_deps_message (spaces_quote names, spaces_quote deps)
    1.16 -  end);
    1.17 +fun tell_thm_deps ths =
    1.18 +  if Output.has_mode thm_depsN then
    1.19 +    let
    1.20 +      val names = filter_out (equal "") (map PureThy.get_name_hint ths);
    1.21 +      val deps = filter_out (equal "")
    1.22 +        (Symtab.keys (fold Proofterm.thms_of_proof
    1.23 +          (map Thm.proof_of ths) Symtab.empty));
    1.24 +    in
    1.25 +      if null names orelse null deps then ()
    1.26 +      else thm_deps_message (spaces_quote names, spaces_quote deps)
    1.27 +    end
    1.28 +  else ();
    1.29  
    1.30  in
    1.31  
    1.32 @@ -369,7 +371,7 @@
    1.33  
    1.34          val wwwpage =
    1.35              (Url.explode (isabelle_www()))
    1.36 -            handle _ =>
    1.37 +            handle ERROR _ =>
    1.38                     (Output.panic
    1.39                          ("Error in URL in environment variable ISABELLE_HOMEPAGE.");
    1.40                          Url.explode isabellewww)
    1.41 @@ -640,13 +642,13 @@
    1.42  
    1.43  fun showproofstate vs = isarcmd "pr"
    1.44  
    1.45 -fun showctxt vs = isarcmd "print_theory"   (* more useful than print_context *)
    1.46 +fun showctxt vs = isarcmd "print_context"
    1.47  
    1.48  fun searchtheorems (Searchtheorems vs) =
    1.49      let
    1.50          val arg = #arg vs
    1.51      in
    1.52 -        isarcmd ("thms_containing " ^ arg)
    1.53 +        isarcmd ("find_theorems " ^ arg)
    1.54      end
    1.55  
    1.56  fun setlinewidth (Setlinewidth vs) =
    1.57 @@ -825,13 +827,13 @@
    1.58  
    1.59  fun process_pgip_element pgipxml =
    1.60      case pgipxml of
    1.61 -        (xml as (XML.Elem elem)) =>
    1.62 +        xml as (XML.Elem elem) =>
    1.63          (case Pgip.input elem of
    1.64               NONE => warning ("Unrecognized PGIP command, ignored: \n" ^
    1.65                                (XML.string_of_tree xml))
    1.66             | SOME inp => (process_input inp)) (* errors later; packet discarded *)
    1.67 -      | (XML.Text t) => ignored_text_warning t
    1.68 -      | (XML.Rawtext t) => ignored_text_warning t
    1.69 +      | XML.Text t => ignored_text_warning t
    1.70 +      | XML.Rawtext t => ignored_text_warning t
    1.71  and ignored_text_warning t =
    1.72      if size (Symbol.strip_blanks t) > 0 then
    1.73             warning ("Ignored text in PGIP packet: \n" ^ t)
    1.74 @@ -883,8 +885,10 @@
    1.75  fun loop ready src =
    1.76      let
    1.77          val _ = if ready then issue_pgip (Ready ()) else ()
    1.78 -        val pgipo = (Source.get_single src)
    1.79 -                        handle e => raise XML_PARSE
    1.80 +        val pgipo =
    1.81 +          (case try Source.get_single src of
    1.82 +            SOME pgipo => pgipo
    1.83 +          | NONE => raise XML_PARSE)
    1.84      in
    1.85          case pgipo of
    1.86               NONE  => ()
    1.87 @@ -969,28 +973,24 @@
    1.88  
    1.89  val initialized = ref false;
    1.90  
    1.91 -(* ML top level only for testing, entered on <quitpgip> *)
    1.92 -fun set_prompts () = ml_prompts "ML> " "ML# ";
    1.93 -
    1.94 -fun init_setup () =
    1.95 -  (conditional (not (! initialized)) (fn () =>
    1.96 -   (setmp warning_fn (K ()) init_outer_syntax ();
    1.97 -    setup_xsymbols_output ();
    1.98 -    setup_pgml_output ();
    1.99 -    setup_messages ();
   1.100 -    setup_state ();
   1.101 -    setup_thy_loader ();
   1.102 -    setup_present_hook ();
   1.103 -    init_pgip_session_id ();
   1.104 -    welcome ();
   1.105 -    set initialized; ()));
   1.106 -  sync_thy_loader ();
   1.107 -  change print_mode (cons proof_generalN o remove (op =) proof_generalN);
   1.108 -  change print_mode (append [pgmlN, pgmlatomsN] o subtract (op =) [pgmlN, pgmlatomsN]);
   1.109 -  set_prompts ());
   1.110 -
   1.111 -fun init_pgip false = Output.panic "PGIP not supported for Isabelle/classic mode."
   1.112 -  | init_pgip true = (init_setup (); pgip_toplevel tty_src);
   1.113 +fun init_pgip false =
   1.114 +      Output.panic "No Proof General interface support for Isabelle/classic mode."
   1.115 +  | init_pgip true =
   1.116 +      (! initialized orelse
   1.117 +        (setmp warning_fn (K ()) init_outer_syntax ();
   1.118 +          setup_xsymbols_output ();
   1.119 +          setup_pgml_output ();
   1.120 +          setup_messages ();
   1.121 +          setup_state ();
   1.122 +          setup_thy_loader ();
   1.123 +          setup_present_hook ();
   1.124 +          init_pgip_session_id ();
   1.125 +          welcome ();
   1.126 +          set initialized);
   1.127 +        sync_thy_loader ();
   1.128 +       change print_mode (cons proof_generalN o remove (op =) proof_generalN);
   1.129 +       change print_mode (append [pgmlN, pgmlatomsN] o subtract (op =) [pgmlN, pgmlatomsN]);
   1.130 +       pgip_toplevel tty_src);
   1.131  
   1.132  
   1.133