equal
deleted
inserted
replaced
48 } |
48 } |
49 |
49 |
50 override def append(dir: String, source_path: Path): String = |
50 override def append(dir: String, source_path: Path): String = |
51 { |
51 { |
52 val path = source_path.expand |
52 val path = source_path.expand |
53 if (path.is_absolute) Url.platform_file(path) |
53 if (dir == "" || path.is_absolute) Url.print_file(path.file) |
54 else if (dir == "") Url.platform_file(File.pwd() + path) |
|
55 else if (path.is_current) dir |
54 else if (path.is_current) dir |
56 else Url.normalize_file(dir + "/" + path.implode) |
55 else Url.normalize_file(dir + "/" + path.implode) |
57 } |
56 } |
58 |
57 |
59 override def with_thy_reader[A](name: Document.Node.Name, f: Reader[Char] => A): A = |
58 override def with_thy_reader[A](name: Document.Node.Name, f: Reader[Char] => A): A = |
63 case Some(model) => |
62 case Some(model) => |
64 val reader = new CharSequenceReader(model.doc.make_text) |
63 val reader = new CharSequenceReader(model.doc.make_text) |
65 f(reader) |
64 f(reader) |
66 |
65 |
67 case None => |
66 case None => |
68 val file = Url.file(uri) |
67 val file = Url.parse_file(uri) |
69 if (!file.isFile) error("No such file: " + quote(file.toString)) |
68 if (!file.isFile) error("No such file: " + quote(file.toString)) |
70 |
69 |
71 val reader = Scan.byte_reader(file) |
70 val reader = Scan.byte_reader(file) |
72 try { f(reader) } finally { reader.close } |
71 try { f(reader) } finally { reader.close } |
73 } |
72 } |
131 (for { |
130 (for { |
132 dep <- thy_info.dependencies("", thys).deps.iterator |
131 dep <- thy_info.dependencies("", thys).deps.iterator |
133 uri = dep.name.node |
132 uri = dep.name.node |
134 if !st.models.isDefinedAt(uri) |
133 if !st.models.isDefinedAt(uri) |
135 text <- |
134 text <- |
136 try { Some(File.read(Url.file(uri))) } |
135 try { Some(File.read(Url.parse_file(uri))) } |
137 catch { case ERROR(_) => None } |
136 catch { case ERROR(_) => None } |
138 } |
137 } |
139 yield { |
138 yield { |
140 val model = Document_Model.init(session, uri) |
139 val model = Document_Model.init(session, uri) |
141 val model1 = (model.update_text(text) getOrElse model).external(true) |
140 val model1 = (model.update_text(text) getOrElse model).external(true) |