actually qualify theory names;
authorwenzelm
Tue Apr 18 14:19:49 2017 +0200 (2017-04-18)
changeset 65503a3fffad8f217
parent 65502 c05bec5d01ad
child 65504 b80477da30eb
actually qualify theory names;
src/Pure/PIDE/resources.ML
src/Pure/PIDE/resources.scala
     1.1 --- a/src/Pure/PIDE/resources.ML	Mon Apr 17 21:50:56 2017 +0200
     1.2 +++ b/src/Pure/PIDE/resources.ML	Tue Apr 18 14:19:49 2017 +0200
     1.3 @@ -119,7 +119,7 @@
     1.4    | NONE =>
     1.5        let val theory =
     1.6          if Long_Name.is_qualified theory0 orelse is_some (global_theory theory0)
     1.7 -          orelse true (* FIXME *) then theory0
     1.8 +        then theory0
     1.9          else Long_Name.qualify qualifier theory0
    1.10        in (false, theory) end);
    1.11  
     2.1 --- a/src/Pure/PIDE/resources.scala	Mon Apr 17 21:50:56 2017 +0200
     2.2 +++ b/src/Pure/PIDE/resources.scala	Tue Apr 18 14:19:49 2017 +0200
     2.3 @@ -73,8 +73,8 @@
     2.4        case Some(theory) => (true, theory)
     2.5        case None =>
     2.6          val theory =
     2.7 -          if (Long_Name.is_qualified(theory0) || session_base.global_theories.isDefinedAt(theory0)
     2.8 -              || true /* FIXME */) theory0
     2.9 +          if (Long_Name.is_qualified(theory0) || session_base.global_theories.isDefinedAt(theory0))
    2.10 +            theory0
    2.11            else Long_Name.qualify(qualifier, theory0)
    2.12          (false, theory)
    2.13      }