src/Pure/ProofGeneral/pgip_isabelle.ML
changeset 23884 1d39ec4fe73f
parent 23867 743f34b12f67
child 26005 431ab3907291
equal deleted inserted replaced
23883:7d5aa704454e 23884:1d39ec4fe73f
    78         val (url,descr) =
    78         val (url,descr) =
    79             (case Position.file_of pos of
    79             (case Position.file_of pos of
    80                NONE => (NONE, NONE)
    80                NONE => (NONE, NONE)
    81              | SOME fname =>
    81              | SOME fname =>
    82                let val path = Path.explode fname in
    82                let val path = Path.explode fname in
    83                  case ThyLoad.check_file [] path of
    83                  case ThyLoad.check_file Path.current path of
    84                    SOME _ => (SOME (PgipTypes.pgipurl_of_path path), NONE)
    84                    SOME _ => (SOME (PgipTypes.pgipurl_of_path path), NONE)
    85                  | NONE => (NONE, SOME fname)
    85                  | NONE => (NONE, SOME fname)
    86                end);
    86                end);
    87     in
    87     in
    88         { descr=descr, url=url, line=line, column=NONE, char=NONE, length=NONE }
    88         { descr=descr, url=url, line=line, column=NONE, char=NONE, length=NONE }