src/Pure/proof_general.ML
changeset 18560 6b4570eb22d2
parent 18174 c6e3c6516a23
child 18587 d4dcdfd764a0
equal deleted inserted replaced
18559:05b3f033c72d 18560:6b4570eb22d2
  1195            ThyLoad.add_path dir;
  1195            ThyLoad.add_path dir;
  1196            current_working_dir := SOME dir)
  1196            current_working_dir := SOME dir)
  1197   end
  1197   end
  1198 
  1198 
  1199   val topnode = Toplevel.node_of o Toplevel.get_state
  1199   val topnode = Toplevel.node_of o Toplevel.get_state
  1200   fun topproofpos () = (case topnode() of Toplevel.Proof ph => SOME(ProofHistory.position ph)
  1200   fun topproofpos () = (case topnode() of Toplevel.Proof (h, _) => SOME(ProofHistory.position h)
  1201                                         | _ => NONE) handle Toplevel.UNDEF => NONE
  1201                                         | _ => NONE) handle Toplevel.UNDEF => NONE
  1202 in
  1202 in
  1203 
  1203 
  1204 fun process_pgip_element pgipxml = (case pgipxml of
  1204 fun process_pgip_element pgipxml = (case pgipxml of
  1205   (XML.Text t) => warning ("Ignored text in PGIP packet: \n" ^ t)
  1205   (XML.Text t) => warning ("Ignored text in PGIP packet: \n" ^ t)