src/Pure/PIDE/resources.ML
changeset 67104 a2fa0c6a7aff
parent 66771 925d10a7a610
child 67147 dea94b1aabc3
     1.1 --- a/src/Pure/PIDE/resources.ML	Mon Nov 27 16:57:34 2017 +0100
     1.2 +++ b/src/Pure/PIDE/resources.ML	Tue Nov 28 22:14:10 2017 +0100
     1.3 @@ -108,26 +108,24 @@
     1.4    | NONE => Long_Name.qualifier theory);
     1.5  
     1.6  fun theory_name qualifier theory =
     1.7 -  if loaded_theory theory then (true, theory)
     1.8 -  else
     1.9 -    let val theory' =
    1.10 -      if Long_Name.is_qualified theory orelse is_some (global_theory theory)
    1.11 -      then theory
    1.12 -      else Long_Name.qualify qualifier theory
    1.13 -    in (false, theory') end;
    1.14 +  if Long_Name.is_qualified theory orelse is_some (global_theory theory)
    1.15 +  then theory
    1.16 +  else Long_Name.qualify qualifier theory;
    1.17  
    1.18  fun import_name qualifier dir s =
    1.19 -  (case theory_name qualifier (Thy_Header.import_name s) of
    1.20 -    (true, theory) => {master_dir = Path.current, theory_name = theory}
    1.21 -  | (false, theory) =>
    1.22 -      let val node_name =
    1.23 -        (case known_theory theory of
    1.24 -          SOME node_name => node_name
    1.25 -        | NONE =>
    1.26 -            if Thy_Header.is_base_name s andalso Long_Name.is_qualified s
    1.27 -            then Path.explode s
    1.28 -            else File.full_path dir (thy_path (Path.expand (Path.explode s))))
    1.29 -      in {master_dir = Path.dir node_name, theory_name = theory} end);
    1.30 +  let val theory = theory_name qualifier (Thy_Header.import_name s) in
    1.31 +    if loaded_theory theory then {master_dir = Path.current, theory_name = theory}
    1.32 +    else
    1.33 +      let
    1.34 +        val node_name =
    1.35 +          (case known_theory theory of
    1.36 +            SOME node_name => node_name
    1.37 +          | NONE =>
    1.38 +              if Thy_Header.is_base_name s andalso Long_Name.is_qualified s
    1.39 +              then Path.explode s
    1.40 +              else File.full_path dir (thy_path (Path.expand (Path.explode s))));
    1.41 +      in {master_dir = Path.dir node_name, theory_name = theory} end
    1.42 +  end;
    1.43  
    1.44  fun check_file dir file = File.check_file (File.full_path dir file);
    1.45