Fri, 21 Apr 2017 20:36:20 +0200 | wenzelm | merged | changeset | files |
Fri, 21 Apr 2017 20:07:51 +0200 | wenzelm | clarified session imports; | changeset | files |
Fri, 21 Apr 2017 19:43:53 +0200 | wenzelm | clarified standard_import: based on Known.get_file as in PIDE editors; | changeset | files |
Fri, 21 Apr 2017 18:57:30 +0200 | wenzelm | afford unconditional all_known = true (reverting ea42dfd95ec8), for practical usability of qualified imports from arbitrary sessions; | changeset | files |
Fri, 21 Apr 2017 18:51:24 +0200 | wenzelm | proper imports_resources for import_name: avoid self-referential name resolution; | changeset | files |
Fri, 21 Apr 2017 17:34:13 +0200 | wenzelm | more precise position information; | changeset | files |