Add askguise/informguise as best as easily possible. Prevent warning in openfile when file doesn't exist in theory database.
authoraspinall
Fri Mar 25 17:47:11 2005 +0100 (2005-03-25 ago)
changeset 156294066f01f1beb
parent 15628 9f912f8fd2df
child 15630 cc3776f004e2
Add askguise/informguise as best as easily possible. Prevent warning in openfile when file doesn't exist in theory database.
src/Pure/proof_general.ML
     1.1 --- a/src/Pure/proof_general.ML	Fri Mar 25 16:20:57 2005 +0100
     1.2 +++ b/src/Pure/proof_general.ML	Fri Mar 25 17:47:11 2005 +0100
     1.3 @@ -434,6 +434,11 @@
     1.4  val inform_file_processed = 
     1.5      ThyInfo.if_known_thy ThyInfo.touch_child_thys o thy_name;
     1.6  
     1.7 +fun if_known_thy_no_warning f name = if ThyInfo.known_thy name then f name else ();
     1.8 +
     1.9 +val openfile_retract = 
    1.10 +    if_known_thy_no_warning ThyInfo.remove_thy o thy_name;
    1.11 +
    1.12  fun proper_inform_file_processed file state =
    1.13    let val name = thy_name file in
    1.14      if Toplevel.is_toplevel state andalso ThyInfo.known_thy name then
    1.15 @@ -646,6 +651,23 @@
    1.16  end
    1.17  
    1.18  
    1.19 +(* Reveal some information about prover state *)
    1.20 +fun send_informguise (openfile, opentheory, openproofpos) =
    1.21 +    let val guisefile = 
    1.22 +	    case openfile of SOME f => [XML.element "guisefile" 
    1.23 +						    [("url",Url.pack (Url.File (Path.unpack f)))] []]
    1.24 +			   | _ => []
    1.25 +	val guisetheory = 
    1.26 +	    case opentheory of SOME t => [XML.element "guisetheory" [("thyname", t)] []]
    1.27 +			     | _ => []
    1.28 +	val guiseproof = 
    1.29 +	    case openproofpos of SOME i => [XML.element "guiseproof" [("proofpos", string_of_int i)] []]
    1.30 +			       | _ => []
    1.31 +    in 
    1.32 +	issue_pgips [XML.element "informguise" [] (guisefile @ guisetheory @ guiseproof)]
    1.33 +    end 
    1.34 +
    1.35 +
    1.36  (* PGIP identifier tables (prover objects). [incomplete] *)
    1.37  
    1.38  local
    1.39 @@ -710,7 +732,8 @@
    1.40    | showid (_, ot, _) = error ("Cannot show objects of type "^ot)
    1.41  
    1.42  end
    1.43 -	 
    1.44 +
    1.45 +
    1.46  (** Parsing proof scripts without execution **)
    1.47  
    1.48  (* Notes.
    1.49 @@ -1138,6 +1161,10 @@
    1.50    val topthy_name = PureThy.get_name o topthy
    1.51  
    1.52    val currently_open_file = ref (NONE : string option)
    1.53 +
    1.54 +  val topnode = Toplevel.node_of o Toplevel.get_state
    1.55 +  fun topproofpos () = (case topnode() of Toplevel.Proof ph => SOME(ProofHistory.position ph) 
    1.56 +					| _ => NONE) handle Toplevel.UNDEF => NONE
    1.57  in
    1.58  
    1.59  fun process_pgip_element pgipxml = (case pgipxml of 
    1.60 @@ -1161,6 +1188,7 @@
    1.61       | "pgmlsymbolsoff"  => (print_mode := (!print_mode \ "xsymbols"))
    1.62       (* properproofcmd: proper commands which belong in script *)
    1.63       (* FIXME: next ten are by Eclipse interface, can be removed in favour of dostep *)
    1.64 +     (* NB: Isar doesn't make lemma name of goal accessible during proof *)
    1.65       | "opengoal"       => isarscript data
    1.66       | "proofstep"      => isarscript data
    1.67       | "closegoal"      => isarscript data
    1.68 @@ -1181,6 +1209,9 @@
    1.69       (* proofctxt: improper commands *)
    1.70       | "askids"         => askids (thyname_attro attrs, objtype_attro attrs)
    1.71       | "showid"	        => showid (thyname_attro attrs, objtype_attr attrs, name_attr attrs)
    1.72 +     | "askguise"	=> send_informguise (!currently_open_file,
    1.73 +					     SOME (topthy_name()) handle Toplevel.UNDEF => NONE,
    1.74 +					     topproofpos())
    1.75       | "parsescript"    => parsescript (xmltext data) attrs (* just pass back attrs unchanged *)
    1.76       | "showproofstate" => isarcmd "pr"
    1.77       | "showctxt"       => isarcmd "print_theory"   (* more useful than print_context *)
    1.78 @@ -1203,7 +1234,7 @@
    1.79       | "aborttheory"    => isarcmd ("init_toplevel")
    1.80       | "retracttheory"  => isarcmd ("kill_thy " ^ (quote (thyname_attr attrs)))
    1.81       | "loadfile"       => use_thy_or_ml_file (fileurl_of attrs)
    1.82 -     | "openfile"       => (inform_file_retracted (fileurl_of attrs);
    1.83 +     | "openfile"       => (openfile_retract (fileurl_of attrs);
    1.84  			    currently_open_file := SOME (fileurl_of attrs))
    1.85       | "closefile"      => (case !currently_open_file of 
    1.86  				SOME f => (inform_file_processed f;